Prof. Bertrand Meyer.Constructor Institute, Schaffhausen (Switzerland)
In search for bugs and fixes: roaming the proof-test border
Tests and proofs, long considered competitors or adversaries in software verification, are actually complementary. Modern proof tools based on SMT solving make it possible to exploit and expand that complementarity through their reliance of the generation of counterexamples. Over the past two years (in work with involving Li Huang and Manuel Oriol) we have combined the power of SMT-based proof tools and of Eiffel’s Design by Contract to develop techniques for generating test cases, full-coverage test suites, and bug fixes (for Automatic Program Repair). One of the key insights to take advantage of the counterexamples produced by a failed attempt at a proof; failure on either side of the test-proof fence can produce useful results on the other side. The talk will explore the proof-test duality and survey these recent results, which hold the promise of significant advances in fault identification and removal.
Bertrand Meyer is Professor of Software Engineering at Constructor Institute, Schaffhausen (Switzerland). He was previously at ETH Zurich and is CTO of Eiffel Software. His latest book is a compendium on requirements: Handbook of Requirements and Business Analysis (Springer, 2022).