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 definition 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', 'foldr', etc., which leads to indirect recursive calls. For instance, second-order recursion is commonly used in implementations of 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 these methods demonstrates that our approach facilitates straightforward inductive proofs in a verification tool.
A A A | Print | Imprint | Sitemap | Contact
zum Seitenanfang