2.4 Model Checking

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 Goldberg¹, Matthias Gudemann², Daniel Kroening³ and Rajdeep Mukherjee⁴ ¹DiffBlue, US; ²DiffBlue, DE; ³DiffBlue, GB; ⁴Oxford 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 Fadiheh¹, Joakim Urdahl¹, Srinivasa Shashank Nuthakki², Subhasish Mitra², Dominik Stoffel¹ and Wolfgang Kunz¹ ¹University of Kaiserslautern, DE; ²Stanford 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 Liang¹, Paul McKenney², Daniel Kroening¹ and Tom Melham¹ ¹University of Oxford, GB; ²IBM 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 Coffee Breaks in the Exhibition Area 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 Coffee Break 10:30 - 11:30 Lunch Break 13:00 - 14:30 Awards Presentation and Keynote Lecture in "Saal 2" 13:50 - 14:20 Coffee Break 16:00 - 17:00 Wednesday, March 21, 2018 Coffee Break 10:00 - 11:00 Lunch Break 12:30 - 14:30 Awards Presentation and Keynote Lecture in "Saal 2" 13:30 - 14:20 Coffee Break 16:00 - 17:00 Thursday, March 22, 2018 Coffee Break 10:00 - 11:00 Lunch Break 12:30 - 14:00 Keynote Lecture in "Saal 2" 13:20 - 13:50 Coffee Break 15:30 - 16:00

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 Goldberg¹, Matthias Gudemann², Daniel Kroening³ and Rajdeep Mukherjee⁴
¹DiffBlue, US; ²DiffBlue, DE; ³DiffBlue, GB; ⁴Oxford 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 Fadiheh¹, Joakim Urdahl¹, Srinivasa Shashank Nuthakki², Subhasish Mitra², Dominik Stoffel¹ and Wolfgang Kunz¹
¹University of Kaiserslautern, DE; ²Stanford 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 Liang¹, Paul McKenney², Daniel Kroening¹ and Tom Melham¹
¹University of Oxford, GB; ²IBM 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

Coffee Breaks in the Exhibition Area

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