The goal of this work is to improve the efficiency of bounded model checkers that are modular in the memory model.
Our first contribution is a static analysis for the given memory model that is performed as a preprocessing step and helps us significantly reduce the encoding size.
Memory model make use of relations to judge whether an execution is consistent. The analysis computes bounds on these relations: which pairs of events may or must be related.
What is new is that the bounds are relativized to the execution of events.
This makes it possible to derive, for the first time, not only upper but also meaningful lower bounds.
Another important feature is that the analysis can import information about the verification instance from external sources to improve its precision.
Our second contribution are new optimizations for the SMT encoding.
Notably, the lower bounds allow us to simplify the encoding of acyclicity constraints.
We implemented our analysis and optimizations within a bounded model checker and evaluated it on challenging benchmarks.
The evaluation shows up-to 40% reduction in verification time (including the analysis) over previous encodings.
Our optimizations allow us to efficiently check safety, liveness, and data race freedom in Linux kernel code.
Thu 26 OctDisplayed time zone: Lisbon change
14:00 - 15:30
|The Bounded Pathwidth of Control-Flow Graphs
Giovanna Kobus Conrado Hong Kong University of Science and Technology, Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Chun Kit Lam Hong Kong University of Science and TechnologyDOI
|How Profilers Can Help Navigate Type Migration
Ben Greenman University of Utah, Matthias Felleisen Northeastern University, Christos Dimoulas Northwestern UniversityDOI
|Synthesizing Precise Static Analyzers for Automatic Differentiation
Jacob Laurel University of Illinois at Urbana-Champaign, Siyuan Brant Qian University of Illinois at Urbana-Champaign; Zhejiang University, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research, Sasa Misailovic University of Illinois at Urbana-ChampaignDOI
|A Container-Usage-Pattern-Based Context Debloating Approach for Object-Sensitive Pointer Analysis
Dongjie He UNSW, Yujiang Gui UNSW, Wei Li UNSW, Yonggang Tao UNSW, Changwei Zou UNSW, Yulei Sui UNSW, Jingling Xue UNSWDOI Pre-print
|Static Analysis of Memory Models for SMT Encodings
Thomas Haas TU Braunschweig, René Maseli TU Braunschweig, Roland Meyer TU Braunschweig, Hernán Ponce de León HuaweiDOI