Semi-automated verification of Erlang code

Author

Fredlund, Lars-Åke ; Gurov, Dilian ; Noll, Thomas

Author_Institution

Swedish Inst. of Comput. Sci., Stockholm, Sweden

fYear

2001

fDate

26-29 Nov. 2001

Firstpage

319

Lastpage

323

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.

Keywords

automatic programming; functional languages; message passing; parallel programming; program verification; telecommunication computing; theorem proving; Ericsson; concurrency; dynamically evolving process structures; functional programming language; goal-directed proof system based verification; message passing communication; proof parameters; proof search; semi-automated Erlang code verification; semi-automated verification task; telecommunication applications; temporal properties; verification framework; Application software; Computer languages; Computer science; Concurrent computing; Functional programming; Message passing; Pattern matching; Reactive power; Software debugging; Software testing;

fLanguage

English

Publisher

ieee

Conference_Titel

Automated Software Engineering, 2001. (ASE 2001). Proceedings. 16th Annual International Conference on

ISSN

1938-4300

Print_ISBN

0-7695-1426-X

Type

conf

DOI

10.1109/ASE.2001.989820

Filename

989820