Mechanical proof assistants have always had support for inductive proofs. Sometimes an alternative to proof assistants, satisfiability modulo theories (SMT) solvers bring the hope of a higher degree of automation. However, SMT solvers do not natively support induction, so inductive proofs require some encoding into the SMT solver's input. This paper shows a surprisingly simple tactic - a rewriting strategy and a heuristic for when to apply it - that has shown to be useful in verifying simple inductive theorems, like those that can occur during program verification. The paper describes the tactic and its implementation in a program verifier, and reports on the positive experience with using the tactic. © 2012 Springer-Verlag.
CITATION STYLE
Leino, K. R. M. (2012). Automating induction with an SMT solver. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7148 LNCS, pp. 315–331). https://doi.org/10.1007/978-3-642-27940-9_21
Mendeley helps you to discover research relevant for your work.