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
The language supports 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
Proof development is support by additional tools:
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