Verification of Erlang programs
Dilian Gurov
SICS
Abstract:
The Erlang programming language has been developed and widely used at
Ericsson for programming telecommunication applications. This kind of
software is often of a highly concurrent and dynamic nature, and it is
for this reason particularly hard to debug and test. We explore the
alternative of verifying Erlang programs, that is, of formally proving
that they behave correctly. For most real-world programming languages
this is not feasible due to their complex nature, but the core fragment
of the Erlang language is economic and clean, allowing a compact and
elegant formalization. Nevertheless, verification of Erlang programs
has to deal with challenging issues like dynamic process creation and
asynchronous message passing, requiring a rich verification framework
and adequate support by a software tool. In the course of the ErlVer
project, which runs in collaboration with Ericsson's Computer Science Lab
and is partly funded by the Advanced Software Technology competence centre,
ASTEC, we developed such a framework, designed and implemented the Erlang
Verification Tool which is publicly available, and evaluated these on a
number of case studies of various size and complexity.
This talk presents an overview of the main theoretical and practical
achievements of the ErlVer project. I will motivate and present a
verification framework for parametric, compositional and inductive
reasoning, consisting of a compositional small-step semantics for
Erlang, a recursive property specification language, and a proof
system, focusing on the methodological, language-independent aspects
of our approach. Then I will describe the Erlang Verification Tool,
its implementation, support for semi-automatic proof search, graphical
user interface, and the main case studies it has been applied to so
far. The talk concludes with a summary of our future ambitions in the
project.
Back to schedule.
Marieke Huisman
Last modified: Fri Feb 2 11:10:25 MET 2001