Title: Using dynamic symbolic execution to improve deductive verification
Authors: Vanoverberghe, Dries ×
Bjørner, Nikolaj
de Halleux, Jonathan
Schulte, Wolfram
Tillmann, Nikolai #
Issue Date: Aug-2008
Publisher: Springer
Series Title: Lecture Notes in Computer Science vol:5156/2008 pages:9-25
Conference: International SPIN Workshop on Model Checking of Software edition:15 location:Los Angeles, USA date:10-12 August 2008
Abstract: One of the most challenging problems in deductive program verification is to find inductive program invariants typically expressed using quantifiers. With strong-enough invariants, existing provers can often prove that a program satisfies its specification. However, provers by themselves do not find such invariants. We propose to automatically generate executable test cases from failed proof attempts using dynamic symbolic execution by exploring program code as well as contracts with quantifiers. A developer can analyze the test cases with a traditional debugger to determine the cause of the error; the developer may then correct the program or the contracts and repeat the process.
Description: The original publication is available at
ISSN: 0302-9743
Publication status: published
KU Leuven publication type: IC
Appears in Collections:Informatics Section
× corresponding author
# (joint) last author

Files in This Item:
File Description Status SizeFormat
main.pdfmain article Published 248KbAdobe PDFView/Open Request a copy

These files are only available to some KU Leuven Association staff members


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science