More Web Proxy on the site http://driver.im/

research-article

Open access

Deductive verification with ghost monitors

Authors:

Martin Clochard,

Claude Marché,

Andrei PaskevichAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 4, Issue POPL

Article No.: 2, Pages 1 - 26

https://doi.org/10.1145/3371070

Published: 20 December 2019 Publication History

Abstract

We present a new approach to deductive program verification based on auxiliary programs called ghost monitors. This technique is useful when the syntactic structure of the target program is not well suited for verification, for example, when an essentially recursive algorithm is implemented in an iterative fashion. Our approach consists in implementing, specifying, and verifying an auxiliary program that monitors the execution of the target program, in such a way that the correctness of the monitor entails the correctness of the target. The ghost monitor maintains the necessary data and invariants to facilitate the proof. It can be implemented and verified in any suitable framework, which does not have to be related to the language of the target programs. This technique is also applicable when we want to establish relational properties between two target programs written in different languages and having different syntactic structure.

We then show how ghost monitors can be used to specify and prove fine-grained properties about the infinite behaviors of target programs. Since this cannot be easily done using existing verification frameworks, we introduce a dedicated language for ghost monitors, with an original construction to catch and handle divergent executions. The soundness of the underlying program logic is established using a particular flavor of transfinite games. This language and its soundness are formalized and mechanically checked.

Supplementary Material

WEBM File (a2-clochard.webm)

Download
83.87 MB

References

[1]

Ralph-Johan Back and Joakim von Wright. 1990. Duality in specification languages: a lattice-theoretical approach. Acta Informatica 27, 7 (July 1990), 583–625.

Digital Library

[2]

Anindya Banerjee, David A. Naumann, and Mohammad Nikouei. 2016. Relational Logic with Framing and Hypotheses. In Foundations of Software Technology and Theoretical Computer Science (Leibniz International Proceedings in Informatics), Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen (Eds.), Vol. 65. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 11:1–11:16.

[3]

Gilles Barthe, Juan Manuel Crespo, and César Kunz. 2011. Relational Verification Using Product Programs. In International Conference on Formal Methods (Lecture Notes in Computer Science), Vol. 6664. Springer, 200–214.

[4]

Richard Bornat. 2000. Proving Pointer Programs in Hoare Logic. In Mathematics of Program Construction. 102–126.

[5]

Martin Clochard. 2018a. Hoare Logic and Games. Formal development, http://toccata.lri.fr/gallery/hoare_logic_and_games. en.html .

[6]

Martin Clochard. 2018b. Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels. Thèse de Doctorat. Université Paris-Saclay. https://tel.archives- ouvertes.fr/tel- 01787689 .

[7]

Martin Clochard, Jean-Christophe Filliâtre, and Claude Marché. 2018a. Variations on the McCarthy’s 91 Function. Formal development, http://toccata.lri.fr/gallery/mccarthy.fr.html .

[8]

Martin Clochard and Claude Marché. 2018. Schorr-Waite Algorithm proved using a Ghost Monitor. Formal development, http://toccata.lri.fr/gallery/schorr_waite_with_ghost_monitor.en.html .

[9]

Martin Clochard, Andrei Paskevich, and Claude Marché. 2018b. Deductive Verification via Ghost Debugging. Research Report 9219. Inria. https://hal.inria.fr/hal- 01907894 .

[10]

Edsger W. Dijkstra. 1975. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18 (August 1975), 453–457. Issue 8.

Digital Library

[11]

Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. 2016. The Spirit of Ghost Code. Formal Methods in System Design 48, 3 (2016), 152–174.

Digital Library

[12]

Moritz Kiefer, Vladimir Klebanov, and Mattias Ulbrich. 2018. Relational Program Reasoning Using Compiler IR. Journal of Automated Reasoning 60, 3 (March 2018), 337–363.

Digital Library

[13]

Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. 2017. The Essence of Higher-Order Concurrent Separation Logic. In 26th European Symposium on Programming Languages and Systems (Lecture Notes in Computer Science), Vol. 10201. Springer, 696–723.

Digital Library

[14]

K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR-16 (Lecture Notes in Computer Science), Vol. 6355. Springer, 348–370.

[15]

Konstantinos Mamouras. 2016. Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism. Logical Methods in Computer Science 12, 3 (2016).

[16]

Zohar Manna and John McCarthy. 1970. Properties of programs and partial function logic. 5 (1970), 79–98.

[17]

Glen Mével, Jacques-Henri Jourdan, and François Pottier. 2019. Time Credits and Time Receipts in Iris. In European Symposium on Programming (LNCS), Luís Caires (Ed.), Vol. 11423. Springer, 3–29.

[18]

Magnus O. Myreen and Michael J. C. Gordon. 2007. Hoare Logic for Realistically Modelled Machine Code. In Tools and Algorithms for the Construction and Analysis of Systems, Orna Grumberg and Michael Huth (Eds.). Springer, 568–582.

[19]

Herbert Schorr and William M. Waite. 1967. An efficient machine-independent procedure for garbage collection in various list structures. Commun. ACM 10 (1967), 501–506.

Digital Library

[20]

Joseph Tassarotti, Ralf Jung, and Robert Harper. 2017. A Higher-Order Logic for Concurrent Termination-Preserving Refinement. In European Symposium on Programming (Lecture Notes in Computer Science), Hongseok Yang (Ed.), Vol. 10201. Springer, 909–936.

Digital Library

[21]

Thomas Tuerk. 2010. Local Reasoning about While-Loops. VS-Theory Workshop, 3rd Int. Conf. on Verified Software: Theories, Tools and Experiments.

[22]

Mattias Ulbrich. 2013. Dynamic Logic for an Intermediate Language Verification, Interaction and Refinement. Ph.D. Dissertation. Karlsruhe Institute of Technology. http://nbn- resolving.org/urn:nbn:de:swb:90- 411691

[23]

Hongseok Yang. 2007. Relational Separation Logic. Theoretical Computer Science 375, 1 (2007), 308–334.

Digital Library

Cited By

Coutelier RRath JRawson MBiere AKovács L(2024)SAT solving for variants of first-order subsumptionFormal Methods in System Design10.1007/s10703-024-00454-1Online publication date: 11-Nov-2024
https://doi.org/10.1007/s10703-024-00454-1
Antonopoulos TKoskinen ELe TNagasamudram RNaumann DNgo M(2023)An Algebra of Alignment for Relational VerificationProceedings of the ACM on Programming Languages10.1145/35712137:POPL(573-603)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571213
Banerjee ANagasamudram RNaumann DNikouei M(2023)A Relational Program Logic with Data Abstraction and Dynamic FramingACM Transactions on Programming Languages and Systems10.1145/355149744:4(1-136)Online publication date: 10-Jan-2023
https://dl.acm.org/doi/10.1145/3551497
Show More Cited By

Index Terms

Deductive verification with ghost monitors
1. Theory of computation
  1. Logic
    1. Hoare logic
    2. Logic and verification

Recommendations

The spirit of ghost code

In the context of deductive program verification, ghost code is a part of the program that is added for the purpose of specification. Ghost code must not interfere with regular code, in the sense that it can be erased without observable difference in ...
The Matrix Reproved (Verification Pearl)

In this paper we describe a complete solution for the first challenge of the VerifyThis 2016 competition held at the 18th ETAPS Forum. We present the proof of two variants for the multiplication of matrices: a naive version using three nested loops and ...
Induction as the Basis for Program Verification

We will consider the inductive mechanisms in five techniques for verifying iterative/recursive program structures: inductive assertion, predicate transformers, subgoal induction, computation induction, and structural induction. We will discover that all ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 4, Issue POPL

January 2020

1984 pages

EISSN:2475-1421

DOI:10.1145/3377388

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 December 2019

Published in PACMPL Volume 4, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
771
Total Downloads

Downloads (Last 12 months)152
Downloads (Last 6 weeks)21

Reflects downloads up to 24 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Coutelier RRath JRawson MBiere AKovács L(2024)SAT solving for variants of first-order subsumptionFormal Methods in System Design10.1007/s10703-024-00454-1Online publication date: 11-Nov-2024
https://doi.org/10.1007/s10703-024-00454-1
Antonopoulos TKoskinen ELe TNagasamudram RNaumann DNgo M(2023)An Algebra of Alignment for Relational VerificationProceedings of the ACM on Programming Languages10.1145/35712137:POPL(573-603)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571213
Banerjee ANagasamudram RNaumann DNikouei M(2023)A Relational Program Logic with Data Abstraction and Dynamic FramingACM Transactions on Programming Languages and Systems10.1145/355149744:4(1-136)Online publication date: 10-Jan-2023
https://dl.acm.org/doi/10.1145/3551497
Nagasamudram RNaumann DGorla D(2021)Alignment completeness for relational hoare logicsProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470690(1-13)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470690
Unno HTerauchi TKoskinen E(2021)Constraint-Based Relational VerificationComputer Aided Verification10.1007/978-3-030-81685-8_35(742-766)Online publication date: 15-Jul-2021
https://doi.org/10.1007/978-3-030-81685-8_35
Arrojado da Horta LSantos Reis Jde Sousa SPereira M(2020) A tool for proving Michelson Smart Contracts in WHY3 * 2020 IEEE International Conference on Blockchain (Blockchain)10.1109/Blockchain50366.2020.00059(409-414)Online publication date: Nov-2020
https://doi.org/10.1109/Blockchain50366.2020.00059
Naumann D(2020)Thirty-Seven Years of Relational Hoare Logic: Remarks on Its Principles and HistoryLeveraging Applications of Formal Methods, Verification and Validation: Engineering Principles10.1007/978-3-030-61470-6_7(93-116)Online publication date: 20-Oct-2020
https://dl.acm.org/doi/10.1007/978-3-030-61470-6_7
Becker BMarché C(2020)Ghost Code in Action: Automated Verification of a Symbolic InterpreterVerified Software. Theories, Tools, and Experiments10.1007/978-3-030-41600-3_8(107-123)Online publication date: 14-Mar-2020
https://doi.org/10.1007/978-3-030-41600-3_8

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

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

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents