Everything you always wanted to know about your program
October 13, 17:45
This will be a description and hands-on demo of work in progress: an automatic program analyzer producing precise answers to questions about run-time object structures.
During its executions, a program can produce huge and complex data structures. Can we confidently predict some of their properties? Examples, important for program verification and compiler optimization, include:
- Aliasing: can two pointer expressions, say x and a.b.c, ever point to the same object?
- Reachability: is there a path from a given object to another?
- Void safety: in x.f, can x ever be a null pointer, causing the program to crash?
The last example is critical: void safety remains in almost all languages an unsolved problem. (The principal exception is Eiffel, which achieves void-safety by design.) Null-pointer calls are unpredictable and can crash any program, even after months of flawless operation. The Common Vulnerabilities and Exposure security database is replete with catastrophic null-pointer attacks involving many widely used products, even the JPEG protocol.
To provide a widely applicable solution, I have developed a theory of object structures, duality semantics, and implemented it. I will briefly outline the theory (based on abstract interpretation and my own earlier work on the Alias Calculus); but mostly the talk is a demonstration of the resulting tool, in its current partial state, on a number of examples. The target programming language is a concentrate of the mechanisms of major languages, making the concepts applicable to C, Java, C# etc.
Anyone who has had even a superficial brush with a static analysis tool, starting with the old “lint” for C, knows that in the end only one thing counts: removing false alarms. With most tools, after the initial thrill of learning a thing or two that they did not know about their program, users quickly lose interest. The reason is that these tools produce a deluge of irrelevant warnings; users must then manually and painfully comb through the list, to weed out the few genuine risks. Precision (minimizing the rate of false alarms) is the name of the game. The requirements are cruel: the only acceptable rate of false alarms, if a tool is to have any chance of practical acceptability, is very close to zero.
Thanks to the theory, the tool presented (in addition to, I hope, being sound) is precise in its approximation of run-time properties. That precision is tunable: it depends on the depth of analysis, which the user can specify, a better precision yielding a longer computation. For every context – from immediate feedback during interactive development to final thorough check before a major release – a user can decide the appropriate tradeoff between computation time and precision.
I will present the state of the work, its achievements and limitations, and say a few words about my development process.
Professor, Politecnico di Milano and Innopolis University
Bertrand Meyer is Professor of Software Engineering at Politecnico di Milano, where he leads an ERC Advanced Investigator Grant project, research professor at Innopolis University (Kazan, Russia) and Chief Architect of Eiffel Software. From the end of 2001 to the beginning of 2016 he was Professor of Software Engineering at ETH Zurich, the Swiss Federal Institute of Software Engineering.
He is the initial designer of the Eiffel method and language and has continued to participate in its evolution. He also directed the development of the EiffelStudio environment, compiler, tools and libraries through their successive versions.
His latest two books are: Agile! The Good, the Hype and the Ugly (2014), a presentation and critical analysis of agile methods; and Touch of Class: Learning to Program Well, Using Object Technology and Contracts (2009), an introductory programming textbook based on several years of teaching introductory programming at ETH and Innopolis.
Earlier books include Object-Oriented Software Construction, (winner of the Jolt Award); Eiffel: The Language; Object Success ; Reusable Software; Introduction to the Theory of Programming Languages. He has also authored numerous articles and edited or co-edited several dozen conference proceedings”.
He has been involved in a number of start-ups, most recently Propulsion Academy, Switzerland’s first coding academy, and Expertyze, a network of international experts on software technology with a particular emphasis on litigation support.
Other activities include: chair of the TOOLS conference series ; director of the LASER summer school on software engineering; member of the IFIP Working Group 2.3 on Programming Methodology; member of the French Academy of Technologies. He is also active as a consultant (object-oriented system design, architectural reviews, technology assessment, patents and software litigation), trainer in object technology and other software topics, and conference speaker. Awards include ACM Software System Award, Fellow of the ACM, Dahl-Nygaard Prize, Harlan D. Mills Prize, and honorary doctorates from the University of York in the UK and the Technical University (ITMO) in Saint Petersburg.
Prior to founding Eiffel Software in 1985, Meyer had a 9-year technical and managerial career at EDF, and was for three years on the faculty at the University of California. His experience with object technology through the Simula language, as well as early work on abstract data types and formal specification (including participation in the first versions of the Z specification language) provided some of the background for the development of Eiffel.
His research covers many different aspects of software engineering but with a single unifying theme: how to produce high-quality software (see Web site of the ETH Chair of Software Engineering).
At 2012 Bertrand joined the program committee of SECR and initiated the Best Research Paper Award.