CADE
2009
Springer
13 years 5 months ago
2009
Springer
CADE
2009
Springer
13 years 9 months ago
2009
Springer
CADE
2009
Springer
13 years 9 months ago
2009
Springer
CADE
2009
Springer
13 years 11 months ago
2009
Springer
CADE
2009
Springer
13 years 11 months ago
2009
Springer
SPASS is an automated theorem prover for full first-order logic with equality and a number of non-classical logics. This system description provides an overview of our recent deve...
CADE
2009
Springer
13 years 11 months ago
2009
Springer
Abstract. The problem of computing Craig interpolants in SMT has recently received a lot of interest, mainly for its applications in formal verification. Efficient algorithms for ...
CADE
2009
Springer
13 years 11 months ago
2009
Springer
predicate abstraction Shuvendu K. Lahiri and Shaz Qadeer Microsoft Research In this paper, we investigate the asymptotic complexity of various predicate abstraction problems relati...
CADE
2009
Springer
14 years 5 months ago
2009
Springer
The dependency pair framework is a powerful technique for proving termination of rewrite systems. One of the most frequently used methods within the dependency pair framework is t...
CADE
2009
Springer
14 years 5 months ago
2009
Springer
Abstract. In functional programming languages the use of infinite structures is common practice. For total correctness of programs dealing with infinite structures one must guarant...
CADE
2009
Springer
14 years 5 months ago
2009
Springer
This paper is concerned with the problem of checking whether a given subset of an unsatisfiable Boolean CNF formula takes part in the basic causes of the inconsistency of . More ...