Verification of Programs/module interfaces
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.
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
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