Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Publication
Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
We present an approach for finding errors in programs and specifications. We formulate our approach as an execution mechanism for a non-deterministic guarded-command language. Guarded commands have already proved useful for verification-condition generation but are usually viewed as a non-executable representation. We show how to execute guarded commands using an explicit-state model checker. We illustrate the benefits of this approach in two related domains: bounded-exhaustive testing and falsification for Hoare triples. The basis of our approach is the delayed-choice technique for improving the execution of guarded commands. Delayed choice postpones non-deterministic choice of values until they are used. Our approach also supports copy-propagation of symbolic values but avoids the cost of full-blown symbolic execution. We describe an implementation of our approach in Java PathFinder, a popular model checker for Java programs. Our experimental results show that our techniques significantly improve performance compared to the current execution strategy in Java Pathfinder.