Write a Blog >>
MSR 2019
Sun 26 - Mon 27 May 2019 Montreal, QC, Canada
co-located with ICSE 2019

The analysis of correctness proofs and counterexamples of program source code is an important way to gain insights into methods that could make it easier in the future to find invariants to prove a program correct or to find bugs. The availability of high-quality data is often a limiting factor for researchers who want to study real program invariants and real bugs. The described data set provides a large collection of concrete verification results, which can be used in research projects as data source or for evaluation purposes. Each result is made available as verification witness, which represents either program invariants that were used to prove the program correct (correctness witness) or an error path to replay the actual bug (violation witness). The verification results are taken from actual verification runs on 10 522 verification problems, using the 31 verification tools that participated in the 8th edition of the International Competition on Software Verification (SV-COMP). The collection contains a total of 125 720 verification witnesses together with various meta data and a map to relate a witness to the C program that it originates from. Data set is available at: https://doi.org/10.5281/zenodo.2559175

Dirk Beyer is Professor of Computer Science and has a Research Chair for Software Systems at LMU Munich, Germany. He was Full Professor at University of Passau (2009-2016), Assistant and Associate Professor 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.

Sun 26 May

msr-2019-Paper-Presentations
11:55 - 12:30: MSR 2019 Paper Presentations - Session IV: Defect Prediction and Testing (Part 2) at Centre-Ville
Chair(s): Jesus M. Gonzalez-BarahonaUniversidad Rey Juan Carlos
msr-2019-Data-Showcase11:55 - 12:01
Talk
Aida Radu, Sarah NadiUniversity of Alberta
Pre-print
msr-2019-papers12:01 - 12:07
Short-paper
Adithya Raghuraman, Truong Ho-Quang, Michel ChaudronChalmers University of Technology, Alexander SerebrenikEindhoven University of Technology, Bogdan VasilescuCarnegie Mellon University
Pre-print
msr-2019-papers12:07 - 12:13
Short-paper
Stanislav ChrenMasaryk University, Radoslav Micko, Barbora BuhnovaMasaryk University, Bruno RossiMasaryk University
Pre-print
msr-2019-Data-Showcase12:13 - 12:19
Talk
Dirk BeyerLMU Munich
DOI Pre-print Media Attached
msr-2019-papers12:19 - 12:25
Short-paper
Hongyu Zhai, Casey CasalnuovoUniversity of California at Davis, USA, Prem DevanbuUniversity of California
msr-2019-papers12:25 - 12:31
Short-paper
Domenico Serra, Giovanni GranoUniversity of Zurich, Fabio Palomba, Filomena FerrucciUniversity of Salerno, Harald GallUniversity of Zurich, Alberto BacchelliUniversity of Zurich
DOI Pre-print Media Attached