Events

Room 20, Building I


Organizers:
Department of Informatics, New Bulgarian University

Lecturers:

Bertrand Meyer

Prof. Ph.D. Georgi Tuparov

Combining Proofs and Tests for Effective Software Verification

Bertrand Meyer

Constructor Institute, Schaffhausen, Switzerland

ABSTRACT

In the search for software quality through verification, proofs and tests have long been considered competing approaches, focused on different goals. In reality both have important contributions to make, and modern proof technology provides considerable help towards automatic test generation. In our work utilizing the AutoProof system for Eiffel, we have found that the underlying SMT solver, through its generation of counterexamples, can bring significant advances to testing. In particular, we use these techniques: for an incorrect program, to produce a set of failing tests entirely automatically; for a successful program, to generate (also automatically) a test suite guaranteeing 100% coverage; and, back in the case of a buggy program, to suggest automatic fixes (fault repairs) that are guaranteed to be correct. The talk will describe these and other advances combining the best of proving and testing techniques.


Participants:
Students and faculty staff of New Bulgarian University, business representatives, experts and researchers.

Prof. Bertrand Meyer is well-known researcher in the filed of informatics, inventor of Eiffel language. He has a significant contribution in software testing, requirements analysis and design of information systems. The lecture could be a matter of interest for students of the programme of informatics as well as other similar programmes, professionals and non-proffesionals.

Bertrand Meyer is professor and provost at Constructor Institute in Schaffhausen, Switzerland, and CTO of Eiffel Software, based in Santa Barbara. He was previous professor and head of department at ETH Zurich. He is well-known for his book, which have introduced object technology and modern software engineering techniques to a wide audience. He is the originator of the widely influential “Design by Contract” methodology for producing software that is guaranteed correct and robust, and of the Eiffel language implementing these ideas.

His contributions have spanned a wide range of topics across software engineering; his latest two books (Springer) are about agile methods (a tutorial and critique) and requirements. His many awards include the ACM Software System Award, the IEEE Harlan Mills prize for software engineering and the Dahl-Nygaard prize for object technology. He combines a strong taste for theory with a very practical slant as programmer and manager as well as technical expert in many software-related legal cases in the US and Europe. His focus is to help companies produce better software and produce software better.