arXiv subjects

Arie Gurfinkel

Publications and source records attributed to Arie Gurfinkel.

27 records · Page 2Linked to original sources

arXiv2019

Local Reasoning for Parameterized First Order Protocols

First Order Logic (FOL) is a powerful reasoning tool for program verification. Recent work on Ivy shows that FOL is well suited for verification of parameterized distributed systems. However, specifying many natural objects, such as a ring topology, in FOL is unexpectedly inconvenient. We present a framework based on FOL for specifying distributed multi-process protocols in a process-local manner together with an implicit network topology. In the specification framework, we provide an auto-active analysis technique to reason about the protocols locally, in a process-modular way. Our goal is to mirror the way designers often describe and reason about protocols. By hiding the topology behind the FOL structure, we simplify the modelling, but complicate the reasoning. To deal with that, we use an oracle for the topology to develop a sound and relatively complete proof rule that reduces reasoning about the implicit topology back to pure FOL. This completely avoids the need to axiomatize the topology. Using the rule, we establish a property that reduces verification to a fixed number of processes bounded by the size of local neighbourhoods. We show how to use the framework on two examples, including leader election on a ring.

cs.LO↗

arXiv2018

Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts

Automated synthesis of reactive systems from specifications has been a topic of research for decades. Recently, a variety of approaches have been proposed to extend synthesis of reactive systems from proposi- tional specifications towards specifications over rich theories. We propose a novel, completely automated approach to program synthesis which reduces the problem to deciding the validity of a set of forall-exists formulas. In spirit of IC3 / PDR, our problem space is recursively refined by blocking out regions of unsafe states, aiming to discover a fixpoint that describes safe reactions. If such a fixpoint is found, we construct a witness that is directly translated into an implementation. We implemented the algorithm on top of the JKind model checker, and exercised it against contracts written using the Lustre specification language. Experimental results show how the new algorithm outperforms JKinds already existing synthesis procedure based on k-induction and addresses soundness issues in the k-inductive approach with respect to unrealizable results.

cs.SE↗

arXiv2017

Synthesis from Assume-Guarantee Contracts using Skolemized Proofs of Realizability

The realizability problem in requirements engineering is to determine the existence of an implementation that meets the given formal requirements. A step forward after realizability is proven, is to construct such an implementation automatically, and thus solve the problem of program synthesis. In this paper, we propose a novel approach to pro- gram synthesis guided by k-inductive proofs of realizability of assume- guarantee contracts constructed from safety properties. The proof of re- alizability is performed over a set of forall-exists formulas, and synthesis is per- formed by extracting Skolem functions witnessing the existential quan- tification. These Skolem functions can then be combined into an imple- mentation. Our approach is implemented in the JSyn tool which con- structs Skolem functions from a contract written in a variant of the Lus- tre programming language and then compiles the Skolem functions into a C language implementation. For a variety of benchmark models that already contained hand-written implementations, we are able to identify the usability and effectiveness of the synthesized counterparts, assuming a component-based verification framework.

cs.SE↗

arXiv2015

Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays

We present a compositional SMT-based algorithm for safety of procedural C programs that takes the heap into consideration as well. Existing SMT-based approaches are either largely restricted to handling linear arithmetic operations and properties, or are non-compositional. We use Constrained Horn Clauses (CHCs) to represent the verification conditions where the memory operations are modeled using the extensional theory of arrays (ARR). First, we describe an exponential time quantifier elimination (QE) algorithm for ARR which can introduce new quantifiers of the index and value sorts. Second, we adapt the QE algorithm to efficiently obtain under-approximations using models, resulting in a polynomial time Model Based Projection (MBP) algorithm. Third, we integrate the MBP algorithm into the framework of compositional reasoning of procedural programs using may and must summaries recently proposed by us. Our solutions to the CHCs are currently restricted to quantifier-free formulas. Finally, we describe our practical experience over SV-COMP'15 benchmarks using an implementation in the tool SPACER.

cs.LO↗

arXiv2014

Synthesizing Modular Invariants for Synchronous Code

In this paper, we explore different techniques to synthesize modular invariants for synchronous code encoded as Horn clauses. Modular invariants are a set of formulas that characterizes the validity of predicates. They are very useful for different aspects of analysis, synthesis, testing and program transformation. We describe two techniques to generate modular invariants for code written in the synchronous dataflow language Lustre. The first technique directly encodes the synchronous code in a modular fashion. While in the second technique, we synthesize modular invariants starting from a monolithic invariant. Both techniques, take advantage of analysis techniques based on property-directed reachability. We also describe a technique to minimize the synthesized invariants.

cs.LO↗

arXiv2014

SMT-based Model Checking for Recursive Programs

We present an SMT-based symbolic model checking algorithm for safety verification of recursive programs. The algorithm is modular and analyzes procedures individually. Unlike other SMT-based approaches, it maintains both "over-" and "under-approximations" of procedure summaries. Under-approximations are used to analyze procedure calls without inlining. Over-approximations are used to block infeasible counterexamples and detect convergence to a proof. We show that for programs and properties over a decidable theory, the algorithm is guaranteed to find a counterexample, if one exists. However, efficiency depends on an oracle for quantifier elimination (QE). For Boolean Programs, the algorithm is a polynomial decision procedure, matching the worst-case bounds of the best BDD-based algorithms. For Linear Arithmetic (integers and rationals), we give an efficient instantiation of the algorithm by applying QE "lazily". We use existing interpolation techniques to over-approximate QE and introduce "Model Based Projection" to under-approximate QE. Empirical evaluation on SV-COMP benchmarks shows that our algorithm improves significantly on the state-of-the-art.

cs.LO↗

arXiv2013

Interpolation Properties and SAT-based Model Checking

Craig interpolation is a widespread method in verification, with important applications such as Predicate Abstraction, CounterExample Guided Abstraction Refinement and Lazy Abstraction With Interpolants. Most state-of-the-art model checking techniques based on interpolation require collections of interpolants to satisfy particular properties, to which we refer as "collectives"; they do not hold in general for all interpolation systems and have to be established for each particular system and verification environment. Nevertheless, no systematic approach exists that correlates the individual interpolation systems and compares the necessary collectives. This paper proposes a uniform framework, which encompasses (and generalizes) the most common collectives exploited in verification. We use it for a systematic study of the collectives and of the constraints they pose on propositional interpolation systems used in SAT-based model checking.

cs.LO↗

arXiv2013

Automatic Abstraction in SMT-Based Unbounded Software Model Checking

Software model checkers based on under-approximations and SMT solvers are very successful at verifying safety (i.e. reachability) properties. They combine two key ideas -- (a) "concreteness": a counterexample in an under-approximation is a counterexample in the original program as well, and (b) "generalization": a proof of safety of an under-approximation, produced by an SMT solver, are generalizable to proofs of safety of the original program. In this paper, we present a combination of "automatic abstraction" with the under-approximation-driven framework. We explore two iterative approaches for obtaining and refining abstractions -- "proof based" and "counterexample based" -- and show how they can be combined into a unified algorithm. To the best of our knowledge, this is the first application of Proof-Based Abstraction, primarily used to verify hardware, to Software Verification. We have implemented a prototype of the framework using Z3, and evaluate it on many benchmarks from the Software Verification Competition. We show experimentally that our combination is quite effective on hard instances.

cs.LO↗

arXiv2010

Robust Vacuity for Branching Temporal Logic

There is a growing interest in techniques for detecting whether a logic specification is satisfied too easily, or vacuously. For example, the specification "every request is eventually followed by an acknowledgment" is satisfied vacuously by a system that never generates any requests. Vacuous satisfaction misleads users of model-checking into thinking that a system is correct. There are several existing definitions of vacuity. Originally, Beer et al. formalized vacuity as insensitivity to syntactic perturbation. However, this definition is only reasonable for vacuity in a single occurrence. Armoni et al. argued that vacuity must be robust -- not affected by semantically invariant changes, such as extending a model with additional atomic propositions. They show that syntactic vacuity is not robust for LTL, and propose an alternative definition -- trace vacuity. In this article, we continue this line of research. We show that trace vacuity is not robust for branching time logic. We refine it to apply uniformly to linear and branching time logic and to not suffer from the common pitfalls of prior definitions. Our new definition -- bisimulation vacuity -- is a proper non-trivial extension of both syntactic and trace vacuity. We discuss the complexity of detecting bisimulation vacuity, and give efficient algorithms to detect vacuity for several practically-relevant subsets of CTL*.

cs.LO↗