Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
A tool for verifying software written in Erlang
Show others and affiliations
Number of Authors: 6
2003 (English)In: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1433-2779, E-ISSN 1433-2787, Vol. 4, 405-420 p.Article in journal (Refereed) Published
Abstract [en]

This paper presents an overview of the main results of the project "Verification of Erlang Programs", which is funded by the Swedish Business Development Agency (NUTEK) and by Ericsson within the ASTEC (Advanced Software TEChnology) initiative. Its main outcome is the Erlang Verification Tool (EVT), a theorem prover which assists in obtaining proofs that Erlang applications satisfy their correctness requirements formulated as behavioural properties in a modal logic with recursion. We give a summary of the verification framework as supported by EVT, discuss reasoning principles essential for successful proofs such as inductive and compositional reasoning, and an efficient treatment of side--effect--free code. The experiences of applying the tool in an industrial case study are summarised, and an approach for supporting verification in the presence of program libraries is outlined. EVT is essentially a classical proof assistant, or theorem proving tool, requiring users to intervene in the proof process at crucial steps such as stating program invariants. However, the tool offers considerable support for automatic proof discovery through higher--level tactics tailored to the particular task of the verification of Erlang programs. In addition, a graphical interface permits easy navigation through proof tableaux, proof reuse, and meaningful feedback about the current proof state, to assist users in taking informed proof decisions.

Place, publisher, year, edition, pages
2003, 1. Vol. 4, 405-420 p.
Keyword [en]
Formal methods - Software verification - Theorem proving
National Category
Computer and Information Science
Identifiers
URN: urn:nbn:se:ri:diva-22576DOI: 10.1007/s100090100071OAI: oai:DiVA.org:ri-22576DiVA: diva2:1042141
Available from: 2016-10-31 Created: 2016-10-31Bibliographically approved

Open Access in DiVA

No full text

Other links

Publisher's full text
In the same journal
International Journal on Software Tools for Technology Transfer (STTT)
Computer and Information Science

Search outside of DiVA

GoogleGoogle Scholar

Altmetric score

Total: 6 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
v. 2.26.0