ABSTRACT. On the surface, modern-day machine learning and program verification tools appear to have very different and contradictory goals - machine learning emphasizes generality of the hypotheses it discovers over soundness of the results it produces, while program verification ensures correctness of the claims it makes, even at the expense of the generality of the problems it can handle.

Nonetheless, it would also appear that machine learning pipelines have much to offer program verifiers precisely because they are structured to extract useful, albeit hidden, information from their subject domain. When applied to software, data-driven methods may help discover facts and properties critical to program verification that would otherwise require tedious human involvement to state and prove. Conversely, program verification methods would seem to have much to offer machine learning pipelines. Neural networks, the building blocks of modern ML methods, are opaque and uninterpretible, characteristics that make them vulnerable to safety violations and adversarial attacks. Suitably-adapted verification methods may help to identify problematic behavior in these networks, an indispensable need in safety-critical environments.

This talk explores two point instances to support these claims. Our first example considers how machine learning tools can facilitate solutions to Constrained Horn Clauses (CHCs), a popular formalism for encoding verification conditions that capture sophisticated safety properties. We demonstrate how data-driven techniques can be used for efficient invariant discovery over complex recursive CHCs in which the structure of the discovered invariants are drawn from expressive feature spaces (e.g., polyhedra domains). Our second example considers how program verification and synthesis tools can be used to guarantee safety of reinforcement learning-based neural controllers. We suggest a black-box technique that uses the neural network as an oracle to guide the search for a similarlybehaving deterministic program, more amenable to verification, that is guaranteed to satisfy a desired safety specification. This program can then be effectively used within a runtime monitoring framework as a safety shield, overriding proposed actions of the network whenever such actions can cause the system to violate safety conditions.

The results of these investigations give us confidence that there are significant synergies to be had by judiciously combining learning and verification techniques. We envision learners as a mechanism to complement the expressivity of program verifiers by enabling improved efficiency and generality, while verifiers can be used to guarantee the safety of machine learning artifacts without compromising accuracy and utility.

ABSTRACT. We present a new learning algorithm Sorcar to synthesize conjunctive invariants for proving a program satisfies its assertions. The new algorithm is property-driven and is biased towards learning smaller conjunctive invariants over a fixed finite set of n predicates, guarantees convergence in 2n rounds, and takes only polynomial time in each round. We implement and evaluate the algorithm and show that its performance is favorable to the existing Houdini algorithm for a class of benchmarks that prove data race freedom of GPU programs and another class that synthesizes invariants for proving separation logic properties for heap manipulating programs.

ABSTRACT. Direct manipulation is a programming paradigm in which the programmer conveys the intended program behavior by modifying program values at runtime. The programming environment then finds a modification of the original program that yields the manipulated values. This paradigm has been successfully applied to drawing editors to provide programming capabilities that allow users to interact with the displayed graphics. In this paper, we propose the first framework for direct manipulation of imperative programs. First, we introduce \emph{direct state manipulation}, which allows programmers to visualize the trace of a buggy program on an input, and modify variable values at a location. Second, we propose a synthesis technique based on program sketching to efficiently find a program modification that yields the manipulated variable values. Third, to avoid diverging too much from the original program, we augment our synthesis technique with quantitative objectives to find the ``closest'' program to the original one that is consistent with the manipulated values. We formalize the problem and build a tool JDial based on the Sketch synthesizer. We investigate the effectiveness of direct manipulation by using \Name to fix benchmarks from introductory programming assignments. In our evaluation, we observe that direct state manipulations are an effective specification mechanism: even when provided with a single state manipulation, JDial can produce desired program modifications for 66% of our benchmarks while techniques based only on test cases always fail.

ABSTRACT. Given a behavior of interest in the program, statically determining the corresponding responsible entity is a task of critical importance, especially in program security. Classical static analysis techniques (e.g. dependency analysis, taint analysis, slicing, etc.) assist programmers in narrowing down the scope of responsibility, but none of them can explicitly identify the responsible entity. Meanwhile, the causality analysis is generally not pertinent for analyzing programs, and the structural equations model (SEM) of actual causality misses some information inherent in programs, making its analysis on programs imprecise. In this paper, a novel definition of responsibility based on the abstraction of event trace semantics is proposed, which can be applied in program security and other scientific fields. Briefly speaking, an entity E_R is responsible for behavior B, if and only if E_R is free to choose its input value, and such a choice is the first one that ensures the occurrence of B in the forthcoming execution. Compared to current analysis methods, the responsibility analysis is more precise. In addition, our definition of responsibility takes into account the cognizance of the observer, which, to the best of our knowledge, is a new innovative idea in program analysis.

ABSTRACT. We study the problem of formally verifying the robustness to adversarial examples of support vector machines (SVMs), a major machine learning model for classification and regression tasks. Following a recent stream of works on formal robustness verification of (deep) neural networks, our approach relies on a sound abstract version of a given SVM classifier to be used for checking its robustness. This methodology is parametric on a given numerical abstraction of real values and, analogously to the case of neural networks, needs neither abstract least upper bounds nor widening operators on this abstraction. The standard interval domain provides a simple instantiation of our abstraction technique, which is enhanced with the domain of reduced affine forms, which is an efficient abstraction of the zonotope abstract domain. This robustness verification technique has been fully implemented and experimentally evaluated on SVMs based on linear and nonlinear (polynomial and radial basis function) kernels, which have been trained on the popular MNIST dataset of images and on the recent and more challenging Fashion-MNIST dataset. The experimental results of our prototype SVM robustness verifier appear to be encouraging: this automated verification is fast, scalable and shows significantly high percentages of provable robustness on the test set of MNIST, in particular compared to the analogous provable robustness of neural networks.

ABSTRACT. This paper presents a novel program verification method based on Mu-Arithmetic, a first-order logic with integer arithmetic and predicate-level least/greatest fixpoints. We first show that linear-time temporal property verification of first-order recursive programs can be reduced to the validity checking of a Mu-Arithmetic formula. We also propose a method for checking the validity of Mu-Arithmetic formulas. The method generalizes a reduction from termination verification to safety property verification and reduces validity of a Mu-Arithmetic formula to satisfiability of CHCs, which can then be solved by using off-the-shelf CHC solvers. We have implemented an automated prover for Mu-Arithmetic based on the proposed method. By combining the automated prover with a known reduction and the reduction from first-order recursive programs above, we obtain: (i) for while-programs, an automated verification method for arbitrary properties expressible in the modal mu-calculus, and (ii) for first-order recursive programs, an automated verification method for arbitrary linear-time properties expressible in Buchi automata. We have applied our Mu-Arithmetic prover to formulas obtained from various verification problems, and obtained promising experimental results.

ABSTRACT. We propose an extension of linear temporal logic that we call Linear Temporal Logic of Calls (LTLC) for describing temporal properties of higher-order functions, such as ``the function calls its first argument before any call of the second argument.'' A distinguishing feature of LTLC is a new modal operator, the call modality, that checks if the function specified by the operator is called in the current step and binds its arguments to variables usable in its subformula. We demonstrate expressiveness of the logic, by giving examples of LTLC formulas describing interesting properties by comparing it with another temporal logic for higher-order programs proposed by Satake and Unno. Despite its high expressiveness, the model checking problem is decidable for programs with finite base types.

ABSTRACT. Multiphase ranking functions (MPhiRFs) are used to prove termination of loops in which the computation progresses through a number of phases. They consist of linear functions <f1,...,fd> where fi decreases during the i-th phase. This work provides new insights regarding MPhiRFs for loops described by a conjunction of linear constraints (SLC loops). In particular, we consider the existence problem (does a given SLC loop admit a MPhiRF). The decidability and complexity of the problem, in the case that d is restricted by an input parameter, have been settled in recent work, while in this paper we make progress regarding the existence problem without a given depth bound. Our new approach, while falling short of a decision procedure for the general case, reveals some important insights into the structure of these functions. Interestingly, it relates the problem of seeking MPhiRFs to that of seeking recurrent sets (used to prove nontermination). It also helps in identifying classes of loops for which MPhiRFs are sufficient, and thus have linear runtime bounds. For the depth-bounded existence problem, we obtain a new polynomial-time procedure that can provide witnesses for negative answers as well. To obtain this procedure we introduce a new representation for SLC loops, the difference polyhedron replacing the customary transition polyhedron. We find that this representation yields new insights on MPhiRFs and SLC loops in general, and some results on termination and nontermination of bounded SLC loops become straightforward.