Deductive Verification with Ghost Monitors
| Autor: | Claude Marché, Andrei Paskevich, Martin Clochard |
|---|---|
| Přispěvatelé: | Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich), Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire de Recherche en Informatique (LRI), CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS), Laboratoire de Recherche en Informatique (LRI), CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS), Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), ANR-14-LAB3-0007,ProofInUse,Preuve en Œuvre (Intégration de la preuve dans le développement logiciel)(2014), Marché, Claude, Laboratoires communs organismes de recherche publics – PME/ETI – Vague 3 - Preuve en Œuvre (Intégration de la preuve dans le développement logiciel) - - ProofInUse2014 - ANR-14-LAB3-0007 - LABCOM - VALID |
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO]
Correctness Computer science 02 engineering and technology Hoare logic computer.software_genre Unstructured programs Infinite behaviors Deductive program verification 0202 electrical engineering electronic engineering information engineering Safety Risk Reliability and Quality Ghost code Soundness Thesaurus (information retrieval) Programming language [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Floyd-Hoare logic 020207 software engineering Hoare Logic deductive verification Computer Science::Programming Languages 020201 artificial intelligence & image processing Syntactic structure Predicate transformers Games computer Software Transfinite number Program logic |
| Zdroj: | POPL 2020-47th ACM SIGPLAN Symposium on Principles of Programming Languages POPL 2020-47th ACM SIGPLAN Symposium on Principles of Programming Languages, Jan 2020, New Orleans, United States. ⟨10.1145/3371070⟩ Proceedings of the ACM on Programming Languages, 4 (POPL) |
| ISSN: | 2475-1421 |
| DOI: | 10.3929/ethz-b-000438585 |
| Popis: | 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. Proceedings of the ACM on Programming Languages, 4 (POPL) ISSN:2475-1421 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|