Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
ISSTA
2012
ACM
8 years 6 months ago
Detecting inconsistencies via universal reachability analysis
Recent research has suggested that a large class of software bugs fall into the category of inconsistencies, or cases where two pieces of program code make incompatible assumption...
Aaron Tomb, Cormac Flanagan
CADE
2011
Springer
9 years 4 months ago
Experimenting with Deduction Modulo
Deduction modulo is a generic framework to describe proofs in a theory better than using raw axioms. This is done by presenting the theory through rules rewriting terms and proposi...
Guillaume Burel
ARESEC
2011
104views more  ARESEC 2011»
9 years 4 months ago
An Inductive Approach to Provable Anonymity
—We formalise in a theorem prover the notion of provable anonymity proposed by Garcia et al. Our formalization relies on inductive definitions of message distinguish ability and...
Yongjian Li, Jun Pang
PODC
2011
ACM
9 years 7 months ago
Securing social networks
We present a cryptographic framework to achieve access control, privacy of social relations, secrecy of resources, and anonymity of users in social networks. The main idea is to u...
Michael Backes, Matteo Maffei, Kim Pecina
PLDI
2011
ACM
9 years 7 months ago
Separation logic + superposition calculus = heap theorem prover
Program analysis and verification tools crucially depend on the ability to symbolically describe and reason about sets of program behaviors. Separation logic provides a promising...
Juan Antonio Navarro Pérez, Andrey Rybalche...
ENTCS
2006
125views more  ENTCS 2006»
10 years 4 months ago
An Even Closer Integration of Linear Arithmetic into Inductive Theorem Proving
To broaden the scope of decision procedures for linear arithmetic, they have to be integrated into theorem provers. Successful approaches e.g. in NQTHM or ACL2 suggest a close int...
Tobias Schmidt-Samoa
CSL
2010
Springer
10 years 5 months ago
A Formalisation of the Normal Forms of Context-Free Grammars in HOL4
We describe the formalisation of the normal forms of context-free grammars (CFGs) using the HOL4 theorem prover. These straightforward pen and paper proofs easily understood from t...
Aditi Barthwal, Michael Norrish
IJCAI
1989
10 years 5 months ago
A Theorem Prover for Prioritized Circumscription
In a recent paper, Ginsberg shows how a backward-chaining ATMS can be used to construct a theorem prover for circumscription. Here, this work is extended to handle prioritized cir...
Andrew B. Baker, Matthew L. Ginsberg
IJCAI
2003
10 years 5 months ago
Practical Partition-Based Theorem Proving for Large Knowledge Bases
Query answering over commonsense knowledge bases typically employs a first-order logic theorem prover. While first-order inference is intractable in general, provers can often b...
Bill MacCartney, Sheila A. McIlraith, Eyal Amir, T...
FMCAD
2008
Springer
10 years 5 months ago
Mechanized Information Flow Analysis through Inductive Assertions
We present a method for verifying information flow properties of software programs using inductive assertions and theorem proving. Given a program annotated with information flow a...
Warren A. Hunt Jr., Robert Bellarmine Krug, Sandip...
books