CADE
2002
Springer
14 years 9 months ago
2002
Springer
The classical NP-complete problem of Boolean Satisfiability (SAT) has seen much interest in not just the theoretical computer science community, but also in areas where practical s...
CADE
2002
Springer
14 years 9 months ago
2002
Springer
CADE
2002
Springer
14 years 9 months ago
2002
Springer
This paper reports on the formal proof of correctness of a compiler from a substantial subset of Java source language to Java bytecode in the proof environment Isabelle. This work ...
CADE
2002
Springer
14 years 9 months ago
2002
Springer
CADE
2002
Springer
14 years 9 months ago
2002
Springer
Abstract. Proof-carrying code (PCC) allows a code producer to associate to a program a machine-checkable proof of its safety. In the original approach to PCC, the safety policy inc...
CADE
2002
Springer
14 years 9 months ago
2002
Springer
The reflection theorem has been proved using Isabelle/ZF. This theorem cannot be expressed in ZF, and its proof requires reasoning at the meta-level. There is a particularly elegan...
CADE
2002
Springer
14 years 9 months ago
2002
Springer
Abstract. We investigate the combination of propositional SAT checkers with domain-specific theorem provers as a foundation for bounded model checking over infinite domains. Given ...
CADE
2002
Springer
14 years 9 months ago
2002
Springer
Modularity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 Michael Abbott, Neil Ghani, and Christoph L?uth Union of Equational Theo...
CADE
2002
Springer
14 years 9 months ago
2002
Springer
Abstract. Description Logics are a family of class based knowledge representation formalisms characterised by the use of various constructors to build complex classes from simpler ...
CADE
2002
Springer
14 years 9 months ago
2002
Springer
We show that a conjunctive normal form (CNF) formula F is unsatisfiable iff there is a set of points of the Boolean space that is stable with respect to F. So testing the satisfiab...