Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Semantics-based program verifiers for all languages
Stefănescu A., Park D., Yuwen S., Li Y., Roşu G.  OOPSLA 2016 (Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, Amsterdam, Netherlands, Nov 2-4, 2016)74-91.2016.Type:Proceedings
Date Reviewed: Jul 20 2017

Programming is hard. Verifying correctness of a program is harder. Building an automated tool for program verification is harder still: there are very few tools that can perform verification of non-trivial programs written in real-world programming languages. We have developed powerful techniques and algorithms for verification, but a frequent stumbling block is the construction of symbolic representations of the semantics of real-world programs written in real-world programming languages.

The state of the art in program analysis often works with an implicit model of the language semantics and constructs algorithms for performing analysis that are shown to be correct, on paper, with respect to the semantic model. The question that arises is whether the semantic model faithfully captures the reality of the programming language.

This paper approaches the problem by starting with a formalization of the operational semantics of a programming language and abstracting out patterns of reasoning over the operational semantics. These patterns of reasoning are captured as rules in a logic and this in turn leads to a proof system for performing program verification. The goal is to focus all validation efforts on a single semantic model (the operational semantics) and leverage this semantics for many different applications like program verification.

A novel aspect of the paper is that all of this is carried out in a general framework, matching logic, that is completely agnostic to a programming language. The framework can express the syntax and semantics of the language, and also theories that are needed to reason about the semantics. The proof system of matching logic itself can capture, at a meta-level, the rules for reasoning about the semantic structures. Matching logic proofs then encode the proof of correctness of programs.

The core infrastructure of matching logic itself has undergone development for more than a decade and has accumulated fairly complete semantic models of programming languages like C. The entire framework, the formalization of the language, and the proof rules of matching logic are made available with the aim of increasing confidence in the approach by reproducing results and encouraging a scientific evaluation of it.

Reviewer:  Prahladavaradan Sampath Review #: CR145437 (1709-0612)
Bookmark and Share
 
Software/ Program Verification (D.2.4 )
 
 
Semantics Of Programming Languages (F.3.2 )
 
 
Specifying And Verifying And Reasoning About Programs (F.3.1 )
 
Would you recommend this review?
yes
no
Other reviews under "Software/Program Verification": Date
Verification of sequential and concurrent programs
Krzysztof R., Olderog E., Springer-Verlag New York, Inc., New York, NY, 1991. Type: Book (9780387975320)
Jul 1 1992
On verification of programs with goto statements
Lifschitz V. (ed) Information Processing Letters 18(4): 221-225, 1984. Type: Article
Mar 1 1985
The validation, verification and testing of software
Ince D. (ed), Oxford University Press, Inc., New York, NY, 1985. Type: Book (9789780198590040)
Sep 1 1987
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy