About VeriFun
VeriFun is a reasoning system for verification of statements about programs written in a simple functional language. It was designed and developed as an easy to learn and easy to use system for teaching Automated Reasoning, Semantics, Verification and similar subjects and has been used in beginner courses about Formal Methods as well as in practical courses about Program Verification for about 15 years at the Technische Universität Darmstadt.
The system’s object language provides definition principles for
- freely generated polymorphic data structures,
- procedures operating on these data structures based on recursion, case analysis and functional composition, and for
- statements (called "lemmas") about the data structures and procedures.
The language allows Unicode as well as in-, out-, pre- and postfix notation for function symbols so that readability is increased by use of the familiar mathematical notation.
In a session with the system, a user
- defines the data structures and procedures of the program as well as lemmas about these program items using the system’s language editor,
- starts the automated verification of lemmas or supports the system by using the system’s proof editor.
Proof development is support by additional tools:
- Upon the definition of a procedure, the system's automated termination analysis is invoked for generating termination hypotheses which are sufficient for the procedure's termination and are proved like lemmas.
- Proof obligations may be generalized to enable proofs by induction.
- Procedures can be tested by running them in an interpreter.
- A disprover is automatically invoked for checking system generated conjectures, like termination hypotheses or generalizations, or is called by the user to test a lemma before a proof attempt is started.
VeriFun is implemented in JAVA and installers for running the system under Windows, Unix/Linux or Mac are available for free download.
_______________________________
Last update 2016-03-02