A Recursive Shortcut for CEGAR: Application To The Modal Logic K Satisfiability Problem

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence ◽

10.24963/ijcai.2017/94 ◽

2017 ◽

Cited By ~ 3

Author(s):

Jean-Marie Lagniez ◽

Daniel Le Berre ◽

Tiago de Lima ◽

Valentin Montmirail

Keyword(s):

Model Checking ◽

Modal Logic ◽

State Of The Art ◽

The State ◽

Satisfiability Problem ◽

Abstraction Refinement ◽

Counter Example ◽

Complete Problems ◽

Large Systems ◽

Specific Implementation

Counter-Example-Guided Abstraction Refinement (CEGAR) has been very successful in model checking large systems. Since then, it has been applied to many different problems. It especially proved to be an highly successful practical approach for solving the PSPACE complete QBF problem. In this paper, we propose a new CEGAR-like approach for tackling PSPACE complete problems that we call RECAR (Recursive Explore and Check Abstraction Refinement). We show that this generic approach is sound and complete. Then we propose a specific implementation of the RECAR approach to solve the modal logic K satisfiability problem. We implemented both a CEGAR and a RECAR approach for the modal logic K satisfiability problem within the solver MoSaiC. We compared experimentally those approaches to the state-of-the-art solvers for that problem. The RECAR approach outperforms the CEGAR one for that problem and also compares favorably against the state-of-the-art on the benchmarks considered.

Download Full-text

Property Directed Reachability for Automated Planning

Journal of Artificial Intelligence Research ◽

10.1613/jair.4231 ◽

2014 ◽

Vol 50 ◽

pp. 265-319 ◽

Cited By ~ 5

Author(s):

M. Suda

Keyword(s):

Model Checking ◽

State Of The Art ◽

Automated Planning ◽

The State ◽

Experimental Comparison ◽

Specific Procedure ◽

Transition Systems ◽

Planning Algorithm ◽

Sat Solver ◽

Recent Method

Property Directed Reachability (PDR) is a very promising recent method for deciding reachability in symbolically represented transition systems. While originally conceived as a model checking algorithm for hardware circuits, it has already been successfully applied in several other areas. This paper is the first investigation of PDR from the perspective of automated planning. Similarly to the planning as satisfiability paradigm, PDR draws its strength from internally employing an efficient SAT-solver. We show that most standard encoding schemes of planning into SAT can be directly used to turn PDR into a planning algorithm. As a non-obvious alternative, we propose to replace the SAT-solver inside PDR by a planning-specific procedure implementing the same interface. This SAT-solver free variant is not only more efficient, but offers additional insights and opportunities for further improvements. An experimental comparison to the state of the art planners finds it highly competitive, solving most problems on several domains.

Download Full-text

Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays

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

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

2021 ◽

pp. 113-132

Author(s):

Makai Mann ◽

Ahmed Irfan ◽

Alberto Griggio ◽

Oded Padon ◽

Clark Barrett

Keyword(s):

Model Checking ◽

State Of The Art ◽

Inductive Reasoning ◽

Auxiliary Variables ◽

Abstraction Refinement ◽

Free Induction ◽

Induction Proofs ◽

Infinite State Systems ◽

Infinite State

AbstractWe develop a framework for model checking infinite-state systems by automatically augmenting them with auxiliary variables, enabling quantifier-free induction proofs for systems that would otherwise require quantified invariants. We combine this mechanism with a counterexample-guided abstraction refinement scheme for the theory of arrays. Our framework can thus, in many cases, reduce inductive reasoning with quantifiers and arrays to quantifier-free and array-free reasoning. We evaluate the approach on a wide set of benchmarks from the literature. The results show that our implementation often outperforms state-of-the-art tools, demonstrating its practical potential.

Download Full-text

LLMC: Verifying High-Performance Software

Computer Aided Verification - Lecture Notes in Computer Science ◽

10.1007/978-3-030-81688-9_32 ◽

2021 ◽

pp. 690-703

Author(s):

Freark I. van der Berg

Keyword(s):

Model Checking ◽

Data Structures ◽

High Performance ◽

State Of The Art ◽

The State ◽

State Model ◽

Test Suite ◽

Model Checker ◽

Unit Tests

AbstractMulti-threaded unit tests for high-performance thread-safe data structures typically do not test all behaviour, because only a single scheduling of threads is witnessed per invocation of the unit tests. Model checking such unit tests allows to verify all interleavings of threads. These tests could be written in or compiled to LLVM IR. Existing LLVM IR model checkers like divine and Nidhugg, use an LLVM IR interpreter to determine the next state. This paper introduces llmc, a multi-core explicit-state model checker of multi-threaded LLVM IR that translates LLVM IR to LLVM IR that is executed instead of interpreted. A test suite of 24 tests, stressing data structures, shows that on average llmc clearly outperforms the state-of-the-art tools divine and Nidhugg.

Download Full-text

Efficient Strategies for CEGAR-Based Model Checking

Journal of Automated Reasoning ◽

10.1007/s10817-019-09535-x ◽

2019 ◽

Vol 64 (6) ◽

pp. 1051-1091

Author(s):

Ákos Hajdu ◽

Zoltán Micskei

Keyword(s):

Model Checking ◽

Formal Verification ◽

State Of The Art ◽

Abstraction Refinement ◽

Remarkable Improvement ◽

Research Questions ◽

Effectiveness And Efficiency ◽

Efficient Verification ◽

New Strategies

Abstract Automated formal verification is often based on the Counterexample-Guided Abstraction Refinement (CEGAR) approach. Many variants of CEGAR have been developed over the years as different problem domains usually require different strategies for efficient verification. This has lead to generic and configurable CEGAR frameworks, which can incorporate various algorithms. In our paper we propose six novel improvements to different aspects of the CEGAR approach, including both abstraction and refinement. We implement our new contributions in the Theta framework allowing us to compare them with state-of-the-art algorithms. We conduct an experiment on a diverse set of models to address research questions related to the effectiveness and efficiency of our new strategies. Results show that our new contributions perform well in general. Moreover, we highlight certain cases where performance could not be increased or where a remarkable improvement is achieved.

Download Full-text

A Formal Approach to Verify Parameterized Protocols in Mobile Cyber-Physical Systems

Mobile Information Systems ◽

10.1155/2017/5731678 ◽

2017 ◽

Vol 2017 ◽

pp. 1-10 ◽

Cited By ~ 3

Author(s):

Long Zhang ◽

Wenyan Hu ◽

Wanxia Qu ◽

Yang Guo ◽

Sikun Li

Keyword(s):

Model Checking ◽

Petri Net ◽

State Of The Art ◽

Cyber Physical Systems ◽

The State ◽

Safety Properties ◽

Memory Consumption ◽

Formal Approach ◽

New Approach ◽

Physical Systems

Mobile cyber-physical systems (CPSs) are very hard to verify, because of asynchronous communication and the arbitrary number of components. Verification via model checking typically becomes impracticable due to the state space explosion caused by the system parameters and concurrency. In this paper, we propose a formal approach to verify the safety properties of parameterized protocols in mobile CPS. By using counter abstraction, the protocol is modeled as a Petri net. Then, a novel algorithm, which uses IC3 (the state-of-the-art model checking algorithm) as the back-end engine, is presented to verify the Petri net model. The experimental results show that our new approach can greatly scale the verification capabilities compared favorably against several recently published approaches. In addition to solving the instances fast, our method is significant for its lower memory consumption.

Download Full-text

Practical Picture Processing

Proceedings, annual meeting, Electron Microscopy Society of America ◽

10.1017/s0424820100051700 ◽

1974 ◽

Vol 32 ◽

pp. 338-339

Author(s):

T. A. Welton

Keyword(s):

Radiation Damage ◽

Coherence Length ◽

Spatial Information ◽

State Of The Art ◽

Coherent Radiation ◽

The State ◽

Energy Spread ◽

Electron Micrograph ◽

Picture Processing ◽

Molecular Skeleton

Various authors have emphasized the spatial information resident in an electron micrograph taken with adequately coherent radiation. In view of the completion of at least one such instrument, this opportunity is taken to summarize the state of the art of processing such micrographs. We use the usual symbols for the aberration coefficients, and supplement these with £ and 6 for the transverse coherence length and the fractional energy spread respectively. He also assume a weak, biologically interesting sample, with principal interest lying in the molecular skeleton remaining after obvious hydrogen loss and other radiation damage has occurred.

Download Full-text