Computer Science Colloquium
Dirk Beyer
University of Passau
Software Verification and Verifiable Witnesses: Report on SV-COMP 2015
Thu 12.03.2015, 17:15, 60 minutesS3-055, Science Park 3
Abstract
SV-COMP 2015 marks the start of a new epoch of software verification: In the 4th Competition on Software Verification, software verifiers produced for each reported property violation a machine-readable error witness in a common exchange format (so far restricted to reachability properties of sequential programs without recursion). Error paths were reported previously, but always in different, incompatible formats, often insufficient to reproduce the identified bug, and thus, useless to the user. The common exchange format and the support by a large set of verification tools that use the format will make a big difference: One verifier can re-verify the witnesses produced by another verifier, visual error-path navigation tools can be developed, and here in the competition, we use witness checking to make sure that a verifier that claimed a found bug, had really found a valid error path. The other two changes to SV-COMP that we made this time were (a) the addition of the new property, a set of verification tasks, and ranking category for termination verification, and (b) the addition of two new categories for reachability analysis: Arrays and Floats. SV-COMP 2015, the fourth edition of the thorough comparative evaluation of fully-automatic software verifiers, reports effectiveness and efficiency results of the state of the art in software verification. The competition used 5803 verification tasks, more than double the number of SV-COMP´14. Most impressively, the number of participating verifiers increased from 15 to 22 verification systems, including 13 new entries.Bio
Dirk Beyer is Professor of Computer Science and has a Research Chair for Software Systems at the University of Passau, Germany. He was Assistant and Associate Professor in the School of Computing Science at Simon Fraser University, B.C., Canada, 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 the 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.Invited by Univ.-Prof. Dr. Volker Strumpen, Institute for Computer Architecture
The Computer Science Colloquium is organized by the Department of Coputer Science at JKU, the Österreichische Gesellschaft für Informatik (ÖGI) and the Österreichische Computergesellschaft (OCG).