We propose an interactive approach to resolve static analysis alarms. Our approach synergistically combines a sound but imprecise analysis with precise but unsound heuristics, through user interaction. In each iteration, it solves an optimization problem to find a set of questions for the user such that the expected payoff is maximized. We have implemented our approach in a tool, Ursa, that enables interactive alarm resolution for any analysis specified in the declarative logic programming language Datalog. We demonstrate the effectiveness of Ursa on a state-of-the-art static datarace analysis using a suite of 8 Java programs comprising 41-194 KLOC each. Ursa is able to eliminate 74% of the false alarms per benchmark with an average payoff of 12 per question. Moreover, Ursa prioritizes user effort effectively by posing questions that yield high payoffs earlier.
Grigore, R. and Tzevelekos, N. (2016). History-Register Automata. Logical Methods in Computer Science[Online]12:1-32. Available at: http://arxiv.org/pdf/1209.0680v3.pdf.
Programs with dynamic allocation are able to create and use an unbounded number of fresh resources, such as references, objects, files, etc. We propose History-Register
Automata (HRA), a new automata-theoretic formalism for modelling such programs. HRAs extend the expressiveness of previous approaches and bring us to the limits of decidability
for reachability checks. The distinctive feature of our machines is their use of unbounded memory sets (histories) where input symbols can be selectively stored and compared with
symbols to follow. In addition, stored symbols can be consumed or deleted by reset. We show that the combination of consumption and reset capabilities renders the automata
powerful enough to imitate counter machines, and yields closure under all regular operations apart from complementation. We moreover examine weaker notions of HRAs which strike
different balances between expressiveness and effectiveness.
Conference or workshop item
Si, X. et al. (2017). Maximum Satisfiability in Software Analysis: Applications and Techniques. in:29th International Conference, CAV 2017.Springer, pp. 68-94. Available at: https://doi.org/10.1007/978-3-319-63387-9_4.
A central challenge in software analysis concerns balancing different competing tradeoffs. To address this challenge, we propose an approach based on the Maximum Satisfiability (MaxSAT) problem, an optimization extension of the Boolean Satisfiability (SAT) problem. We demonstrate the approach on three diverse applications that advance the state-of-the-art in balancing tradeoffs in software analysis. Enabling these applications on real-world programs necessitates solving large MaxSAT instances comprising over 10301030 clauses in a sound and optimal manner. We propose a general framework that scales to such instances by iteratively expanding a subset of clauses while providing soundness and optimality guarantees. We also present new techniques to instantiate and optimize the framework.
Mikolas, J., Radu, G. and Vasco, M. (2017). On the Quest for an Acyclic Graph. in:24th RCRA International Workshop on "Experimental Evaluation of Algorithms for solving problems with combinatorial explosion".
The paper aims at finding acyclic graphs under a given set of
constraints. More specifically, given a propositional formula
φ over edges of a fixed-size graph, the objective is to find a model of
φ that corresponds to a graph that is acyclic. The paper proposes several encodings of the
problem and compares them in an experimental evaluation using stateof-the-art
Grigore, R. (2017). Java Generics are Turing Complete. in:POPL 2017: Symposium on Principles of Programming Languages.ACM, pp. 73-85. Available at: https://doi.org/10.1145/3009837.3009871.
This paper describes a reduction
from the halting problem of Turing machines to subtype checking in Java.
It follows that subtype checking in Java is undecidable,
which answers a question posed by Kennedy and Pierce in 2007.
It also follows that Java's type checker can recognize any recursive language,
which improves a result of Gil and Levy from 2016.
The latter point is illustrated by a parser generator for fluent interfaces.
Bruna, M. et al. (2016). Proving the Herman-Protocol Conjecture. in:Chatzigiannakis, I. et al. eds.ICALP 2016.Dagstuhl, Germany: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, pp. 104:1-104:12. Available at: http://dx.doi.org/10.4230/LIPIcs.ICALP.2016.104.
Herman's self-stabilisation algorithm, introduced 25 years ago, is a well-studied synchronous randomised protocol for enabling a ring of N processes collectively holding any odd number of tokens to reach a stable state in which a single token remains. Determining the worst-case expected time to stabilisation is the central outstanding open problem about this protocol. It is known that there is a constant h such that any initial configuration has expected stabilisation time at most hN2. Ten years ago, McIver and Morgan established a lower bound of 4/27≈0.148 for h, achieved with three equally-spaced tokens, and conjectured this to be the optimal value of h. A series of papers over the last decade gradually reduced the upper bound on h, with the present record (achieved in 2014) standing at approximately 0.156. In this paper, we prove McIver and Morgan's conjecture and establish that h=4/27 is indeed optimal.
Grigore, R. (2016). Abstraction Refinement Guided by a Learnt Probabilistic Model. in:Principles of Programming Languages.Association for Computing Machinery, pp. 485-498. Available at: http://dx.doi.org/10.1145/2837614.2837663.
The core challenge in designing an effective static program analysis is to find a good program abstraction -- one that retains only details relevant to a given query. In this paper, we present a new approach for automatically finding such an abstraction. Our approach uses a pessimistic strategy, which can optionally use guidance from a probabilistic model. Our approach applies to parametric static analyses implemented in Datalog, and is based on counterexample-guided abstraction refinement. For each untried abstraction, our probabilistic model provides a probability of success, while the size of the abstraction provides an estimate of its cost in terms of analysis time. Combining these two metrics, probability and cost, our refinement algorithm picks an optimal abstraction. Our probabilistic model is a variant of the Erdos-Renyi random graph model, and it is tunable by what we call hyperparameters. We present a method to learn good values for these hyperparameters, by observing past runs of the analysis on an existing codebase. We evaluate our approach on an object sensitive pointer analysis for Java programs, with two client analyses (PolySite and Downcast).
Grigore, R. and Kiefer, S. (2015). Tree Buffers. in:Computer Aided Verification.pp. 290-306. Available at: http://dx.doi.org/10.1007/978-3-319-21690-4_17.
In runtime verification, the central problem is to decide if
a given program execution violates a given property. In online runtime
verification, a monitor observes a program's execution as it happens.
If the program being observed has hard real-time constraints, then the
monitor inherits them. In the presence of hard real-time constraints it
becomes a challenge to maintain enough information to produce error
traces, should a property violation be observed. In this paper we introduce
a data structure, called tree buffer, that solves this problem in the
context of automata-based monitors: If the monitor itself respects hard
real-time constraints, then enriching it by tree buffers makes it possible
to provide error traces, which are essential for diagnosing defects.
We show that tree buffers are also useful in other application domains.
For example, they can be used to implement functionality of capturing
groups in regular expressions. We prove optimal asymptotic bounds for
our data structure, and validate them using empirical data from two
sources: regular expression searching through Wikipedia, and runtime
verification of execution traces obtained from the DaCapo test suite.
Zhang, X. et al. (2014). On abstraction refinement for program analyses in Datalog. in:Programming Language Design and Implementation.New York, USA: Association for Computing Machinery, pp. 239-248. Available at: http://dx.doi.org/10.1145/2594291.2594327.
A central task for a program analysis concerns how to efficiently
find a program abstraction that keeps only information relevant for
proving properties of interest. We present a new approach for finding
such abstractions for program analyses written in Datalog. Our
approach is based on counterexample-guided abstraction refinement:
when a Datalog analysis run fails using an abstraction, it seeks to
generalize the cause of the failure to other abstractions, and pick
a new abstraction that avoids a similar failure. Our solution uses
a boolean satisfiability formulation that is general, complete, and
optimal: it is independent of the Datalog solver, it generalizes the
failure of an abstraction to as many other abstractions as possible,
and it identifies the cheapest refined abstraction to try next. We
show the performance of our approach on a pointer analysis and a
typestate analysis, on eight real-world Java benchmark programs.
Grigore, R. and Kiefer, S. (2018). Selective Monitoring. in:29th International Conference on Concurrency Theory (CONCUR 2018), 4--7 September 2018, Beijing, China.Germany: LIPICS. Available at: http://dx.doi.org/110.4230/LIPIcs.CONCUR.2018.20.
We study selective monitors for labelled Markov chains. Monitors observe the outputs that are
generated by a Markov chain during its run, with the goal of identifying runs as correct or faulty.
A monitor is selective if it skips observations in order to reduce monitoring overhead. We are
interested in monitors that minimize the expected number of observations. We establish an
undecidability result for selectively monitoring general Markov chains. On the other hand, we
show for non-hidden Markov chains (where any output identifies the state the Markov chain is
in) that simple optimal monitors exist and can be computed efficiently, based on DFA language
equivalence. These monitors do not depend on the precise transition probabilities in the Markov
chain. We report on experiments where we compute these monitors for several open-source