Verification of Erlang 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 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
- Cláudio Amaral
- Links
- erl2why
ProVal gallery of verified programs