Show simple item record

dc.contributor.author
Müller, Peter
dc.contributor.author
Ruskiewicz, Joseph N.
dc.date.accessioned
2017-07-28T12:01:09Z
dc.date.available
2017-06-09T09:12:03Z
dc.date.available
2017-07-28T12:01:09Z
dc.date.issued
2011
dc.identifier.uri
http://hdl.handle.net/20.500.11850/29682
dc.identifier.doi
10.3929/ethz-a-006903083
dc.description.abstract
Automatic program verification allows programmers to detect program errors at compile time. When an attempt to automatically verify a program fails the reason for the failure is often difficult to understand. Many program verifiers provide a counterexample of the failed attempt. These counterexamples are usually very complex and therefore not amenable to manual inspection. Moreover, the counterexample may be invalid, possibly misleading the programmer. We present a new approach to help the programmer understand failed verification attempts by generating an executable program that reproduces the failed verification attempt described by the counterexample. The generated program (1) can be executed within the program debugger to systematically explore the counterexample, (2) encodes the program semantics used by the verifier, which allows us to detect errors in specifications as well as in programs, and (3) contains runtime checks for all specifications, which allows us to detect spurious errors. Our approach is implemented within the Spec# programming system.
en_US
dc.format
application/pdf
dc.language.iso
en
en_US
dc.publisher
ETH Zürich, Department of Computer Science
en_US
dc.rights.uri
http://rightsstatements.org/page/InC-NC/1.0/
dc.subject
VERIFICATION (SOFTWARE ENGINEERING)
en_US
dc.subject
TESTING + DEBUGGING (SOFTWARE ENGINEERING)
en_US
dc.subject
VERIFIKATION (SOFTWARE ENGINEERING)
en_US
dc.subject
TESTEN + FEHLERSUCHEN (SOFTWARE ENGINEERING)
en_US
dc.title
Using Debuggers to Understand Failed Verification Attempts
en_US
dc.type
Report
dc.rights.license
In Copyright - Non-Commercial Use Permitted
dc.date.published
2011
ethz.journal.title
Technical Report
ethz.journal.volume
713
en_US
ethz.size
15 p.
en_US
ethz.code.ddc
DDC - DDC::0 - Computer science, information & general works::004 - Data processing, computer science
en_US
ethz.identifier.nebis
006903083
ethz.publication.place
Zürich
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
en_US
ethz.leitzahl
ETH Zürich::00002 - ETH Zürich::00012 - Lehre und Forschung::00007 - Departemente::02150 - Dep. Informatik / Dep. of Computer Science
en_US
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
2017-06-09T09:12:14Z
ethz.source
ECOL
ethz.source
ECIT
ethz.identifier.importid
imp59364d9dbe12310162
ethz.identifier.importid
imp59366b1c68bda94452
ethz.ecolpid
eth:5145
ethz.ecitpid
pub:49164
ethz.eth
yes
en_US
ethz.availability
Open access
en_US
ethz.rosetta.installDate
2017-07-19T05:54:48Z
ethz.rosetta.lastUpdated
2020-02-15T06:30:42Z
ethz.rosetta.versionExported
true
ethz.COinS
ctx_ver=Z39.88-2004&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.atitle=Using%20Debuggers%20to%20Understand%20Failed%20Verification%20Attempts&rft.jtitle=Technical%20Report&rft.date=2011&rft.volume=713&rft.au=M%C3%BCller,%20Peter&Ruskiewicz,%20Joseph%20N.&rft.genre=report&
 Search print copy at ETH Library

Files in this item

Thumbnail

Publication type

Show simple item record