ABSTRACT. Systems mixing Boolean logic and arithmetic have been a long-standing challenge for verification tools such as SAT-based bit-vector solvers. Though SAT solvers can be highly efficient for Boolean reasoning, they scale poorly once multiplication is involved. Algebraic methods using Groebner basis reduction have recently been used to efficiently verify multiplier circuits in isolation, but generally do not perform well with bit-level reasoning.

We propose that pseudo-Boolean solvers equipped with cutting planes reasoning have the potential to combine the complementary strengths of the existing SAT and algebraic approaches while avoiding their weaknesses.

Theoretically, we show that there are optimal-length cutting planes proofs for a large class of bit-level properties of the most common multiplier circuits. This scaling is significantly better than the smallest proofs known for SAT and, in some instances, for algebraic methods. We also show that cutting planes reasoning can extract bit-level consequences of word-level equations in exponentially fewer steps than methods based on Gröbner bases.

Experimentally, we demonstrate that pseudo-Boolean solvers can verify the word-level equivalence of adder-based multiplier architectures, as well as commutativity of bit-vector multiplication, in times comparable to the best algebraic methods. We then go further than previous approaches and also verify these properties at the bit-level. Finally, we find examples of simple nonlinear bit-vector inequalities that are intractable for current bit-vector and SAT solvers, but easy for pseudo-Boolean solvers.

ABSTRACT. The goal of this study is to improve the scalability of today’s SAT-based solutions for optimization problems and to pave the way towards extending the range of optimization problems solvable with SAT in practice. Let OptSAT be the problem of optimizing a generic Pseudo-Boolean function, given a satisfiable propositional formula F. We introduce an incremental and anytime incomplete algorithm for solving OptSAT, called Polosat. We show that integrating Polosat into a state-of-the-art open-source anytime MaxSAT solver significantly improves the solver’s performance. Furthermore, we demonstrate that Polosat substantially improves the solution quality of an industrial placement tool, where placement is a sub-stage of the physical design stage of chip design.

ABSTRACT. Current state of the art for reasoning about quantifier-free bit-vector constraints in Satisfiability Modulo Theories (SMT) is a technique called bit-blasting, an eager translation into propositional logic (SAT). While efficient in practice, it may not scale for large bit-widths when the input size can not be sufficiently reduced with preprocessing techniques. A recent propagation-based local search procedure was shown to be effective on hard satisfiable instances, in particular in combination with bit-blasting in a sequential portfolio setting. However, a major weakness of this approach is its obliviousness to bits that can be simplified to constant values. In this paper, we generalize propagation-based local search with respect to such constant bits to ternary values. We further extend the procedure to handle more bit-vector operators, and to infer inequality bounds from satisfied root constraints for value selection. We provide an extensive experimental evaluation and show that the presented techniques yield a considerable improvement in performance.

ABSTRACT. The theory of strings supports a large number of operators. Instead of implementing a semi-decision procedure that operates on all the operators directly, string solvers often reduce operators to a core fragment and implement a semi-decision procedure over that fragment. These reductions considerably increase the number of constraints and thus have to be done carefully to achieve good performance. We propose novel reductions from regular expressions to string constraints and a framework for minimizing the introduction of new variables in existing reductions of string constraints. The reductions of regular expression constraints enable string solvers to handle a significant fragment of regular expression constraints without using dedicated reasoning over regular expressions. Minimizing the number of variables in the reduced constraints makes those constraints significantly cheaper to solve by the core solver. An experimental evaluation of our implementation of both techniques in CVC4, a state-of-the-art SMT solver with extensive support for the theory of strings, shows that they significantly improve the solver's performance.

ABSTRACT. Deep neural networks are increasingly being used as con- trollers for safety-critical systems. Because neural networks are opaque, certifying their correctness is a significant challenge. To address this issue, several neural network verification approaches have recently been pro- posed. However, these approaches afford limited scalability, and apply- ing them to large networks can be challenging. In this paper, we propose a framework that can enhance neural network verification techniques by using over-approximation to reduce the size of the network — thus making it more amenable to verification. We perform the approximation such that if the property holds for the smaller (abstract) network, it holds for the original as well. The over-approximation may be too coarse, in which case the underlying verification tool might return a spurious coun- terexample. Under such conditions, we perform counterexample-guided refinement to adjust the approximation, and then repeat the process. Our approach is orthogonal to, and can be integrated with, many exist- ing verification techniques. For evaluation purposes, we integrate it with the recently proposed Marabou framework, and observe a significant im- provement in Marabou’s performance. Our experiments demonstrate the great potential of our approach for verifying larger neural networks.

ABSTRACT. Propositional model counting and model enumeration are key tasks in various applications. In this report I summarize my contributions in this field and identify future research questions.

ABSTRACT. Automated safety and liveness verification of parameterized software is hard: State-of-the-art methods rely on intricate abstractions and complicated proof techniques that often impede automation. We replace this heavy machinery with a clean abstraction framework built from a novel combination of counter abstraction, thread-modular reasoning, and predicate abstraction. Our fully automated method proves parameterized safety and liveness for a wide range of classically challenging examples in a straight-forward manner.

ABSTRACT. The problem of synthesizing specifications of undefined procedures that are consistent with a given safety property has a broad range of applications. However, the usefulness of generated specifications depends on their quality. We formulate this problem as that of solving a system of constrained Horn clauses (CHCs) and present an iterative algorithm to solve them. The algorithm discovers meaningful procedure specifications, along with necessary inductive invariants.

ABSTRACT. In this line of work, we investigate the benefits and key challenges of applying LTL-based synthesis techniques to multi-agent systems. Major challenges are identified and are tackled by the introduction of \emph{least-limiting advisers}; local and minimal assumptions on the behaviour of other actors in the system. The use of these advisers as a means for scalable synthesis, negotiation of assumed behaviours, reasoning about needed information and incorporation of humans in the system is briefly described. After an overview of the envisioned method is given, work done so far is presented.

ABSTRACT. We report on our ongoing work on formulating new methods for synthesis of multi-process reactive programs from the temporal specification. Our methods are fundamentally modular in nature. We show that combining modularity with symmetry helps overcome state explosion which otherwise severely limits scalability.

ABSTRACT. Microbiomes play a critical role in pathogenesis of diseases such as inflammatory bowel disease (IBD). Previous analyses focused on determining gut microbiome composition, but these methods do not provide a way to determine fundamental relationships between microbes. Our method uses Boolean analysis as a CAD tool to find microbe relationships related to IBD and was applied to publicly available microbiome datasets involving IBD. We found that Actinomyces and Lachnospiraceae seem to stronger candidates in determining whether a patient had Crohn’s disease (CD) or ulcerative colitis (UC). This new analysis may improve disease diagnosis and drug testing in terms of accuracy and efficiency. 

ABSTRACT. Designing and monitoring the security of a web-based application is a complex task that does not depend uniquely on the technologies used and on their potential vulnerabilities. Designing a secure architecture also depends on more general threats, arising from the business logic itself and the human interpretation of its inner mechanisms. Threat modeling is a common practice to identify, understand, and address security threats. It is usually done at an early stage, best during the design phase, and heavily relies on a graph of the infrastructure and its data-flow diagram. To the best of my knowledge, there is currently no formal automated threat modeling technique that could help users and security engineers perform security reviews of cloud-based applications. Such a technique should enable comprehensive semantic reasoning about the security of the system. We investigate the usage of Description Logics, a family of logics suitable for knowledge representation, for reasoning about the security of cloud infrastructure. Although the problem of modeling cloud configurations resembles that of modeling generic designs, reasoning about security—potential threats and necessary mitigations—makes it unique in its kind.

ABSTRACT. Witnessing subsystems for probabilistic reachability thresholds in discrete Markovian models are an important concept both as diagnostic information on why a property holds, and as input to refinement algorithms. We present SWITSS, a tool for the computation of Small WITnessing SubSystems. SWITSS implements exact and heuristic approaches based on reducing the problem to (mixed integer) linear programming. Returned subsystems can automatically be rendered graphically and are accompanied with a certificate which proves that the subsystem is indeed a witness.

ABSTRACT. Proof assistants offer tactics to facilitate inductive proofs. However, it still requires human ingenuity to decide what arguments to pass to these tactics. To automate this process, we present smart_induct for Isabelle/HOL. Given an inductive problem in any problem domain, smart_induct lists promising arguments for the induct tactic without relying on a search. Our evaluation demonstrated smart_induct produces valuable recommendations across problem domains.

ABSTRACT. We propose trace logic, an instance of many-sorted first-order logic, to automate the partial correctness verification of programs containing loops. Trace logic generalizes semantics of program locations and captures loop semantics by encoding properties at arbitrary timepoints and loop iterations. We guide and automate inductive loop reasoning in trace logic by using generic trace lemmas capturing inductive loop invariants. Our work is implemented in the RAPID framework, by extending and integrating superposition-based first-order reasoning within RAPID. We successfully used RAPID to prove correctness of many programs whose functional behavior are best summarized in the first-order theories of linear integer arithmetic, arrays and inductive data types.

ABSTRACT. Generating and checking proof certificates is important to increase the trust in automated reasoning tools. In recent years formal verification using computer algebra became more important and is heavily used in automated circuit verification. An existing proof format which covers algebraic reasoning and allows efficient proof checking is the practical algebraic calculus. In this paper we present two independent proof checkers Pacheck and Pastèque. The checker Pacheck checks algebraic proofs more efficiently than Pastèque, but the latter is formally verified using the proof assistant Isabelle/HOL. Furthermore, we introduce extension rules to simulate essential rewriting techniques required in practice. For efficiency we also make use of indices for existing polynomials and include deletion rules too.