Date: Tuesday 20 March 2018
Time: 11:30 - 13:00
Location / Room: Konf. 2
Chair:
Armin Biere, JKU Linz, AT
Co-Chair:
Daniel Große, University Bremen, DE
The session consists of four papers on model checking. It ranges from model checking of multiple properties, improving bit-level model checking, checking specific properties in processor design to software model checking of the Linux kernel.
| Time | Label | Presentation Title Authors |
|---|---|---|
| 11:30 | 2.4.1 | (Best Paper Award Candidate) EFFICIENT VERIFICATION OF MULTI-PROPERTY DESIGNS (THE BENEFIT OF WRONG ASSUMPTIONS) Speaker: Eugene Goldberg, Diffblue, US Authors: Eugene Goldberg1, Matthias Gudemann2, Daniel Kroening3 and Rajdeep Mukherjee4 1DiffBlue, US; 2DiffBlue, DE; 3DiffBlue, GB; 4Oxford University, GB Abstract We consider the problem of efficiently checking a set of safety properties P1,...,Pk of one design. We introduce a new approach called Ja-verification, where Ja stands for ``Just-Assume'' (as opposed to ``assume-guarantee''). In this approach, when proving a property Pi, one assumes that every property Pj for j != i holds. The process of proving properties either results in showing that P1,...,Pk hold without any assumptions or finding a ``debugging set'' of properties. The latter identifies a subset of failed properties that are the first to break. The design behaviors that cause the properties in the debugging set to fail must be fixed first. Importantly, in our approach, there is no need to prove the assumptions used. We describe the theory behind our approach and report experimental results that demonstrate substantial gains in performance, especially in the cases where a small debugging set exists. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 12:00 | 2.4.2 | COMBINING PDR AND REVERSE PDR FOR HARDWARE MODEL CHECKING Speaker: Tobias Seufert, University of Freiburg, DE Authors: Tobias Seufert and Christoph Scholl, University Freiburg, DE Abstract In the last few years IC3 resp. PDR attracted a lot of attention as a SAT-based hardware verification approach without needing to unroll the transition relation as in Bounded Model Checking (BMC). Motivated by different strengths of forward and backward traversal already observed in BDD based model checking and by an exponential complexity gap between original PDR and its reverted counterpart 'Reverse PDR' (which starts its analysis with the initial states instead of the unsafe states as in the original PDR), we take a closer look at Reverse PDR and we present a combined forward/backward version of PDR that inherits the advantages of both original and Reverse PDR. Our experimental results on benchmarks from the Hardware Model Checking Competition demonstrate clear benefits of the combined approach. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 12:30 | 2.4.3 | SYMBOLIC QUICK ERROR DETECTION USING SYMBOLIC INITIAL STATE FOR PRE-SILICON VERIFICATION Speaker: Mohammad Rahmani Fadiheh, University of Kaiserslautern, DE Authors: Mohammad Rahmani Fadiheh1, Joakim Urdahl1, Srinivasa Shashank Nuthakki2, Subhasish Mitra2, Dominik Stoffel1 and Wolfgang Kunz1 1University of Kaiserslautern, DE; 2Stanford University, US Abstract Driven by the demand for highly customizable processor cores for IoT and related applications, there is a renewed interest in effective but low-cost techniques for verifying systems-on-chip (SoCs). This paper revisits the problem of processor verification and presents a radically different approach when compared to the state of the art. The proposed approach is highly automated and leverages recent progress in the field of post-silicon validation by the method of Quick Error Detection (QED) and Symbolic Quick Error Detection (SQED). In this paper, we modify SQED by incorporating a symbolic initial state in its BMC-based analysis and generalize the approach into the S2QED method. As a first advantage, S2QED can separate logic bugs from electrical bugs in QED-based post-silicon validation. Secondly, it also makes a strong contribution to pre-silicon verification by proving that the execution of each instruction is independent of its context in the program. The manual efforts for the proposed approach are orders of magnitude smaller than for conventional property checking. Our experimental results demonstrate the potential of S2QED using the Aquarius open-source processor example. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 12:45 | 2.4.4 | VERIFICATION OF TREE-BASED HIERARCHICAL READ-COPY UPDATE IN THE LINUX KERNEL Speaker: Paul McKenney, IBM Linux Technology Center, US Authors: Lihao Liang1, Paul McKenney2, Daniel Kroening1 and Tom Melham1 1University of Oxford, GB; 2IBM Linux Technology Center, US Abstract Read-Copy Update (RCU) is a scalable, high-performance Linux-kernel synchronization mechanism that runs low-overhead readers concurrently with updaters. Production-quality RCU implementations are decidedly non-trivial and their stringent validation is mandatory. This suggests use of formal verification. Previous formal verification efforts for RCU either focus on simple implementations or use modeling languages. In this paper, we construct a model directly from the source code of Tree RCU in the Linux kernel, and use the CBMC program analyzer to verify its safety and liveness properties. To the best of our knowledge, this is the first verification of a significant part of RCU's source code—an important step towards integration of formal verification into the Linux kernel's regression test suite. Download Paper (PDF; Only available from the DATE venue WiFi) |
| 13:00 | End of session Lunch Break in Großer Saal and Saal 1
On all conference days (Tuesday to Thursday), coffee and tea will be served during the coffee breaks at the below-mentioned times in the exhibition area (Terrace Level of the ICCD). Lunch Breaks (Großer Saal + Saal 1)On all conference days (Tuesday to Thursday), a seated lunch (lunch buffet) will be offered in the rooms "Großer Saal" and "Saal 1" (Saal Level of the ICCD) to fully registered conference delegates only. There will be badge control at the entrance to the lunch break area. Tuesday, March 20, 2018
Wednesday, March 21, 2018
Thursday, March 22, 2018
|