Tools:VeriFun

VeriFun (... a verifier for functional programs)

• developed at Technische Universität Darmstadt, Germany
• home page: http://verifun.de
• developers: Markus Aderhold, Visar Januzaj, Andreas Schlosser, Stephan Schweitzer, Simon Siegler, Christoph Walther, Nathan Wasser
• publication: Automated Termination Analysis for Programs with Second-Order Recursion; Automated Termination Analysis for Incompletely Defined Programs; On Proving the Termination of Algorithms by Machine (see http://verifun.de/Documents for details and more)

VeriFun is a tool for verifying total correctness of functional programs. It uses a termination analysis based on the method of Argument-Bounded Functions which is automatically invoked upon the definition of a recursively defined procedure. The method aims to generate termination hypotheses which are sufficient for the procedure’s termination and are proved like lemmas. If the method fails to compute termination hypotheses, the user must provide an appropriate termination function. Afterwards induction axioms are computed from the terminating procedures’ recursion structure to be on stock for future use. See http://verifun.de/CaseStudies for a collection of examples from various domains.