Files in this item

FilesDescriptionFormat

application/pdf

application/pdfrosu-stefanescu-2012-tr-d.pdf (343Kb)
(no description provided)PDF

Description

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)

Item Statistics

  • Total Downloads: 98
  • Downloads this Month: 1
  • Downloads Today: 0