ABSTRACT. Property Directed Reachability (PDR) is an efficient and scalable approach for solving systems of symbolic constraints, also known as Constrained Horn Clauses (CHC). In the case of non-linear CHCs, which may arise, e.g., from relational verification tasks, PDR aims to infer an inductive invariant for each uninterpreted predicate. However, in many practical cases, this reasoning is not successful, as invariants need to be discovered for groups of predicates, as opposed to individual predicates. We contribute a novel algorithm that identifies such groups automatically and complements the existing PDR technique. The key feature of the algorithm is that it does not require a possibly expensive synchronization transformation over the system of CHCs. We have implemented the algorithm on top of a state-of-the-art CHC solver Spacer. Our experimental evaluation shows that for some CHC systems, on which existing solvers diverge, our tool is able to discover relational invariants.

ABSTRACT. A Boolean relational specification is a Boolean formula F (X, Y), where X is a vector of outputs, Y is a vector of inputs, that specifies admissible values of X for every value of Y. The Boolean functional synthesis problem asks for a function vector G(Y), of the same dimension as X, such that for all Y, there is an X such that F(X,Y) holds iff F(G(Y),Y) holds. This problem is at the heart several varied applications and hence has resulted in significant interest and design of practically efficient algorithms to solve it. Empirical evidence from applying these algorithms shows that some specifications, despite having a large representation, admit efficient synthesis, while others with a much smaller representation are notoriously hard to synthesize.

In this paper, we investigate the relation between the representation form of the specification F (X, Y) and the complexity of synthesis. We introduce a new normal form for Boolean formulas, called SynNNF, and show that for specifications in SynNNF, synthesis can be accomplished in time quadratic in the size of the specification. We show that several normal forms studied in the knowledge compilation literature (viz. ROBDD/FBDDs, DNNF and dDNNF) are either already in SynNNF or can be efficiently converted to SynNNF, thereby admitting efficient synthesis. We also show that SynNNF can be exponentially more succinct than these other representation forms. Motivated by these results, we propose an algorithm to convert a Boolean relational specification in CNF to SynNNF, with the intent of solving the Boolean functional synthesis problem. Experiments with a prototype implementation show that this approach solves several benchmarks from the QBFEVAL18 suite that state-of-the-art synthesis tools aren’t able to solve.

ABSTRACT. We present a logical framework for the verification of relational properties in imperative programs. Our work is motivated by relational properties which come from security applications and often require reasoning about formulas with quantifier-alternations. Our framework reduces verification of relational properties of imperative programs to a validity problem into trace logic, an expressive instance of first-order predicate logic. Trace logic draws its expressiveness from its syntax, which allows expressing properties over computation traces. Its axiomatization supports fine-grained reasoning about intermediate steps in program execution, notably loop iterations. We present an algorithm to encode the semantics of programs as well as their relational properties in trace logic, and then show how first-order theorem proving can be used to reason about the resulting trace logic formulas. Our work is implemented in the tool \rapid{} and evaluated with examples coming from the security field.

ABSTRACT. Autarkies for SAT can be used for theoretical studies, preprocessing and inprocessing. They generalise satisfying assignments by allowing to leave some clauses "untouched" (no variable assigned). We introduce the natural generalisation to DQCNF (dependency-quantified boolean CNF), and prove basic results on autarky reduction and autarky normal forms.

Finding an autarky for DQCNF is as hard as finding a satisfying assignment. Fortunately there are (many) natural autarky-systems, which allow restricting the range of autarkies to a more feasible domain, while still maintaining the good general properties of arbitrary autarkies (most important here the unique normalform).

We discuss what seems the most fundamental autarky systems, and how the related reductions can be found by SAT solvers.

ABSTRACT. Dependency quantified Boolean formulas (DQBFs) are a powerful formalism, which subsumes quantified Boolean formulas (QBFs) and allows an explicit specification of dependencies of existential variables on universal variables. Driven by the needs of various applications which can be encoded by DQBFs in a natural, compact, and elegant way, research on DQBF solving has emerged in the past few years. However, research focused on closed DQBFs in prenex form (where all quantifiers are placed in front of a propositional formula) and non-prenex DQBFs have almost not been studied in the literature. In this paper we provide a formal definition for syntax and semantics of non-closed non-prenex DQBFs and prove useful properties enabling quantifier localization. Moreover, we make use of our theory by integrating quantifier localization into a state-of-the-art DQBF solver. Experiments with prenex DQBF benchmarks including those from the QBFEVAL’18 competition clearly show that quantifier localization pays off in this context.

ABSTRACT. This paper introduces a new incremental anytime algorithm for Weighted MaxSAT consisting of two main algorithmic components. First, we propose a new efficient polarity selection heuristic and an enhancement to the variable decision heuristic for SAT-based anytime Weighted MaxSAT solving (and, more generally, for solving any optimization problem with a SAT-based anytime algorithm). Second, we enhance an existing Bit-vector Optimization-based algorithm for solving Unweighted MaxSAT and generalize it to Weighted MaxSAT. Our resulting Weighted MaxSAT solver outscores the state-of-the-art solvers in the settings of both the 60-second and 300-second weighted incomplete tracks of MaxSAT Evaluation 2018. In addition, we describe a new application of anytime incremental Weighted MaxSAT solving: placing at the physical design stage of Computer-aided Design (CAD).

ABSTRACT. The problem of sampling a large number of random solutions to SAT and SMT constraints is essential for constrained-random verification and testing. However, most current sampling techniques lack a problem-specific notion of coverage, considering only general goals such uniform distribution. We have developed a new technique for coverage-guided sampling that allows the user to specify the desired coverage points in order to shape the distribution of solutions. Our tool GuidedSampler can efficiently generate high-quality stimuli for constrained-random verification, by sampling valid solutions to a SMT constraint that also cover a large number of user-defined coverage classes.

ABSTRACT. Many relevant problems in formal methods can be tackled using enumerative syntax-guided synthesis (SyGuS). Algorithms for enumerative SyGuS range from universally applicable techniques based on counterexample-guided inductive synthesis (CEGIS), to more scalable but specialized techniques based on divide and conquer. This paper presents a novel algorithm for enumerative SyGuS, Unif+PI, which reaps the benefits of scalability based on divide and conquer without sacrificing generality. In this algorithm, an instance of an SMT solver is used as both a classifier and an attribute generator. Logical constraints in the form of test cases for the function-to-synthesize and failed classification attempts guide its search for new candidate solutions. We implement our approach as an extension of the CVC4Sy solver and evaluate it on standard SyGuS benchmarks from different applications. We show that the new algorithm leads to significant gains in invariant synthesis with respect to state-of-the-art SyGuS solvers, and is competitive with state-of-the-art k-induction based model checking.

ABSTRACT. We present the first approach to prove non-termination of integer programs that is based on loop acceleration. Whenever our technique cannot show non-termination of a loop, it tries to accelerate it instead. Our novel acceleration technique is applicable if the loop's guard satisfies a certain monotonicity condition. As this condition generalizes a simple yet effective non-termination criterion, we can use the same program transformations to facilitate both loop acceleration and non-termination proving. In particular, we present a novel invariant inference technique that is tailored to our approach. An extensive evaluation of our fully automated tool LoAT shows that it is competitive with state-of-the-art termination analyzers.