Sciweavers

CSL
2001
Springer
13 years 8 months ago
Uniform Derivation of Decision Procedures by Superposition
We show how a well-known superposition-based inference system for first-order equational logic can be used almost directly as a decision procedure for various theories including l...
Alessandro Armando, Silvio Ranise, Michaël Ru...
LICS
2003
IEEE
13 years 9 months ago
New Directions in Instantiation-Based Theorem Proving
We consider instantiation-based theorem proving whereby instances of clauses are generated by certain inferences, and where inconsistency is detected by propositional tests. We gi...
Harald Ganzinger, Konstantin Korovin
LPAR
2004
Springer
13 years 9 months ago
Evaluating QBFs via Symbolic Skolemization
Abstract. We describe a novel decision procedure for Quantified Boolean Formulas (QBFs) which aims to unleash the hidden potential of quantified reasoning in applications. The Sk...
Marco Benedetti
JELIA
2004
Springer
13 years 9 months ago
Combining Decision Procedures for Sorted Theories
The Nelson-Oppen combination method combines decision procedures for theories satisfying certain conditions into a decision procedure for their union. While the method is known to ...
Cesare Tinelli, Calogero G. Zarba
FSTTCS
2004
Springer
13 years 9 months ago
A Decidable Fragment of Separation Logic
We present a fragment of separation logic oriented to linked lists, and study decision procedures for validity of entailments. The restrictions in the fragment are motivated by the...
Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
ICALP
2005
Springer
13 years 9 months ago
Combining Intruder Theories
Abstract. Most of the decision procedures for symbolic analysis of protocols are limited to a fixed set of algebraic operators associated with a fixed intruder theory. Examples o...
Yannick Chevalier, Michaël Rusinowitch
ATVA
2007
Springer
162views Hardware» more  ATVA 2007»
13 years 9 months ago
Verifying Heap-Manipulating Programs in an SMT Framework
Automated software verification has made great progress recently, and a key enabler of this progress has been the advances in efficient, automated decision procedures suitable fo...
Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. H...
SPIN
2009
Springer
13 years 10 months ago
A Decision Procedure for Detecting Atomicity Violations for Communicating Processes with Locks
Abstract. We present a new decision procedure for detecting property violations in pushdown models for concurrent programs that use lock-based synchronization, where each thread’...
Nicholas Kidd, Peter Lammich, Tayssir Touili, Thom...
LFCS
2009
Springer
13 years 10 months ago
Fuzzy Description Logic Reasoning Using a Fixpoint Algorithm
We present FixIt(ALC), a novel procedure for deciding knowledge base (KB) satisfiability in the Fuzzy Description Logic (FDL) ALC. FixIt(ALC) does not search for tree-structured m...
Uwe Keller, Stijn Heymans
VMCAI
2009
Springer
13 years 10 months ago
Deciding Extensions of the Theories of Vectors and Bags
Vectors and bags are basic collection data structures, which are used frequently in programs and specifications. Reasoning about these data structures is supported by established ...
Patrick Maier