{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T10:52:45Z","timestamp":1760784765551,"version":"3.41.0"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"<jats:p>\n            We present a new approach to deductive program verification based on auxiliary programs called\n            <jats:italic>ghost monitors<\/jats:italic>\n            . 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.\n          <\/jats:p>\n          <jats:p>\n            We then show how ghost monitors can be used to specify and prove fine-grained properties about the\n            <jats:italic>infinite behaviors<\/jats:italic>\n            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\n            <jats:italic>catch<\/jats:italic>\n            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.\n          <\/jats:p>","DOI":"10.1145\/3371070","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Deductive verification with ghost monitors"],"prefix":"10.1145","volume":"4","author":[{"given":"Martin","family":"Clochard","sequence":"first","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"given":"Claude","family":"March\u00e9","sequence":"additional","affiliation":[{"name":"Inria, France \/ University of Paris-Saclay, France"}]},{"given":"Andrei","family":"Paskevich","sequence":"additional","affiliation":[{"name":"LRI, France \/ University of Paris-Sud, France \/ CNRS, France"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00259469"},{"volume-title":"Foundations of Software Technology and Theoretical Computer Science (Leibniz International Proceedings in Informatics), Akash Lal","author":"Banerjee Anindya","key":"e_1_2_2_2_1","unstructured":"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 \u2013 Leibniz-Zentrum f\u00fcr Informatik , 11:1\u201311:16. 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 \u2013 Leibniz-Zentrum f\u00fcr Informatik, 11:1\u201311:16."},{"key":"e_1_2_2_3_1","volume-title":"Relational Verification Using Product Programs. In International Conference on Formal Methods (Lecture Notes in Computer Science)","volume":"6664","author":"Barthe Gilles","year":"2011","unstructured":"Gilles Barthe , Juan Manuel Crespo , and C\u00e9sar Kunz . 2011 . Relational Verification Using Product Programs. In International Conference on Formal Methods (Lecture Notes in Computer Science) , Vol. 6664 . Springer, 200\u2013214. Gilles Barthe, Juan Manuel Crespo, and C\u00e9sar Kunz. 2011. Relational Verification Using Product Programs. In International Conference on Formal Methods (Lecture Notes in Computer Science), Vol. 6664. Springer, 200\u2013214."},{"key":"e_1_2_2_4_1","doi-asserted-by":"crossref","unstructured":"Richard Bornat. 2000. Proving Pointer Programs in Hoare Logic. In Mathematics of Program Construction. 102\u2013126.  Richard Bornat. 2000. Proving Pointer Programs in Hoare Logic. In Mathematics of Program Construction. 102\u2013126.","DOI":"10.1007\/10722010_8"},{"key":"e_1_2_2_5_1","unstructured":"Martin Clochard. 2018a. Hoare Logic and Games. Formal development http:\/\/toccata.lri.fr\/gallery\/hoare_logic_and_games. en.html .  Martin Clochard. 2018a. Hoare Logic and Games. Formal development http:\/\/toccata.lri.fr\/gallery\/hoare_logic_and_games. en.html ."},{"key":"e_1_2_2_6_1","unstructured":"Martin Clochard. 2018b. M\u00e9thodes et outils pour la sp\u00e9cification et la preuve de propri\u00e9t\u00e9s difficiles de programmes s\u00e9quentiels. Th\u00e8se de Doctorat. Universit\u00e9 Paris-Saclay. https:\/\/tel.archives- ouvertes.fr\/tel- 01787689 .  Martin Clochard. 2018b. M\u00e9thodes et outils pour la sp\u00e9cification et la preuve de propri\u00e9t\u00e9s difficiles de programmes s\u00e9quentiels. Th\u00e8se de Doctorat. Universit\u00e9 Paris-Saclay. https:\/\/tel.archives- ouvertes.fr\/tel- 01787689 ."},{"key":"e_1_2_2_7_1","unstructured":"Martin Clochard Jean-Christophe Filli\u00e2tre and Claude March\u00e9. 2018a. Variations on the McCarthy\u2019s 91 Function. Formal development http:\/\/toccata.lri.fr\/gallery\/mccarthy.fr.html .  Martin Clochard Jean-Christophe Filli\u00e2tre and Claude March\u00e9. 2018a. Variations on the McCarthy\u2019s 91 Function. Formal development http:\/\/toccata.lri.fr\/gallery\/mccarthy.fr.html ."},{"key":"e_1_2_2_8_1","unstructured":"Martin Clochard and Claude March\u00e9. 2018. Schorr-Waite Algorithm proved using a Ghost Monitor. Formal development http:\/\/toccata.lri.fr\/gallery\/schorr_waite_with_ghost_monitor.en.html .  Martin Clochard and Claude March\u00e9. 2018. Schorr-Waite Algorithm proved using a Ghost Monitor. Formal development http:\/\/toccata.lri.fr\/gallery\/schorr_waite_with_ghost_monitor.en.html ."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0243-x"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9433-5"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_2_14_1","volume-title":"Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR-16 (Lecture Notes in Computer Science)","author":"Leino K. Rustan M.","year":"2010","unstructured":"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\u2013370. 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\u2013370."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-12(3:6)2016"},{"key":"e_1_2_2_16_1","volume-title":"Properties of programs and partial function logic. 5","author":"Manna Zohar","year":"1970","unstructured":"Zohar Manna and John McCarthy . 1970. Properties of programs and partial function logic. 5 ( 1970 ), 79\u201398. Zohar Manna and John McCarthy. 1970. Properties of programs and partial function logic. 5 (1970), 79\u201398."},{"key":"e_1_2_2_17_1","volume-title":"Time Credits and Time Receipts in Iris. In European Symposium on Programming (LNCS), Lu\u00eds Caires (Ed.)","volume":"11423","author":"M\u00e9vel Glen","year":"2019","unstructured":"Glen M\u00e9vel , Jacques-Henri Jourdan , and Fran\u00e7ois Pottier . 2019 . Time Credits and Time Receipts in Iris. In European Symposium on Programming (LNCS), Lu\u00eds Caires (Ed.) , Vol. 11423 . Springer, 3\u201329. Glen M\u00e9vel, Jacques-Henri Jourdan, and Fran\u00e7ois Pottier. 2019. Time Credits and Time Receipts in Iris. In European Symposium on Programming (LNCS), Lu\u00eds Caires (Ed.), Vol. 11423. Springer, 3\u201329."},{"key":"e_1_2_2_18_1","volume-title":"Gordon","author":"Myreen Magnus O.","year":"2007","unstructured":"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\u2013582. 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\u2013582."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/363534.363554"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"e_1_2_2_21_1","volume-title":"VS-Theory Workshop, 3rd Int. Conf. on Verified Software: Theories, Tools and Experiments.","author":"Tuerk Thomas","year":"2010","unstructured":"Thomas Tuerk . 2010 . Local Reasoning about While-Loops . VS-Theory Workshop, 3rd Int. Conf. on Verified Software: Theories, Tools and Experiments. Thomas Tuerk. 2010. Local Reasoning about While-Loops. VS-Theory Workshop, 3rd Int. Conf. on Verified Software: Theories, Tools and Experiments."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371070","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371070","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:42Z","timestamp":1750273542000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371070"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":21,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371070"],"URL":"https:\/\/doi.org\/10.1145\/3371070","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}