Invited Talks and Tutorials

In the last decade, advances in satisfiability-modulo-theories (SMT) solvers have powered a new generation of software tools for verification and testing. These tools transform various program analysis problems into the problem of satisfiability of formulas in propositional or first-order logic, where they are discharged by SMT solvers, such as Z3 from Microsoft Research (MSR). In this talk, I’ll review advances from MSR that expand the scope of SMT solvers on two fronts.

First, I’ll discuss queries that move beyond satisfiability: Fixed points. µZ is a scalable, efficient engine for discharging fixed point queries with logical constraints, integrated in the Z3 solver. Authors of program analysis tools can query µZ programmatically or via a Datalog input format to help establish facts that hold along all possible program execution paths. Interpolants. Interpolating Z3 uses Z3's proof generation capability to generate Craig interpolants in the first-order theory of uninterpreted functions, arrays and linear arithmetic. Interpolants have applications in abstraction refinement and invariant generation.

Second, I’ll discuss novel algorithms for complex theories: Automata. The symbolic automata toolkit lifts classical automata analyses to work modulo symbolic constraints on alphabets, using Z3, enabling the precise analysis of programs that manipulate strings. Polynomials. A new decision procedure for the existential theory of the reals allows efficient solving of systems of non-linear arithmetic constraints. The applications of this algorithm are many, ranging from hybrid systems to virtual reality environments.

These advances are due to Nikolaj Bjorner, Leonardo de Moura, Ken McMillan, and Margus Veanes at MSR, and their colleagues and interns.

Thomas Ball is Principal Researcher and Research Manager at Microsoft Research in the Research in Software Engineering area. Tom received a Ph.D. from the University of Wisconsin-Madison in 1993, was with Bell Labs from 1993-1999, and has been at Microsoft Research since 1999. Tom's interests range from program analysis, model checking, testing and automated theorem proving to the problems of defining and measuring software quality.

Software complexity is growing, so is the demand for software verification. Soon, perhaps within a decade, wide deployment of software verification tools will be indispensable or even mandatory to ensure software reliability in a large number of application domains, including but not restricted to safety and security critical systems. To adequately respond to the demand we need to eliminate tedious aspects of software verifier development, while providing support for the accomplishment of creative aspects.

We believe that the next generation of software verifiers will be constructed from logical specifications designed by quality/verification engineers with expertise in the application domain. Give a specification describing a verification method, a corresponding software verifier will be obtained by implementing a frontend that translates software source code into constraints according to the specification and then coupling the frontend with a highly-tuned general-purpose constraint solver, thus eliminating the need for algorithmic implementation efforts from the ground up. I will discuss the necessary methodology, solving algorithms, and tools for building verifiers of the future.

Joint work with Sergey Grebenshchikov, Nuno Lopes, and Corneliu Popeea.

Andrey Rybalchenko develops theories, algorithms and tools for improving the quality of software – one of the biggest challenges facing the information society. Andrey studied computer science at Saarland University and received a doctorate at the Max Planck Institute for Computer Science in Saarbrücken for his work on transition invariants. Before joining TUM, he was at Microsoft Research, École Polytechnique Fédérale de Lausanne, and the Max Planck Institute for Software Systems. Awards: MIT TR35 (2010), Microsoft Research European Fellow (2006), Otto Hahn Medal from MPG (2006).

Modern Model Checking techniques can easily verify advanced properties in complex software systems. Specifying these models and properties is as hard as ever, though. In this talk, I present techniques to extract models from legacy systems – models that are precise and complete enough to serve as specifications, and which open the door to modular verification.

Andreas Zeller is a professor for Software Engineering at Saarland University in Saarbrücken, Germany. His research concerns the analysis of large software systems and their development process; his students are funded by companies like Google, Microsoft, or SAP. In 2010, Zeller was inducted as Fellow of the ACM for his contributions to automated debugging and mining software archives. In 2011, he received an ERC Advanced Grant for work in specification mining and test case generation.

Symbolic execution has gathered significant interest in recent years as an effective technique for finding deep errors in complex software applications. In this tutorial, I will give an overview of modern dynamic symbolic execution techniques, discuss their key challenges in terms of path exploration, constraint solving, and memory modeling, and present our experience building two practical symbolic execution tools, EXE and KLEE, which are able to automatically discover serious bugs and security vulnerabilities in a diverse set of software systems, such as network servers, file systems, device drivers, packet filters, utility applications, and computer vision code.

Cristian Cadar is a Lecturer (Assistant Professor) in the Department of Computing at Imperial College London, where he leads the Software Reliability Group. His research interests span the areas of software engineering, computer systems and software security with an emphasis on building practical tools for improving the reliability and security of software systems. Cristian received a PhD in Computer Science from Stanford University, and undergraduate and Master's degrees from the Massachusetts Institute of Technology.