Semi-Automated Verification of Erlang Code

Lars-Åke Fredlund, Dilian Gurov, Thomas Noll

DOI 10.1109/ase.2001.989820 dblp

Abstract

Erlang is a functional programming language with support for concurrency and message passing communication that is used at Ericsson for developing telecommunication applications. We consider the challenge of verifying temporal properties of systems programmed in Erlang with dynamically evolving process structures. To accomplish this, a rich verification framework for goal-directed, proof system-based verification is used. The paper investigates the problem of semi-automating the verification task by identifying the proof parameters crucial for successful proof search.

BibTeX

@inproceedings{Fredlund-al:ASE01,
  author    = {Lars{-}{\r{A}}ke Fredlund and
               Dilian Gurov and
               Thomas Noll},
  title     = {{Semi-Automated} Verification of Erlang Code},
  booktitle = {ASE},
  pages     = {319--323},
  publisher = {{IEEE} Computer Society},
  year      = {2001},
}

Semi-Automated Verification of Erlang Code

Abstract

Related papers