Sciweavers

CADE
2007
Springer
14 years 3 months ago
Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
Manna and Pnueli have extensively shown how a mixture of first-order logic (FOL) and discrete Linear time Temporal Logic (LTL) is sufficient to precisely state verification problem...
Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, D...
CADE
2007
Springer
14 years 3 months ago
Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
Abstract. First order logic provides a convenient formalism for describing a wide variety of verification conditions. Two main approaches to checking such conditions are pure first...
Yeting Ge, Clark Barrett, Cesare Tinelli
CADE
2007
Springer
14 years 3 months ago
Dependency Pairs for Rewriting with Non-free Constructors
Abstract. A method based on dependency pairs for showing termination of functional programs on data structures generated by constructors with relations is proposed. A functional pr...
Stephan Falke, Deepak Kapur
CADE
2007
Springer
14 years 3 months ago
Encoding First Order Proofs in SAT
We present a method for proving rigid first order theorems by encoding them as propositional satisfiability problems. We encode the existence of a first order connection tableau an...
Todd Deshane, Wenjin Hu, Patty Jablonski, Hai Lin,...
CADE
2007
Springer
14 years 3 months ago
Handling Polymorphism in Automated Deduction
Jean-François Couchot, Stéphane Lesc...
CADE
2007
Springer
14 years 3 months ago
T-Decision by Decomposition
Much research concerning Satisfiability Modulo Theories is devoted to the design of efficient SMT-solvers that integrate a SATsolver with T -satisfiability procedures. The rewrite-...
Maria Paola Bonacina, Mnacho Echenim
CADE
2007
Springer
14 years 3 months ago
The KeY system 1.0 (Deduction Component)
Bernhard Beckert, Martin Giese, Reiner Hähnle...
CADE
2007
Springer
14 years 3 months ago
Hyper Tableaux with Equality
Abstract. In most theorem proving applications, a proper treatment of equational theories or equality is mandatory. In this paper we show how to integrate a modern treatment of equ...
Björn Pelzer, Peter Baumgartner, Ulrich Furba...
CADE
2007
Springer
14 years 3 months ago
The Bedwyr System for Model Checking over Syntactic Expressions
David Baelde, Andrew Gacek, Dale Miller, Gopalan N...