Sciweavers

CADE
2010
Springer

Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion

14 years 8 days ago
Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion
In order to support the verification of programs, verification tools such as ACL2 or Isabelle try to extract suitable induction axioms from the definitions of terminating, recursively defined procedures. However, these extraction techniques have difficulties with procedures that are defined by second-order recursion: There a first-order procedure f passes itself as an argument to a second-order procedure like map, every, foldl, etc., which leads to indirect recursive calls. For instance, secondorder recursion is commonly used in algorithms on data structures such as terms (variadic trees). We present a method to automatically extract induction axioms from such procedures. Furthermore, we describe how the induction axioms can be optimized (i. e., generalized and simplified). An implementation of our methods demonstrates that the approach facilitates straightforward inductive proofs in a verification tool.
Markus Aderhold
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2010
Where CADE
Authors Markus Aderhold
Comments (0)