The AutoProof technology pursues the idea of “Verification As a Matter Of Course”: making full-fledged verification an integral part of the development process. Based on Eiffel and Boogie, it supports an “auto-active” style of verification where users interactively add the necessary mechanism to permit a full proof.
This first AutoProof workshop is intended to discuss the state of AutoProof technology, needs for improvement and current advances. The workshop is results-focused rather than publication-focused; on the basis of the results we may propose a post-event proceedings volume.
The keynote will be given by Rustan Leino.