Cooperative Bounded Model Checking Using STE and Hybrid Three-Valued SAT Solving

The cost of LTL model checking is highly sensitive to the length of the formula under verification. We observe that, under some specific conditions, the input LTL formula can be reduced to an easier-to-handle one before model checking. In such reduction, these two formulae need not to be logically equivalent, but they share the same counterexample set w.r.t the model. In the case that the model is symbolically represented, the condition enabling such reduction can be detected with a lightweight effort (e.g., with SAT-solving). In this paper, we tentatively name such technique “counterexample-preserving reduction” (CePRe, for short), and the proposed technique is evaluated by conducting comparative experiments of BDD-based model checking, bounded model checking, and property directed reachability-(IC3) based model checking.

Download Full-text

Tuning Parallel SAT Solvers

10.29007/z3g2 ◽

2019 ◽

Author(s):

Thorsten Ehlers ◽

Dirk Nowotka

Keyword(s):

Model Checking ◽

Database Management ◽

Bounded Model Checking ◽

Experimental Results ◽

Massively Parallel ◽

Sat Solving ◽

Sat Solvers ◽

Sat Solver ◽

The Impact

In this paper we present new implementation details and benchmarking results for our parallel portfolio solver TopoSAT2. In particular, we discuss ideas and implementation details for the exchange of learned clauses in a massively-parallel SAT solver which is designed to run more that 1, 000 solver threads in parallel. Furthermore, we go back to the roots of portfolio SAT solving, and discuss the impact of diversifying the solver by using different restart- , branching- and clause database management heuristics. We show that these techniques can be used to tune the solver towards different problems. However, in a case study on formulas derived from Bounded Model Checking problems we see the best performance when using a rather simple clause exchange strategy. We show details of these tests and discuss possible explanations for this phenomenon.As computing times on massively-parallel clusters are expensive, we consider it especially interesting to share these kind of experimental results.

Download Full-text

Bounded Model Checking for Hyperproperties

Tools and Algorithms for the Construction and Analysis of Systems - Lecture Notes in Computer Science ◽

10.1007/978-3-030-72016-2_6 ◽

2021 ◽

pp. 94-112

Author(s):

Tzu-Han Hsu ◽

César Sánchez ◽

Borzoo Bonakdarpour

Keyword(s):

Model Checking ◽

Path Planning ◽

Case Studies ◽

Data Structures ◽

Mutation Testing ◽

Bounded Model Checking ◽

Sat Solving ◽

Concurrent Data Structures ◽

Simultaneous Quantification

AbstractThis paper introduces a bounded model checking (BMC) algorithm for hyperproperties expressed in HyperLTL, which — to the best of our knowledge — is the first such algorithm. Just as the classic BMC technique for LTL primarily aims at finding bugs, our approach also targets identifying counterexamples. BMC for LTL is reduced to SAT solving, because LTL describes a property via inspecting individual traces. Our BMC approach naturally reduces to QBF solving, as HyperLTL allows explicit and simultaneous quantification over multiple traces. We report on successful and efficient model checking, implemented in our tool called , of a rich set of experiments on a variety of case studies, including security, concurrent data structures, path planning for robots, and mutation testing.

Download Full-text

Parallel SAT Solving in Bounded Model Checking

Formal Methods: Applications and Technology - Lecture Notes in Computer Science ◽

10.1007/978-3-540-70952-7_21 ◽

2007 ◽

pp. 301-315 ◽

Cited By ~ 5

Author(s):

Erika Ábrahám ◽

Tobias Schubert ◽

Bernd Becker ◽

Martin Fränzle ◽

Christian Herde

Keyword(s):

Model Checking ◽

Bounded Model Checking ◽

Sat Solving

Download Full-text

Finding More Property Violations in Model Checking via the Restart Policy

Electronics ◽

10.3390/electronics10232957 ◽

2021 ◽

Vol 10 (23) ◽

pp. 2957

Author(s):

Mengtao Geng ◽

Xiaoyu Zhang ◽

Jianwen Li

Keyword(s):

Model Checking ◽

State Of The Art ◽

Wide Spectrum ◽

Current Model ◽

Bounded Model Checking ◽

Search Problem ◽

Sat Solving ◽

Car Model ◽

Bug Finding ◽

Incremental Construction

Model checking is an efficient formal verification technique that has been applied to a wide spectrum of applications in software engineering. Popular model checking algorithms include Bounded Model Checking (BMC) and Incremental Construction of Inductive Clauses for Indubitable Correctness/Property Directed Reachability(IC3/PDR). The recently proposed Complementary Approximate Reachability (CAR) model checking algorithm has a performance close to BMC in bug-finding, while its depth-first strategy sometimes leads the algorithm to a trap, which will waste lots of computation. In this paper, we enhance the recently proposed Complementary Approximate Reachability (CAR) model checking algorithm by integrating the restart policy, which yields a restartable CAR model (abbreviated as r-CAR). The restart policy can help avoid the trap problem caused by the depth-first strategy and has played an important role in modern SAT-solving algorithms to search for a satisfactory solution. As the bug-finding in model checking is reducible to a similar search problem, the restart policy can be useful to enhance the bug-finding capability. We made an extensive experiment to evaluate the new algorithm. Our results show that out of the 749 industrial instances, r-CAR is able to find 13 instances that the state-of-the-art BMC technique cannot find and can solve more than 11 instances than the original CAR. The new algorithm successfully contributes to the current model-checking portfolio in practice.

Download Full-text