Verification of Programs/module interfaces
1 Background
Erlang is an expression-oriented, single-assignment, garbage-collected, purely functional language. There are no loops, so recursion is heavily used.
Since the language is mostly used to build reliable
systems, it is good to be able to verify some
properties of Erlang programs.
erl2why[1] is a tool to help verify functional
contracts of Erlang programs. Erlang source files
with annotated properties are analysed and generated
verification conditions are translated to automatic
and/or interactive provers to be checked.
There are currently few examples of verified Erlang
programs through this tool.
2 Goal
To choose suitable pure Erlang programs or modules that could benefit from verification (BS and AVL trees, sorting algorithms’ implementations, data-structures interfaces, etc) and verify them against a specification using erl2why.
3 Work plan
- Choose the programs/modules to be verified
- Specify the behaviour of such programs/modules in natural language
- Specify the behaviour of such programs/modules formally
- Verify the Erlang programs/modules against the formal specification using
erl2why
- Contact
- ---
- Links
- A gallery of verified programs
erl2why