\ Chair of Programming Methodology ETH - Student Projects - Jürg Billeter

We do not maintain this page any more.
Please visit our new web presence for up-to-date information.

Chair of Programming Methodology

SCT Student Projects - Jürg Billeter

Master Thesis - Counterexample Execution

Goal of this master project is to make it easier to understand and locate errors reported by Boogie. We use the counterexample returned by the Z3 theorem prover to create a runtime state. The developer will be able to run the method in the debugger step-by-step from the beginning to the failing condition.

Project Timeframe:	February 2008 to August 2008
Project Description:	PDF
Project Report:	PDF
Short Demo:	Screencast
Supervisor:	Joseph N. Ruskiewicz