Abstract:
Recent advances in software validation and verification make it possible to widely automate whether a specification is satisfied. This progress is hampered, though, by the persistent difficulty of writing spec- ifications. Are we facing a “specification crisis”? We can alleviate the problem by leveraging existing code as a source for abstract descriptions of how software behaves. To infer correct usage, code analysis needs usage examples, though; the more, the better. Such usage examples can come from _executions_: Leveraging modern test case generation techniques, we can systematically explore the specification space, resulting in precise models of software behavior. A second source is _code instances_: We have built a lightweight parser that efficiently extracts API usage models from source code–models that can then be used to detect anomalies. Applied on the 200 million lines of code of the Gentoo Linux distribution, we would extract more than 15 million API constraints, encoding and abstracting the “wisdom of Linux code”. (A public prototype is available at http://www.checkmycode.org/.)

Bio:
Andreas Zeller is professor for software engineering at Saarland University, Saarbrücken, Germany. His research is concerned with the analysis of large software systems, in particular their execution and their development history. He is one of the pioneers in automated debugging ("Why does my program fail?") and mining software archives ("Where do most bugs occur?").