Computing PhD Colloquium

Title: Benchmarking and Preserving Tools for Formal Methods

Presented by Dr. Dirk Beyer, Full Professor, LMU Munich, Germany

Abstract

The first part of the talk will describe the common challenges that occur during comparative evaluations of the performance of formal-methods tools (solvers, verifiers, etc.). We will also describe the tool kit BenchExec, which makes it easy for benchmarking engineers to use Linux kernel features like cgroups, name spaces, and overlay file systems.

The second part of the talk is concerned with an approach to find, use, and conserve tools for formal methods using the meta-data platform FM-Tools and the container-execution tool FM-Weck.

Speaker Bio

Dirk Beyer is Full Professor of Computer Science and has a Research Chair for Software and Computational-Systems Engineering at LMU Munich, Germany (since 2016). Before, he was Full Professor of Computer Science at University of Passau, Germany (2009-2016). He was Assistant and Associate Professor at Simon Fraser University, B.C., Canada (2006-2009), and Postdoctoral Researcher at EPFL in Lausanne, Switzerland (2004-2006) and at the University of California, Berkeley, USA (2003-2004), in the group of Tom Henzinger. Dirk Beyer holds a Dipl.-Inf. degree (1998) and a Dr. rer. nat. degree (2002) in Computer Science from the Brandenburg University of Technology in Cottbus, Germany. In 1998 he was Software Engineer with Siemens AG, SBS Dept. Major Projects in Dresden, Germany. His research focuses on models, algorithms, and tools for the construction and analysis of reliable software systems. He is architect, designer, and implementor of several successful tools. For example, CrocoPat is the first efficient interpreter for relational programming, CCVisu is a successful tool for visual clustering, and CPAchecker and BLAST are two well-known and successful software model checkers.