Sciweavers

CADE
2010
Springer
14 years 16 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, recursiv...
Markus Aderhold