Low-Level Program Verification using Matching Logic Reachability

From FSL
Jump to: navigation, search

Low-Level Program Verification using Matching Logic Reachability
Dwight Guth and Andrei Stefanescu and Grigore Rosu
LOLA'13. 2013
Abstract. Matching logic reachability is an emerging verification approach which uses a language-independent proof system to prove program properties based on the operational semantics. In this paper we apply this approach in the context of a low-level real-time language with interrupts, in which each instruction takes a specified time to execute. In particular, we verify that if the interrupts are scheduled with large enough intervals, the program execution terminates yielding the correct result. Surprisingly, it turns out that matching logic reachability can handle the low-level and real-time features of the language just by using their operational semantics, and that language specific reasoning is unnecessary.
PDF, Slides(PDF), Matching Logic, LOLA'13, BIB

Personal tools