Speaker: Erika Ábrahám

RWTH Aachen University, Germany

Title:SMT: Something you Must Try

Abstract: SMT (Satisfiability Modulo Theories) solving is a technology for the fully automated solution of logical formulas. Due to their impressive efficiency, SMT solvers are nowadays frequently used in a wide variety of applications. These tools are general purpose and as off-the-shelf solvers, their usage is truly integrated. A typical application encodes real-world problems as logical formulas, whose solutions can be decoded to solutions of the real-world problem.

In this talk we give some insights into the mechanisms of SMT solving, discuss some areas of application, and present a novel application from the domain of simulation.

Short bio: Erika Ábrahám was born in Hungary and moved to Germany to study Computer Science at the University of Kiel. After her diploma studies, she started to work on deductive proof systems and received her Ph.D. from the University of Leiden in 2005. As a postdoctoral researcher, she was active in different areas of formal methods at the University of Freiburg and at Forschungszentrum Jülich before she was appointed a junior professorship at RWTH Aachen University in 2008, and became a full professor in 2013. Ábrahám's main research interests are formal methods for the synthesis and analysis of discrete, hybrid, and probabilistic systems. Furthermore, she is also active in the development of algorithms and tools (solvers) for satisfiability checking.

Speaker: Barbara Jobstmann

EPFL and Cadence Design Systems, Switzerland

Title: Formal Signoff Flows

Abstract: Verification sign-off flows aim to answer the question of when to stop the verification effort, i.e., when the design is good enough for tape-out (manufacturing). Classical functional verification sign-off flows are based on simulation coverage metrics, which allow one to track the performed verification effort. With the rise of formal verification in industry, formal verification sign-off flows are becoming more and more critical. In this talk, we will first discuss coverage models and metrics used in formal verification in the industry. These metrics allow analyzing a verification setup from two different angles: (1) From a controllability angle to answer questions like does the verification setup exercise all parts of the design? Did I over-constrain my design? (2) From the observability angle, to know if the set of checks is sufficient to catch potential faults in the design. To be meaningful, the metrics need to be tailored to a design. Therefore, we will next discuss methods to ensure coverage is measured in the context of design-specific scenarios. Finally, we will discuss dedicated techniques like bound aggregation and bug hunting to increase the coverage numbers.

Short bio: Barbara is a Senior Principal Product Engineer at Cadence Design Systems. Before joining the product engineering team, she worked for about 10 years as an application engineer for the Jasper platform, supporting European customers. Barbara joined Jasper in 2012 and came to Cadence as part of the Jasper acquisition. Before joining Jasper, she spent nine years doing research in the area of formal verification. First as a PhD student in Austria, then as a postdoctoral researcher in Switzerland, and finally, as an independent researcher for the French National Centre for Scientific Research (CNRS) in France. Her research focused on the development of reliable computer systems using synthesis techniques. In particular, she worked on analyzing and repairing software programs, hardware designs, transactional memories, and business process models. Since 2014, she splits her time between university and industry. She holds a lecturer position at EPFL in Switzerland and works 50% for Cadence.

Speaker: Rustan Leino

Amazon Web Services, Seattle, WA, USA

Title:Industrial experience with a verification-aware programming language

Abstract: The programming language Dafny was designed to support specifications and formal verification in a modern software-engineering setting. As a language, it blends imperative and functional features with specifications and proof authoring. The Dafny ecosystem includes not just compilers, but also, conspicuously, an automated program verifier. Following a decade of use in teaching and in research projects, the language and its verifier now also have several years of industrial use. In this talk, I reflect on some of the lessons learned from working with engineers to write and maintain verified software and how this has impacted the language and its tooling.

Short bio: K. Rustan M. Leino is a Senior Principal Applied Scientist in the Automated Reasoning Group at Amazon Web Services. He works on ways to make sure programs behave as intended, secure and functionally correct. Leino is known for his work on programming methods and program verification tools and is a world leader in building automated program verification tools. These include the languages and tools Dafny, Chalice, Jennisys, Spec#, Boogie, Houdini, ESC/Java, and ESC/Modula-3.

He is an ACM Fellow, an IFIP Fellow, and a recipient of the CAV Award.

Before Amazon, Leino was a Principal Researcher at Microsoft Research, Visiting Professor at Imperial College London, and a researcher at DEC/Compaq Systems Research Center (SRC). He received his PhD from Caltech (1995), before which he designed and wrote object-oriented software as a technical lead in the Windows NT group at Microsoft.

Leino hosts the Verification Corner channel on youtube.