IDEALS Home University of Illinois at Urbana-Champaign logo The Alma Mater The Main Quad

Checking Reachability using Matching Logic

Show full item record

Bookmark or cite this item: http://hdl.handle.net/2142/30725

Files in this item

File Description Format
PDF rosu-stefanescu-2012-tr-d.pdf (343KB) (no description provided) PDF
Title: Checking Reachability using Matching Logic
Author(s): Rosu, Grigore; Stefanescu, Andrei
Subject(s): Program verification Operational semantics Matching logic Partial correctness Relative completeness
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.
Issue Date: 2012-04
Genre: Technical Report
Type: Text
Language: English
URI: http://hdl.handle.net/2142/30725
Publication Status: unpublished
Peer Reviewed: not peer reviewed
Date Available in IDEALS: 2012-04-20
 

This item appears in the following Collection(s)

Show full item record

Item Statistics

  • Total Downloads: 73
  • Downloads this Month: 0
  • Downloads Today: 0

Browse

My Account

Information

Access Key