CADE
2012
Springer
12 years 1 months ago
2012
Springer
Abstract. This paper presents new results on the decidability of inductive validity of conjectures. For these results, a class of term rewrite systems (TRSs) with built-in linear i...
CADE
2012
Springer
12 years 1 months ago
2012
Springer
Abstract. This paper describes a novel decision procedure for quantifierfree linear integer arithmetic. Standard techniques usually relax the initial problem to the rational domai...
CADE
2007
Springer
14 years 12 months ago
2007
Springer
We introduce a calculus for handling integer arithmetic in first-order logic. The method is tailored to Java program verification and meant to be used both as a supporting procedur...