Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

DATENSATZ AKTIONENEXPORT
Zur Ablage hinzufügen
 Lokale TagsFreigabegeschichteDetailsÜbersicht
  Temporal Verification with Transition Invariants

Rybalchenko, A. (2005). Temporal Verification with Transition Invariants. PhD Thesis, Universität des Saarlandes, Saarbrücken. doi:10.22028/D291-25890.

Item is

 

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:
Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-0027-B61C-6 Versions-Permalink: https://hdl.handle.net/21.11116/0000-000C-7A78-5
Genre: Hochschulschrift

Externe Referenzen

einblenden:
ausblenden:
externe Referenz:
http://scidok.sulb.uni-saarland.de/volltexte/2007/1280/ (beliebiger Volltext)
Beschreibung:
-
OA-Status:
Grün
externe Referenz:
http://scidok.sulb.uni-saarland.de/doku/lic_ohne_pod.php?la=de (Verlagsvertrag)
Beschreibung:
-
OA-Status:
Keine Angabe

Urheber

einblenden:
ausblenden:
 Urheber:
Rybalchenko, Andrey1, 2, 3, Autor           
Wilhelm, Rainhard4, Ratgeber
Podelski, Andreas2, Gutachter           
Affiliations:
1Group A. Rybalchenko, Max Planck Institute for Software Systems, Max Planck Society, ou_2105299              
2Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              
3International Max Planck Research School, MPI for Informatics, Max Planck Society, Campus E1 4, 66123 Saarbrücken, DE, ou_1116551              
4External Organizations, ou_persistent22              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: Program verification increases the degree of confidence that a program will
perform correctly. Manual verification is an error-prone and tedious task. Its
automation is highly desirable. The verification methodology reduces the
reasoning about temporal properties of program computations to testing the
validity of implication between auxiliary
first-order assertions. The synthesis of such auxiliary assertions is the main
challenge for automated tools. There already exist successful tools for the
verification of safety properties. These properties require that some �bad�
states never appear during program computations. The tools construct
invariants, which are auxiliary assertions for safety. Invariants are computed
symbolically by applying techniques of abstract interpretation. Liveness
properties require that some �good� states will eventually appear in every
computation. The synthesis of auxiliary assertions for the verification of
liveness properties is the next challenge for automated verification tools.
This dissertation argues that transition invariants can provide a new basis for
the development of automated methods for the verification of liveness
properties. We support this thesis as follows. We introduce a new notion of
auxiliary assertions called transition invariant. We apply this notion to
propose a proof rule for the verification of liveness properties. We provide a
viable approach for the automated synthesis of transition invariants by
abstract interpretation, which automates the proof rule. For this purpose, we
introduce a transition predicate abstraction. This abstraction does not have an
inherent limitation to preserve only safety properties.
Most liveness properties of concurrent programs only hold under certain
assumptions on non-deterministic choices made during program executions. These
assumptions are known as fairness requirements. A direct treatment of fairness
requirements in a proof rule is desirable. We specialize our proof rule for the
direct accounting of two common ways of specifying fairness. Fairness
requirements can be imposed either on program transitions or on sets of
programs states. We treat both cases via abstract-transition programs and
labeled transition invariants respectively.
We have developed a basis for the construction of automated tools that can not
only prove that a program never does anything bad, but can also prove that the
program eventually does something good. Such proofs increase our confidence
that the program will perform correctly.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2005-06-0120052005
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: Saarbrücken : Universität des Saarlandes
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: BibTex Citekey: Rybalchenko2004
DOI: 10.22028/D291-25890
URN: urn:nbn:de:bsz:291-scidok-12809
Anderer: hdl:20.500.11880/25946
 Art des Abschluß: Doktorarbeit

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle

einblenden: