Sie können Bookmarks mittels Listen verwalten, loggen Sie sich dafür bitte in Ihr SLUB Benutzerkonto ein.
Medientyp:
E-Artikel
Titel:
Checking reachability using matching logic
Beteiligte:
Rosu, Grigore;
Stefanescu, Andrei
Erschienen:
Association for Computing Machinery (ACM), 2012
Erschienen in:
ACM SIGPLAN Notices, 47 (2012) 10, Seite 555-574
Sprache:
Englisch
DOI:
10.1145/2398857.2384656
ISSN:
0362-1340;
1558-1160
Entstehung:
Anmerkungen:
Beschreibung:
<jats:p>This paper presents a verification framework that is parametric in a (trusted) operational semantics of some programming language. The underlying proof system is language-independent and consists of eight proof rules. The proof system is proved partially correct and relatively complete (with respect to the programming language configuration model). To show its practicality, the generic framework is instantiated with a fragment of C and evaluated with encouraging results.</jats:p>