Using Debuggers to Understand Failed Verification Attempts
OPEN ACCESS
Loading...
Author / Producer
Date
2011
Publication Type
Report
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
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.
Permanent link
Publication status
published
External links
Editor
Book title
Journal / series
Volume
713
Pages / Article No.
Publisher
ETH Zurich, Departement of Computer Science
Event
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
VERIFICATION (SOFTWARE ENGINEERING); TESTING + DEBUGGING (SOFTWARE ENGINEERING); VERIFIKATION (SOFTWARE ENGINEERING); TESTEN + FEHLERSUCHEN (SOFTWARE ENGINEERING)
Organisational unit
03653 - Müller, Peter / Müller, Peter
02150 - Dep. Informatik / Dep. of Computer Science