CSL
2001
Springer
14 years 4 months ago
2001
Springer
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...
LICS
2003
IEEE
14 years 4 months ago
2003
IEEE
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...
LPAR
2004
Springer
14 years 4 months ago
2004
Springer
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...
JELIA
2004
Springer
14 years 4 months ago
2004
Springer
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 ...
FSTTCS
2004
Springer
14 years 4 months ago
2004
Springer
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...
ICALP
2005
Springer
14 years 5 months ago
2005
Springer
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...
ATVA
2007
Springer
14 years 5 months ago
2007
Springer
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...
SPIN
2009
Springer
14 years 6 months ago
2009
Springer
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’...
LFCS
2009
Springer
14 years 6 months ago
2009
Springer
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...
VMCAI
2009
Springer
14 years 6 months ago
2009
Springer
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 ...