Finding More Property Violations in Model Checking via the Restart Policy

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

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

2006 10th International Conference on Computer Supported Cooperative Work in Design ◽

10.1109/cscwd.2006.253184 ◽

2006 ◽

Cited By ~ 1

Author(s):

Shujun Deng ◽

Weimin Wu ◽

Jinian Bian

Keyword(s):

Model Checking ◽

Bounded Model Checking ◽

Sat Solving

Download Full-text

Bounded Model Checking Combining Symbolic Trajectory Evaluation Abstraction with Hybrid Three-Valued SAT Solving

Computer Supported Cooperative Work in Design III - Lecture Notes in Computer Science ◽

10.1007/978-3-540-72863-4_31 ◽

2007 ◽

pp. 297-307

Author(s):

Shujun Deng ◽

Weimin Wu ◽

Jinian Bian

Keyword(s):

Model Checking ◽

Bounded Model Checking ◽

Sat Solving ◽

Symbolic Trajectory Evaluation ◽

Symbolic Trajectory

Download Full-text

Counterexample-Preserving Reduction for Symbolic Model Checking

Journal of Applied Mathematics ◽

10.1155/2014/702165 ◽

2014 ◽

Vol 2014 ◽

pp. 1-13 ◽

Cited By ~ 1

Author(s):

Wanwei Liu ◽

Rui Wang ◽

Xianjin Fu ◽

Ji Wang ◽

Wei Dong ◽

...

Keyword(s):

Model Checking ◽

Bounded Model Checking ◽

Symbolic Model Checking ◽

Sat Solving ◽

Symbolic Model ◽

Highly Sensitive ◽

The Cost ◽

Ltl Model Checking

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

Model-Checking Speculation-Dependent Security Properties: Abstracting and Reducing Processor Models for Sound and Complete Verification

Electronics ◽

10.3390/electronics8091057 ◽

2019 ◽

Vol 8 (9) ◽

pp. 1057

Author(s):

Gianpiero Cabodi ◽

Paolo Camurati ◽

Fabrizio Finocchiaro ◽

Danilo Vendraminetto

Keyword(s):

Model Checking ◽

Formal Verification ◽

High Performance ◽

State Of The Art ◽

Realistic Model ◽

Bounded Model Checking ◽

Sensitive Information ◽

Model Checker ◽

Verification Process ◽

Verification Techniques

Spectre and Meltdown attacks in modern microprocessors represent a new class of attacks that have been difficult to deal with. They underline vulnerabilities in hardware design that have been going unnoticed for years. This shows the weakness of the state-of-the-art verification process and design practices. These attacks are OS-independent, and they do not exploit any software vulnerabilities. Moreover, they violate all security assumptions ensured by standard security procedures, (e.g., address space isolation), and, as a result, every security mechanism built upon these guarantees. These vulnerabilities allow the attacker to retrieve leaked data without accessing the secret directly. Indeed, they make use of covert channels, which are mechanisms of hidden communication that convey sensitive information without any visible information flow between the malicious party and the victim. The root cause of this type of side-channel attacks lies within the speculative and out-of-order execution of modern high-performance microarchitectures. Since modern processors are hard to verify with standard formal verification techniques, we present a methodology that shows how to transform a realistic model of a speculative and out-of-order processor into an abstract one. Following related formal verification approaches, we simplify the model under consideration by abstraction and refinement steps. We also present an approach to formally verify the abstract model using a standard model checker. The theoretical flow, reliant on established formal verification results, is introduced and a sketch of proof is provided for soundness and correctness. Finally, we demonstrate the feasibility of our approach, by applying it on a pipelined DLX RISC-inspired processor architecture. We show preliminary experimental results to support our claim, performing Bounded Model-Checking with a state-of-the-art model checker.

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

Concurrent Bug Finding Based on Bounded Model Checking

International Journal of Software Engineering and Knowledge Engineering ◽

10.1142/s0218194020500242 ◽

2020 ◽

Vol 30 (05) ◽

pp. 669-694

Author(s):

Milena Vujošević Janičić

Keyword(s):

Model Checking ◽

Software Verification ◽

Symbolic Execution ◽

Bounded Model Checking ◽

Sequential Approach ◽

Software Analysis ◽

Verification Tool ◽

Single Compound ◽

Bug Finding ◽

Reliable Software

Automated and reliable software verification is of crucial importance for development of high-quality software. Formal methods can be used for finding different kinds of bugs without executing the software, for example, for finding possible run-time errors. The methods like model checking and symbolic execution offer very precise static analysis but on real world programs do not always scale well. One way to tackle the scalability problem is to apply new concurrent and sequential approaches to complex algorithms used in these kinds of software analysis. In this paper, we compare different variants of bounded model checking and propose two concurrent approaches: concurrency of intra-procedural analysis and concurrency of inter-procedural analysis. We implemented these approaches in a software verification tool LAV, a tool that is based on bounded model checking and symbolic execution. For assessing the improvements gained, we experimentally compared the concurrent approaches with the standard bounded model checking approach (where all correctness conditions are put into a single compound formula) and with a sequential approach (where correctness conditions are checked separately, one after the other). The results show that, in many cases, the proposed concurrent approaches give significant improvements.

Download Full-text