Zur Kurzanzeige

dc.contributor.author
Clochard, Martin
dc.contributor.author
Marché, Claude
dc.contributor.author
Paskevich, Andrei
dc.date.accessioned
2020-09-08T15:07:50Z
dc.date.available
2020-09-04T20:05:21Z
dc.date.available
2020-09-08T15:07:50Z
dc.date.issued
2020-01
dc.identifier.issn
2475-1421
dc.identifier.other
10.1145/3371070
en_US
dc.identifier.uri
http://hdl.handle.net/20.500.11850/438585
dc.identifier.doi
10.3929/ethz-b-000438585
dc.description.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.
en_US
dc.format
application/pdf
en_US
dc.language.iso
en
en_US
dc.publisher
Association for Computing Machinery
en_US
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
dc.title
Deductive Verification with Ghost Monitors
en_US
dc.type
Conference Paper
dc.rights.license
Creative Commons Attribution 4.0 International
dc.date.published
2019-12
ethz.journal.title
Proceedings of the ACM on Programming Languages
ethz.journal.volume
4
en_US
ethz.journal.issue
POPL
en_US
ethz.journal.abbreviated
Proc. ACM Program. Lang.
ethz.pages.start
1
en_US
ethz.size
26 p.
en_US
ethz.version.deposit
publishedVersion
en_US
ethz.event
47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020)
en_US
ethz.event.location
New Orleans, Louisiana, USA
en_US
ethz.event.date
January 19-25, 2020
en_US
ethz.identifier.wos
ethz.identifier.scopus
ethz.publication.place
New York, NY
en_US
ethz.publication.status
published
en_US
ethz.leitzahl
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science::02664 - Inst. f. Programmiersprachen u. -systeme / Inst. Programming Languages and Systems::03653 - Müller, Peter / Müller, Peter
ethz.leitzahl.certified
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science::02664 - Inst. f. Programmiersprachen u. -systeme / Inst. Programming Languages and Systems::03653 - Müller, Peter / Müller, Peter
ethz.date.deposited
2020-09-04T20:05:35Z
ethz.source
SCOPUS
ethz.eth
yes
en_US
ethz.availability
Open access
en_US
ethz.rosetta.installDate
2020-09-08T15:08:11Z
ethz.rosetta.lastUpdated
2022-03-29T03:04:30Z
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.atitle=Deductive%20Verification%20with%20Ghost%20Monitors&rft.jtitle=Proceedings%20of%20the%20ACM%20on%20Programming%20Languages&rft.date=2020-01&rft.volume=4&rft.issue=POPL&rft.spage=1&rft.issn=2475-1421&rft.au=Clochard,%20Martin&March%C3%A9,%20Claude&Paskevich,%20Andrei&rft.genre=proceeding&rft_id=info:doi/10.1145/3371070&
 Printexemplar via ETH-Bibliothek suchen

Dateien zu diesem Eintrag

Thumbnail

Publikationstyp

Zur Kurzanzeige