Write a Blog >>
VMCAI 2017
Sun 15 - Tue 17 January 2017
co-located with POPL 2017
Mon 16 Jan 2017 14:00 - 14:30 at Amphitheater 44 - Model-checking and bug finding Chair(s): Andreas Podelski

Software projects tend to suffer from conceptually simple resource manipulation bugs, such as accessing a de-allocated memory region, or acquiring a non-reentrant lock twice. Static code scanners are used extensively to remove these bugs from projects like the Linux kernel. Yet, when the manipulation of the resource spans multiple functions, efficiently finding these bugs is a challenge. We present a shape-and-effect inference system for C, that enables efficient and scalable inter-procedural reasoning about resource manipulation. The inference system is used to build a program abstraction: a control-flow graph decorated with alias relationships and observable effects. Bugs are found by model checking this control-flow graph, matching undesirable sequences of operations. We evaluate a prototype implementation of our approach (EBA) and run it on a collection of historical double-lock bugs from the Linux kernel. Our results show that our tool is more effective at finding bugs than similar code-scanning tools. EBA analyzes the drivers/ directory of Linux (nine thousand files) in less than thirty minutes, and uncovers a handful previously unknown double-lock bugs in various drivers.

Mon 16 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 15:30
Model-checking and bug findingVMCAI at Amphitheater 44
Chair(s): Andreas Podelski University of Freiburg, Germany
Effective Bug Finding in C Programs with Shape and Effect Abstraction
Iago Abal IT University of Copenhagen, Claus Brabrand IT University of Copenhagen, Denmark, Andrzej Wąsowski IT University of Copenhagen, Denmark
Reduction of Workflow Nets for Generalised Soundness Verification
Hadrien Bride Femto-ST / Université de Franche-Comté, Olga Kouchnarenko Femto-ST / Université de Franche-Comté, Fabien Peureux Femto-ST / Université de Franche-Comté + Smartesting S&S
Media Attached
Dynamic Reductions for Model Checking Concurrent Software.
Henning Günther Technische Universität Wien, Alfons Laarman Vienna University of Technology, Ana Sokolova University of Salzburg, Georg Weissenbacher Technische Universität Wien
File Attached