Sciweavers

Share
CADE
2007
Springer

A Sequent Calculus for Integer Arithmetic with Counterexample Generation

9 years 5 months ago
A Sequent Calculus for Integer Arithmetic with Counterexample Generation
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 procedure and simplifier during interactive verification and as an automated tool for discharging (ground) proof obligations. There are four main components: a complete procedure for linear equations, a complete procedure for linear inequalities, an incomplete procedure for nonlinear (polynomial) equations, and an incomplete procedure for nonlinear inequalities. The calculus is complete for the generation of counterexamples for invalid ground formula in integer arithmetic. All parts described here have been implemented as part of the KeY verification system.
Philipp Rümmer
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where CADE
Authors Philipp Rümmer
Comments (0)
books