research-article

Public Access

Semantics-based program verifiers for all languages

Authors:

Grigore RoşuAuthors Info & Claims

ACM SIGPLAN Notices, Volume 51, Issue 10

Pages 74 - 91

https://doi.org/10.1145/3022671.2984027

Published: 19 October 2016 Publication History

PDF eReader

Abstract

We present a language-independent verification framework that can be instantiated with an operational semantics to automatically generate a program verifier. The framework treats both the operational semantics and the program correctness specifications as reachability rules between matching logic patterns, and uses the sound and relatively complete reachability logic proof system to prove the specifications using the semantics. We instantiate the framework with the semantics of one academic language, KernelC, as well as with three recent semantics of real-world languages, C, Java, and JavaScript, developed independently of our verification infrastructure. We evaluate our approach empirically and show that the generated program verifiers can check automatically the full functional correctness of challenging heap-manipulating programs implementing operations on list and tree data structures, like AVL trees. This is the first approach that can turn the operational semantics of real-world languages into correct-by-construction automatic verifiers.

References

[1]

VCC: A verifier for concurrent C. http://vcc. codeplex.com. Accessed: October 5, 2016.

Google Scholar

[2]

S. Antoy, R. Echahed, and M. Hanus. A needed narrowing strategy. J. ACM, 47(4):776–822, 2000.

Digital Library

Google Scholar

[3]

A. W. Appel. Verified software toolchain. In ESOP, volume 6602 of LNCS, pages 1–17, 2011.

Digital Library

Google Scholar

[4]

M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Proceedings of the 4th International Conference on Formal Methods for Components and Objects (FMCO’05), volume 4111 of LNCS, pages 364–387, 2006.

Digital Library

Google Scholar

[5]

M. Barnett, M. Fähndrich, K. R. M. Leino, P. Müller, W. Schulte, and H. Venter. Specification and verification: the Spec# experience. Commun. ACM, 54(6):81–91, 2011.

Digital Library

Google Scholar

[6]

B. Beckert, R. Hähnle, and P. H. Schmitt. Verification of Objectoriented Software: The KeY Approach. Springer-Verlag, 2007.

Digital Library

Google Scholar

[7]

G. Berry and G. Boudol. The chemical abstract machine. Theoretical Computer Science, 96(1):217–248, 1992.

Digital Library

Google Scholar

[8]

D. Bogdanas and G. Rosu. K-Java: A complete semantics of Java. In POPL, pages 445–456. ACM, 2015.

Digital Library

Google Scholar

[9]

S. Bucur, J. Kinder, and G. Candea. Prototyping symbolic execution engines for interpreted languages. In ASPLOS, pages 239–254. ACM, 2014.

Digital Library

Google Scholar

[10]

A. Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In PLDI, pages 234– 245, 2011.

Digital Library

Google Scholar

[11]

E. Cohen, M. Dahlweid, M. A. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies. VCC: A practical system for verifying concurrent C. In TPHOLs, volume 5674 of LNCS, pages 23–42, 2009.

Digital Library

Google Scholar

[12]

A. ¸ Stefănescu, S. Ciobâcă, R. Mereu¸tă, B. M. Moore, T. F. ¸ Serbănu¸tă, and G. Ro¸su. All-path reachability logic. In RTA, volume 8560 of LNCS, pages 425–440, July 2014.

Google Scholar

[13]

E. De Angelis, F. Fioravanti, A. Pettorossi, and M. Proietti. Semantics-based generation of verification conditions by program specialization. In PPDP, pages 91–102. ACM, 2015.

Digital Library

Google Scholar

[14]

L. M. de Moura and N. Bjørner. E fficient E-matching for SMT solvers. In CADE, volume 4603 of LNCS, pages 183–198, 2007.

Digital Library

Google Scholar

[15]

L. M. de Moura and N. Bjørner. Z3: An e fficient SMT solver. In TACAS, volume 4963 of LNCS, pages 337–340, 2008.

Digital Library

Google Scholar

[16]

L. M. de Moura and N. Bjørner. Generalized, e fficient array decision procedures. In FMCAD, pages 45–52. IEEE, 2009.

Google Scholar

[17]

D. Distefano and M. J. Parkinson. jStar: Towards practical verification for Java. In OOPSLA, pages 213–226. ACM, 2008.

Digital Library

Google Scholar

[18]

C. Ellison and G. Ros, u. An executable formal semantics of C with applications. In POPL, pages 533–544. ACM, 2012.

Digital Library

Google Scholar

[19]

M. Felleisen, R. B. Findler, and M. Flatt. Semantics Engineering with PLT Redex. MIT, 2009.

Digital Library

Google Scholar

[20]

J. Filliâtre and C. Marché. The why /krakatoa/caduceus platform for deductive program verification. In CAV, volume 4590 of LNCS, pages 173–177, 2007.

Digital Library

Google Scholar

[21]

J. Filliâtre and A. Paskevich. Why3 - where programs meet provers. In ESOP, volume 7792 of LNCS, pages 125–128, 2013.

Digital Library

Google Scholar

[22]

C. George, A. E. Haxthausen, S. Hughes, R. Milne, S. Prehn, and J. S. Pedersen. The RAISE Development Method. Prentice Hall, 1995.

Google Scholar

[23]

S. Grebenshchikov, N. P. Lopes, C. Popeea, and A. Rybalchenko. Synthesizing software verifiers from proof rules. In PLDI, pages 405–416. ACM, 2012.

Digital Library

Google Scholar

[24]

D. Harel, D. Kozen, and J. Tiuryn. Dynamic logic. In Handbook of Philosophical Logic, pages 497–604, 1984.

Crossref

Google Scholar

[25]

C. Hathhorn, C. Ellison, and G. Rosu. Defining the undefinedness of C. In PLDI, pages 336–345. ACM, 2015.

Digital Library

Google Scholar

[26]

B. Jacobs. Weakest pre-condition reasoning for Java programs with JML annotations. J. Logic and Algebraic Programming, 58(1-2):61–88, 2004.

Crossref

Google Scholar

[27]

B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx, and F. Piessens. Verifast: A powerful, sound, predictable, fast verifier for C and Java. In Proceedings of the Third International Conference on NASA Formal Methods (NFM’11), volume 6617 of LNCS, pages 41–55, 2011.

Digital Library

Google Scholar

[28]

S. K. Lahiri and S. Qadeer. Verifying properties of wellfounded linked lists. In POPL, pages 115–126, 2006.

Digital Library

Google Scholar

[29]

D. Leinenbach and T. Santen. Verifying the microsoft hyper-v hypervisor with VCC. In FM, volume 5850 of LNCS, pages 806–809, 2009.

Digital Library

Google Scholar

[30]

K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. In LPAR, pages 348–370, 2010.

Digital Library

Google Scholar

[31]

K. R. M. Leino, P. Müller, and J. Smans. Deadlock-free channels and locks. In ESOP, volume 6012 of LNCS, pages 407–426, 2010.

Digital Library

Google Scholar

[32]

H. Liu and J. S. Moore. Java program verification via a JVM deep embedding in ACL2. In TPHOLs, volume 3223 of LNCS, pages 184–200, 2004.

Google Scholar

[33]

P. Madhusudan, X. Qiu, and A. ¸ Stefănescu. Recursive proofs for inductive tree data-structures. In POPL, pages 123–136. ACM, 2012.

Digital Library

Google Scholar

[34]

A. Møller and M. I. Schwartzbach. The pointer assertion logic engine. In PLDI, pages 221–231, 2001.

Digital Library

Google Scholar

[35]

H. H. Nguyen, C. David, S. Qin, and W.-N. Chin. Automated verification of shape and size properties via separation logic. In VMCAI, volume 4349 of LNCS, pages 251–266, 2007.

Digital Library

Google Scholar

[36]

T. Nipkow. Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing, 10:171– 186, 1998.

Digital Library

Google Scholar

[37]

P. W. O’Hearn, J. C. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In CSL, volume 2142 of LNCS, pages 1–19, 2001.

Digital Library

Google Scholar

[38]

D. Park, A. Stefanescu, and G. Rosu. KJS: A complete formal semantics of JavaScript. In PLDI, pages 346–356. ACM, 2015.

Digital Library

Google Scholar

[39]

E. Pek, X. Qiu, and P. Madhusudan. Natural proofs for data structure manipulation in C using separation logic. In PLDI, pages 440–451. ACM, 2014.

Digital Library

Google Scholar

[40]

J. A. N. Pérez and A. Rybalchenko. Separation logic + superposition calculus = heap theorem prover. In PLDI, pages 556–566. ACM, 2011.

Digital Library

Google Scholar

[41]

X. Qiu, P. Garg, A. ¸ Stefănescu, and P. Madhusudan. Natural proofs for structure, data, and separation. In PLDI, pages 231–242. ACM, 2013.

Digital Library

Google Scholar

[42]

G. Ro¸su. Matching logic — extended abstract. In RTA, volume 36 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5–21. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2015.

Google Scholar

[43]

G. Ro¸su, A. ¸ Stefănescu, S. Ciobâcă, and B. M. Moore. Onepath reachability logic. In LICS, pages 358–367. IEEE, 2013.

Google Scholar

[44]

G. Ros, u and T.-F. S, erbănut, ă. An overview of the K semantic framework. J. Logic and Algebraic Programming, 79(6):397– 434, 2010.

Crossref

Google Scholar

[45]

G. Ros, u and A. S, tefănescu. From Hoare logic to matching logic reachability. In FM, volume 7436 of LNCS, pages 387– 402, 2012.

Google Scholar

[46]

G. Ros, u and A. S, tefănescu. Towards a unified theory of operational and axiomatic semantics. In ICALP, volume 7392 of LNCS, pages 351–363, 2012.

Google Scholar

[47]

G. Ros, u and A. S, tefănescu. Checking reachability using matching logic. In OOPSLA, pages 555–574. ACM, 2012.

Digital Library

Google Scholar

[48]

G. Ros, u, C. Ellison, and W. Schulte. Matching logic: An alternative to Hoare /Floyd logic. In AMAST, volume 6486 of LNCS, pages 142–162, 2010.

Digital Library

Google Scholar

Cited By

View all

Lorenzen ALeijen DSwierstra WLindley S(2024)The Functional Essence of Imperative Binary Search TreesProceedings of the ACM on Programming Languages10.1145/36563988:PLDI(518-542)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656398
Lin ZChen XTrinh MWang JRoşu G(2023)Generating Proof Certificates for a Language-Agnostic Deductive Program VerifierProceedings of the ACM on Programming Languages10.1145/35860297:OOPSLA1(56-84)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586029
Wang KWang JPoskitt CChen XSun JCheng P(2023)K-ST: A Formal Executable Semantics of the Structured Text Language for PLCsIEEE Transactions on Software Engineering10.1109/TSE.2023.331529249:10(4796-4813)Online publication date: 1-Oct-2023
https://dl.acm.org/doi/10.1109/TSE.2023.3315292
Show More Cited By

Index Terms

Semantics-based program verifiers for all languages

Recommendations

Semantics-based program verifiers for all languages
OOPSLA 2016: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications

We present a language-independent verification framework that can be instantiated with an operational semantics to automatically generate a program verifier. The framework treats both the operational semantics and the program correctness specifications ...
Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier

Previous work on rewriting and reachability logic establishes a vision for a language-agnostic program verifier, which takes three inputs: a program, its formal specification, and the formal semantics of the programming language in which the program is ...
Validating Formal Semantics by Property-Based Cross-Testing
IFL '20: Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages

To describe the behaviour of programs in a programming language we can define a formal semantics for the language, and formalise it in a proof assistant. From this semantics we can derive the behaviour of each particular program in the language. But ...

Reviews

Reviewer: Prahladavaradan Sampath

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. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ACM SIGPLAN Notices Volume 51, Issue 10

OOPSLA '16

October 2016

915 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/3022671

Editor:
Matthew Fluet

Issue’s Table of Contents

OOPSLA 2016: Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
October 2016
915 pages
ISBN:9781450344449
DOI:10.1145/2983990
General Chair:
Eelco Visser
Delft University of Technology, Netherlands
,
Program Chair:
Yannis Smaragdakis
University of Athens, Greece

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 October 2016

Published in SIGPLAN Volume 51, Issue 10

Check for updates

Badges

Distinguished Paper

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

53
Total Citations
View Citations
1,784
Total Downloads

Downloads (Last 12 months)250
Downloads (Last 6 weeks)29

Reflects downloads up to 22 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Lorenzen ALeijen DSwierstra WLindley S(2024)The Functional Essence of Imperative Binary Search TreesProceedings of the ACM on Programming Languages10.1145/36563988:PLDI(518-542)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656398
Lin ZChen XTrinh MWang JRoşu G(2023)Generating Proof Certificates for a Language-Agnostic Deductive Program VerifierProceedings of the ACM on Programming Languages10.1145/35860297:OOPSLA1(56-84)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586029
Wang KWang JPoskitt CChen XSun JCheng P(2023)K-ST: A Formal Executable Semantics of the Structured Text Language for PLCsIEEE Transactions on Software Engineering10.1109/TSE.2023.331529249:10(4796-4813)Online publication date: 1-Oct-2023
https://dl.acm.org/doi/10.1109/TSE.2023.3315292
Babel KDaian PKelkar MJuels A(2023)Clockwork Finance: Automated Analysis of Economic Security in Smart Contracts2023 IEEE Symposium on Security and Privacy (SP)10.1109/SP46215.2023.10179346(2499-2516)Online publication date: May-2023
https://doi.org/10.1109/SP46215.2023.10179346
Han NLi XWang GShi ZGuan Y(2020)Formal Verification of Atomicity Requirements for Smart ContractsProgramming Languages and Systems10.1007/978-3-030-64437-6_3(44-64)Online publication date: 24-Nov-2020
https://doi.org/10.1007/978-3-030-64437-6_3
Chen XRoşu GBouyer P(2019)Matching μ-logicProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470173(1-13)Online publication date: 24-Jun-2019
https://dl.acm.org/doi/10.5555/3470152.3470173
Fragoso Santos JMaksimović PSampaio GGardner P(2019)JaVerT 2.0: compositional symbolic execution for JavaScriptProceedings of the ACM on Programming Languages10.1145/32903793:POPL(1-31)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290379
Huang YBian YLi RZhao JShi P(2019)Smart Contract Security: A Software Lifecycle PerspectiveIEEE Access10.1109/ACCESS.2019.29469887(150184-150202)Online publication date: 2019
https://doi.org/10.1109/ACCESS.2019.2946988
Rouhani SDeters R(2019)Security, Performance, and Applications of Smart Contracts: A Systematic SurveyIEEE Access10.1109/ACCESS.2019.29110317(50759-50779)Online publication date: 2019
https://doi.org/10.1109/ACCESS.2019.2911031
Huang YBu XZhu GYe XZhu XShi J(2019)KST: Executable Formal Semantics of IEC 61131-3 Structured Text for VerificationIEEE Access10.1109/ACCESS.2019.28940267(14593-14602)Online publication date: 2019
https://doi.org/10.1109/ACCESS.2019.2894026
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Index Terms

Recommendations