scholarly journals Program Verification via Craig Interpolation for Presburger Arithmetic with Arrays

10.29007/zfkw ◽  
2018 ◽  
Author(s):  
Angelo Brillout ◽  
Daniel Kroening ◽  
Philipp Rümmer ◽  
Thomas Wahl
Keyword(s):  
Model Checking ◽  
Program Verification ◽  
Model Checker ◽  
Craig Interpolation ◽  
Presburger Arithmetic ◽  
C Programs ◽  
Full Theory ◽  
Software Model ◽  
Interpolation Procedure ◽  
Versatile Tool

Craig interpolation has become a versatile tool in formal verification, in particular for generating intermediate assertions in safety analysis and model checking. In this paper, we present a novel interpolation procedure for the theory of arrays, extending an interpolating calculus for the full theory of quantifier-free Presburger arithmetic, which will be presented at IJCAR this year. We investigate the use of this procedure in a software model checker for C programs. A distinguishing feature of the model checker is its ability to faithfully model machine arithmetic with an encoding into Presburger arithmetic with uninterpreted predicates. The interpolation procedure allows the synthesis of quantified invariants about arrays. This paper presents work in progress; we include initial experiments to demonstrate the potential of our method.

scholarly journals Gazer-Theta: LLVM-based Verifier Portfolio with BMC/CEGAR (Competition Contribution)

2021 ◽  
pp. 433-437
Author(s):  
Zsófia Ádám ◽  
Gyula Sallai ◽  
Ákos Hajdu
Keyword(s):  
Model Checking ◽  
Predicate Abstraction ◽  
Model Checker ◽  
Software Model Checking ◽  
Abstraction Refinement ◽  
Value Analysis ◽  
C Programs ◽  
Software Model

AbstractGazer-Theta is a software model checking toolchain including various analyses for state reachability. The frontend, namely Gazer, supports C programs through an LLVM-based transformation and optimization pipeline. Gazer includes an integrated bounded model checker (BMC) and can also employ the Theta backend, a generic verification framework based on abstraction-refinement (CEGAR). On SV-COMP 2021, a portfolio of BMC, explicit-value analysis, and predicate abstraction is applied sequentially in this order.

scholarly journals Craig Interpolation for the Integers: Results, Implementation, and Experiences

10.29007/9rxz ◽  
2018 ◽  
Author(s):  
Philipp Rümmer
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Safety Analysis ◽  
Craig Interpolation ◽  
Integer Arithmetic ◽  
Theorem Provers ◽  
Smt Solvers ◽  
Versatile Tool ◽  
Runtime Infrastructure

Craig interpolation is a versatile tool in formal verification, in particular for generating intermediate assertions in safety analysis and model checking. Over the last years, a variety of interpolation procedures for linear integer arithmetic (and extensions) have been developed. I will give an overview of the existing algorithms and design choices, and then discuss implementations of such procedures within theorem provers and SMT solvers. In particular, I will describe an implementation done using the multi-paradigm language Scala, which is built on top of the Java runtime infrastructure, and evaluate performance and engineering aspects.

scholarly journals Program Verification as Satisfiability Modulo Theories

10.29007/1l7f ◽  
2018 ◽  
Author(s):  
Nikolaj Bjorner ◽  
Kenneth McMillan ◽  
Andrey Rybalchenko
Keyword(s):  
Model Checking ◽  
Program Verification ◽  
Satisfiability Modulo Theories ◽  
Limited Extent ◽  
Software Model Checking ◽  
First Order ◽  
The Past ◽  
Software Model ◽  
Key Driver ◽  
Interchange Format

A key driver of SMT over the past decade has been an interchange format, SMT-LIB,and a growing set of benchmarks sharing this common format.SMT-LIB captures very well an interface that is suitablefor many tasks that reduce to solving first-order formulas modulo theories.Here we propose to extend these benefits into the domain of symbolicsoftware model checking. We make a case that SMT-LIB canbe used, and to a limited extent adapted, for exchanging symbolicsoftware model checking benchmarks. We believe this layer facilitatesdividing innovations in modeling, developing program logics and front-ends,from developing algorithms for solving constraints over recursive predicates.

scholarly journals Towards Support for Software Model Checking: Improving the Efficiency of Formal Specifications

2011 ◽  
Vol 2011 ◽  
pp. 1-13 ◽  
Author(s):  
Salamah Salamah ◽  
Ann Q. Gates ◽  
Steve Roach ◽  
Matthew Engskow
Keyword(s):  
Model Checking ◽  
Spin Model ◽  
Software Systems ◽  
Formal Specifications ◽  
Model Checker ◽  
Software Model Checking ◽  
Software Model ◽  
Property Specification ◽  
Büchi Automaton ◽  
Spin Model Checker

The Property Specification (Prospec) tool uses patterns and scopes defined by Dwyer et al., to generate formal specifications in Linear Temporal Logic (LTL) and other languages. The work presented in this paper provides improved LTL specifications for patterns and scopes over those originally provided by Prospec. This improvement comes in the efficiency of the LTL formulas as measured in terms of the number of states in the Büchi automaton generated for the formula. Minimizing the size of the Büchi automata for an LTL specification provides a significant improvement for model checking software systems using such tools as the highly acclaimed Spin model checker.

scholarly journals Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution)

2020 ◽  
pp. 378-382
Author(s):  
Hernán Ponce-de-León ◽  
Florian Furbach ◽  
Keijo Heljanko ◽  
Roland Meyer
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
Memory Models ◽  
Memory Model ◽  
Complete Analysis ◽  
Concurrent Programs ◽  
Sequential Consistency ◽  
Model Checker ◽  
Safety Properties ◽  
C Programs

Abstract Dartagnanis a bounded model checker for concurrent programs under weak memory models. What makes it different from other tools is that the memory model is not hard-coded inside Dartagnanbut taken as part of the input. For SV-COMP’20, we take as input sequential consistency (i.e. the standard interleaving memory model) extended by support for atomic blocks. Our point is to demonstrate that a universal tool can be competitive and perform well in SV-COMP. Being a bounded model checker, Dartagnan’s focus is on disproving safety properties by finding counterexample executions. For programs with bounded loops, Dartagnanperforms an iterative unwinding that results in a complete analysis. The SV-COMP’20 version of Dartagnanworks on Boogiecode. The C programs of the competition are translated internally to Boogieusing SMACK.

scholarly journals ATL Strategic Reasoning Meets Correlated Equilibrium

2017 ◽  
Author(s):  
Xiaowei Huang ◽  
Ji Ruan
Keyword(s):  
Model Checking ◽  
Correlated Equilibrium ◽  
Model Checker ◽  
Strategic Reasoning ◽  
Rational Agents ◽  
Software Model ◽  
Utilitarian Value ◽  
Total Rewards ◽  
Joint Strategy ◽  
Car Accident

This paper is motivated by analysing a Google self-driving car accident, i.e., the car hit a bus, with the framework and the tools of strategic reasoning by model checking. First of all, we find that existing ATL model checking may find a solution to the accident with {\it irrational} joint strategy of the bus and the car. This leads to a restriction of treating both the bus and the car as rational agents, by which their joint strategy is an equilibrium of certain solution concepts. Second, we find that a randomly-selected joint strategy from the set of equilibria may result in the collision of the two agents, i.e., the accident. Based on these, we suggest taking Correlated Equilibrium (CE) as agents' joint stratgey and optimising over the utilitarian value which is the expected sum of the agents' total rewards. The language ATL is extended with two new modalities to express the existence of an CE and a unique CE, respectively. We implement the extension into a software model checker and use the tool to analyse the examples in the paper. We also study the complexity of the model checking problems.

scholarly journals Program Transformation for Program Verification

10.29007/t9v2 ◽  
2018 ◽  
Author(s):  
Alberto Pettorossi ◽  
Maurizio Proietti
Keyword(s):  
Model Checking ◽  
Logic Programming ◽  
Program Transformation ◽  
Program Verification ◽  
Constraint Logic Programming ◽  
Software Model Checking ◽  
Program Specialization ◽  
Software Model

We present a transformational approach to program verification and software model checking that uses three main ingredients:(i) Constraint Logic Programming (CLP),(ii) metaprogramming and program specialization, and(iii) proof by transformation.

scholarly journals Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field Bounds

2021 ◽  
pp. 218-239
Author(s):  
Pablo Ponzio ◽  
Ariel Godio ◽  
Nicolás Rosner ◽  
Marcelo Arroyo ◽  
Nazareno Aguirre ◽  
...  
Keyword(s):  
Model Checking ◽  
Data Structures ◽  
Efficient Algorithm ◽  
Bounded Model Checking ◽  
Model Checker ◽  
Data Types ◽  
Dynamic Data Structures ◽  
Dynamic Data ◽  
Software Model ◽  
Improve Model

AbstractSoftware model checkers are able to exhaustively explore different bounded program executions arising from various sources of non-determinism. These tools provide statements to produce non-deterministic values for certain variables, thus forcing the corresponding model checker to consider all possible values for these during verification. While these statements offer an effective way of verifying programs handling basic data types and simple structured types, they are inappropriate as a mechanism for nondeterministic generation of pointers, favoring the use of insertion routines to produce dynamic data structures when verifying, via model checking, programs handling such data types.We present a technique to improve model checking of programs handling heap-allocated data types, by taming the explosion of candidate structures that can be built when non-deterministically initializing heap object fields. The technique exploits precomputed relational bounds, that disregard values deemed invalid by the structure’s type invariant, thus reducing the state space to be explored by the model checker. Precomputing the relational bounds is a challenging costly task too, for which we also present an efficient algorithm, based on incremental SAT solving.We implement our approach on top of the bounded model checker, and show that, for a number of data structures implementations, we can handle significantly larger input structures and detect faults that is unable to detect.

scholarly journals Interpolation and Model Checking for Nonlinear Arithmetic

2021 ◽  
pp. 266-288
Author(s):  
Dejan Jovanović ◽  
Bruno Dutertre
Keyword(s):  
Model Checking ◽  
Satisfiability Modulo Theories ◽  
Full Model ◽  
Model Checker ◽  
New Model ◽  
Smt Solver ◽  
Partial Model ◽  
Interpolation Procedure ◽  
State Of Art ◽  
Nonlinear Arithmetic

AbstractWe present a new model-based interpolation procedure for satisfiability modulo theories (SMT). The procedure uses a new mode of interaction with the SMT solver that we call solving modulo a model. This either extends a given partial model into a full model for a set of assertions or returns an explanation (a model interpolant) when no solution exists. This mode of interaction fits well into the model-constructing satisfiability (MCSAT) framework of SMT. We use it to develop an interpolation procedure for any MCSAT-supported theory. In particular, this method leads to an effective interpolation procedure for nonlinear real arithmetic. We evaluate the new procedure by integrating it into a model checker and comparing it with state-of-art model-checking tools for nonlinear arithmetic.

Sign in / Sign up

Export Citation Format

Share Document