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

Displayed time zone: Eastern Time (US & Canada) change

11:55 - 12:30
Session IV: Defect Prediction and Testing (Part 2)MSR 2019 Technical Papers / MSR 2019 Data Showcase at Centre-Ville
Chair(s): Jesus M. Gonzalez-Barahona Universidad Rey Juan Carlos
11:55
6m
Talk
A Dataset of Non-Functional Bugs
MSR 2019 Data Showcase
Aida Radu , Sarah Nadi University of Alberta
Pre-print
12:01
6m
Short-paper
Does UML Modeling Associate with Higher Software Quality in Open-Source Software?
MSR 2019 Technical Papers
Adithya Raghuraman , Truong Ho-Quang , Michel Chaudron Chalmers University of Technology, Alexander Serebrenik Eindhoven University of Technology, Bogdan Vasilescu Carnegie Mellon University
Pre-print
12:07
6m
Short-paper
STRAIT: A Tool for Automated Software Reliability Growth Analysis
MSR 2019 Technical Papers
Stanislav Chren Masaryk University, Radoslav Micko , Barbora Buhnova Masaryk University, Bruno Rossi Masaryk University
Pre-print
12:13
6m
Talk
A Data Set of Program Invariants and Error Paths
MSR 2019 Data Showcase
Dirk Beyer LMU Munich
DOI Pre-print Media Attached
12:19
6m
Short-paper
Test Coverage in Python Programs
MSR 2019 Technical Papers
Hongyu Zhai , Casey Casalnuovo University of California at Davis, USA, Prem Devanbu University of California
12:25
6m
Short-paper
On the Effectiveness of Manual and Automatic Unit Test Generation: Ten Years Later
MSR 2019 Technical Papers
Domenico Serra , Giovanni Grano University of Zurich, Fabio Palomba , Filomena Ferrucci University of Salerno, Harald Gall University of Zurich, Alberto Bacchelli University of Zurich
DOI Pre-print Media Attached