University of Illinois Urbana-Champaign

Checking Reachability using Matching Logic

Rosu, Grigore; Stefanescu, Andrei

Content Files
rosu-stefanescu-2012-tr-g.pdf

Permalink

https://hdl.handle.net/2142/33771

Description

Title
Checking Reachability using Matching Logic
Author(s)
  • Rosu, Grigore
  • Stefanescu, Andrei
Issue Date
2012-08
Keyword(s)
  • Reachability
  • Hoare logic
  • matching logic
Date of Ingest
2012-08-06T05:28:44Z
Abstract
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.
Type of Resource
text
Genre of Resource
Technical Report
Language
en
Permalink
http://hdl.handle.net/2142/33771

Owning Collections

Research and Tech Reports - Computer Science PRIMARY