Logo des Repositoriums
 

Model checking Erlang programs – LTL-propositions and abstract interpretation

Kurzanzeige
dc.contributor.authorHuch, Frank
dc.contributor.editorDadam, Peter
dc.contributor.editorReichert, Manfred
dc.date.accessioned2019-10-11T11:37:51Z
dc.date.available2019-10-11T11:37:51Z
dc.date.issued2004
dc.description.abstractWe present an approach for the formal verification of Erlang programs using abstract interpretation and model checking. In previous work we defined a framework for the verification of Erlang programs using abstract interpretation and LTL model checking. The application of LTL model checking yields some problems in the verification of state propositions, because propositions are also abstracted in the framework. While state propositions must be satisfied, negated state propositions have to be refuted. We show how this can be decided by means of the abstract domain. The approach is implemented as a prototype and we are able to prove properties like mutual exclusion or the absence of deadlocks and lifelocks for some Erlang programs.en
dc.identifier.isbn3-88579-380-6
dc.identifier.pissn1617-5468
dc.identifier.urihttps://dl.gi.de/handle/20.500.12116/28809
dc.language.isoen
dc.publisherGesellschaft für Informatik e.V.
dc.relation.ispartofInformatik 2004, Informatik verbindet, Band 2, Beiträge der 34. Jahrestagung der Gesellschaft für Informatik e.V. (GI)
dc.relation.ispartofseriesLecture Notes in Informatics (LNI) - Proceedings, Volume P-51
dc.titleModel checking Erlang programs – LTL-propositions and abstract interpretationen
dc.typeText/Conference Paper
gi.citation.endPage448
gi.citation.publisherPlaceBonn
gi.citation.startPage438
gi.conference.date20.-24. September 2004
gi.conference.locationUlm
gi.conference.sessiontitleRegular Research Papers

Dateien

Originalbündel
1 - 1 von 1
Vorschaubild
Name:
GI-Proceedings.51-93.pdf
Größe:
340.94 KB
Format:
Adobe Portable Document Format
Herunterladen

Sammlungen

P051 - INFORMATIK 2004 - Informatik verbindet - Band 2