Tools:VeriFun
From Termination-Portal.org
Revision as of 00:07, 8 August 2017 by Christoph Walther (talk | contribs) (Created page with " <!-- Please fill in the data so that your tool can be added to some default categories and a simple tool page can be created. You may extend that tool pa...")
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.
