@inproceedings{af2f898bc2ec41afb3a08edba2405f9a,
title = "Checking reachability using matching logic ?",
abstract = "This paper presents a verification framework that is parametric in a (trusted) operational semantics of some programming language. The underlying proof system is languageindependent 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.",
keywords = "Hoare logic, Matching logic, Reachability",
author = "Grigore Rosu and Andrei Stefanescu",
year = "2012",
doi = "10.1145/2384616.2384656",
language = "English (US)",
isbn = "9781450315616",
series = "Proceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA",
pages = "555--574",
booktitle = "SPLASH 2012",
note = "2012 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2012 ; Conference date: 19-10-2012 Through 26-10-2012",
}