Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Using Dynamic Symbolic Execution to Improve Deductive Verification

Dries Vanoverberghe, Nikolaj Bjørner, Jonathan de Halleux, Wolfram Schulte, and Nikolai Tillmann

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.

Details

Publication typeInproceedings
Published inProc. 15th International SPIN Workshop
URLhttp://dx.doi.org/10.1007/978-3-540-85114-1_4
Pages9-25
Volume5156
SeriesLecture Notes in Computer Science
ISBN978-3-540-85113-4
PublisherSpringer Verlag

Previous versions

Dries Vanoverberghe, Nikolaj Bjørner, Jonathan de Halleux, Wolfram Schulte, and Nikolai Tillmann. Using Dynamic Symbolic Execution to Improve Deductive Verification, Springer Verlag, 2008.

> Publications > Using Dynamic Symbolic Execution to Improve Deductive Verification