View: session overviewtalk overview

10:30 | Sorcar: Property-Driven Algorithms for Learning Conjunctive Invariants PRESENTER: Daniel Neider 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. |

11:00 | Direct Manipulation for Imperative Programs PRESENTER: Qinheping Hu 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. |

11:30 | Responsibility Analysis by Abstract Interpretation PRESENTER: Patrick Cousot 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 |

12:00 | Robustness Verification of Support Vector Machines PRESENTER: Marco Zanella 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. |

14:00 | Temporal Verification of Programs via First-Order Fixpoint Logic PRESENTER: Takeshi Nishikawa 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. |

14:30 | A Temporal Logic for Higher-Order Functional Programs PRESENTER: Yuya Okuyama 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. |

15:00 | Multiphase-Linear Ranking Functions and their Relation to Recurrent Sets PRESENTER: Samir Genaim 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. |