Abstract The key practical issue in verifying software is to come up with the right loop invariants. We are performing an extensive analysis of loop invariants in important algorithms across all major areas of computer science, and have developed a taxonomy. I will present some of the results of this ongoing work, performed with Sergey Velder (ITMO) and Carlo Furia (ETH).
Abstract Agile methods (such as Extreme Programming, Scrum and Lean Software) are a remarkable mix of very good, unremarkable and very bad ideas. This short presentation summarizes the key agile ideas and analyzes which ones software projects should retain and which they should reject.
Abstract Frame specifications, the description of what does not change in a routine call, are one of the most annoying components of verification, in particular for object-oriented software. Ideally frame conditions should be inferred automatically. I will present how the alias calculus, described in recent papers, can address this need.
Designing good APIs is hard, and most recommendations on the topic given in the literature are very informal and difficult to apply. This talk discusses how strong behavioral specifications help construct better APIs by avoiding over-abstraction and inconsistencies in class hierarchies. We introduce model-based contracts: a methodology to equip object-oriented components with expressive and structured specifications, and to evaluate their completeness. As an example, this talk presents EiffelBase2 — a data structure library for Eiffel, developed from the start with strong specifications and with the ultimate goal of proving its full functional correctness. We focus on how strong specifications solidify the design of the library, improve its usability and enable more extensive verification.