22–24 July 2015, L'Aquila, Italy
In the mind of the practitioner, the term “formal specification” often conjures up ghastly images of impenetrable logic formulas that only highly-trained experts can digest. Our experience with using contracts indicates, however, that developing simple elements of formal specification embedded in the program text as assertions requires an effort that is generally compatible with standard development practices. In exchange for it, even the very simple contracts that programmers write can improve the effectiveness of a variety of analysis and verification techniques.
In this tutorial, I will present a number of tools we developed for the Eiffel programming language that take advantage of contracts in various guises. AutoTest generates random unit tests and uses contracts as oracles to automatically detect bugs; it has been used to find hundreds of errors in standard libraries. AutoFix builds source-code patches that turn failing tests into passing tests, thus automatically providing program repair for real software faults. AutoProof supports the static full-fledged verification of functional properties in object-oriented software; it has been used to verify the complete functionality of a realistic general-purpose container library. The various tools demonstrate a variety of techniques both dynamic (tests and runtime checking) and static (correctness proofs), which all leverage contracts to improve their effectiveness.
Carlo A. Furia is a senior researcher at the Chair of Software Engineering in the Department of Computer Science of ETH Zurich. In his research he develops models, techniques, methods, and tools to support the analysis, rigorous development, and verification of software and software-intensive systems. His recent research has focused on improving the applicability and practicality of formal methods by taking advantage of simple program annotations such as contracts and by combining static and dynamic techniques. He is co-chairing SCORE (the student contest on software engineering), an event of ICSE 2016. He has a PhD in Computer Science from the Politecnico di Milano.