Publications

In this paper, we examine linear programming (LP) based relaxations for synthesizing polynomial Lyapunov functions to prove the stability of polynomial ODEs. A common approach to Lyapunov function synthesis starts from a desired parametric polynomial form of the polynomial Lyapunov function. Subsequently, we encode the positive-definiteness of the function, and the negative-definiteness of its derivative over the domain of interest. Therefore, the key primitives for this encoding include: (a) proving that a given polynomial is positive definite over a domain of interest, and (b) encoding the positive definiteness of a given parametric polynomial, as a constraint on the unknown parameters. We first examine two classes of relaxations for proving polynomial positivity: relaxations by sum-of-squares (SOS) programs, against relaxations that produce linear programs. We compare both types of relaxations by examining the class of polynomials that can be shown to be positive in each case.

Next, we present a progression of increasingly more powerful LP relaxations based on expressing the given polynomial in its Bernstein form, as a linear combination of Bernstein polynomials. The well-known bounds on Bernstein polynomials over the unit box help us formulate increasingly precise LP relaxations that help us establish the positive definiteness of a polynomial over a bounded domain. Subsequently, we show how these LP relaxations can be used to search for Lyapunov functions for polynomial ODEs by formulating LP instances. We compare our approaches to synthesizing Lyapunov functions with approaches based on SOS programming relaxations. The approaches are evaluated on a suite of benchmark examples drawn from the literature and automatically synthesized benchmarks. Our evaluation clearly demonstrates the promise of LP relaxations, especially for finding polynomial local Lyapunov functions that prove that the system is asymptotically stable over a given bounded region containing the equilibrium. In particular, the LP approach is shown to be as fast as the SOS programming approach, but less prone to numerical problems.

@article{BenSassi_Sankaranarayanan_Others__2015__Synthesis,
author = { Mohamed Amin Ben Sassi, Sriram Sankaranarayanan, Xin Chen, and Erika Abraham },
title = { Linear Relaxations of Polynomial Positivity for Polynomial Lyapunov Function Synthesis },
journal = { IMA Journal of Mathematical Control and Information },
volume = { TBA },
year = { 2015 },
pages = { dnv003 },
publisher = { Oxford University Press }}

This paper deals with the computation of positive polyhedral invariant sets for polynomial dynamical system. A positive invariant set is a subset of the state-space such that if the state of the system is initially in this set, then it remains inside the set for all future time instances. We present a procedure that constructs an invariant set, iteratively, starting from an initial polyhedron that forms a ‘‘guess’’ at the invariant. Our iterative procedure attempts to prove at each stage that the given polyhedron is a positive invariant. This is achieved by first setting up a non-linear program that encodes the invariance conditions for the vector field at each facet of the current polyhedron. This is relaxed to a linear program through the use of blossoming principle for polynomials. If the set fails to be invariant, then we attempt to use local sensitivity analysis using the primal-dual solutions of the linear program to push its faces outwards/inwards in a bid to make it invariant. Doing so, however, keeps the face normals of the iterates fixed for all steps.

In this paper, we generalize the process to allow us to vary the normal vectors as well as the offsets for the individual faces. Doing so, makes the procedure completely general but at the same time increases its complexity. Nevertheless, we demonstrate that the new approach allows our procedure to recover from a poor choice of templates initially to yield better invariants.

@InProceedings{BenSassi+Girard+Sankaranarayanan-2014-Iterative,
author = {Mohamed Amin Ben Sassi and Antoine Girard and Sriram Sankaranarayanan},
title = {Iterative Computation of Polyhedral Invariants Sets for Polynomial Dynamical Systems},
year = {2014},
pages = {6348-6353},
publisher = {IEEE Press},
booktitle = {IEEE Conference on Decision and Control (CDC)},
}

We discuss the verification and optimization of complex systems with respect to a set of specifications under stochastic parameter variations. We introduce a simulation-based statistically sound model inference approach. Our technique considers systems whose responses depend on a few design parameters and many stochastic parameters. The approach consists of two parts: verification and optimization. First, we verify whether the system satisfy the specifications for a given set of values of design parameters using regression and a generalization technique based on statistical model checking. If not, we seek new values of the design parameters for which statistical verification succeeds. The proposed approach involves repeated simulation of the system with fixed design parameters and variational stochastic parameters. Quantile regression is used to construct a relational model that is further generalized into a statistically sound model. The resulting model is used to search iteratively for a new design point. We evaluate this approach over several applications. In each case, the performance is improved significantly compared to the nominal design.

@InProceedings{Zhang+Sankaranarayanan+Somenzi-2014-Statistically,
author = {Yan Zhang and Sriram Sankaranarayanan and Fabio Somenzi},
title = {Statistically Sound Verification and Optimization for Complex Systems},
year = {2014},
pages = {411-427},
publisher = {},
booktitle = {Automated Techniques for Verification and Analysis (ATVA)},
series = {Lecture Notes in Computer Science},
volume = {8837},
}

Diabetes cases worldwide have risen steadily over the past decades, lending urgency to the search for more efficient, effective, and personalized ways to treat the disease. Current treatment strategies, however, may fail to maintain ultradian oscillations in blood glucose concentration, an important element of a healthy alimentary system. Building upon recent successes in mathematical modeling of the human glucose-insulin system, we show that both food intake and insulin therapy likely demand increasingly precise control over insulin sensitivity if oscillations at a healthy average glucose concentration are to be maintained. We then suggest guidelines and personalized treatment options for diabetic patients that maintain these oscillations. We show that for a type II diabetic, both blood glucose levels can be controlled and healthy oscillations maintained when the patient gets an hour of daily exercise and is placed on a combination of Metformin and sulfonylurea drugs. We note that insulin therapy and an additional hour of exercise will reduce the patient's need for sulfonylureas. Results of a modeling analysis suggest that a typical type I diabetic's blood glucose levels can be properly controlled with a constant insulin infusion between 0.45 and 0.7 microU/(ml*min). Lastly, we note that all suggested strategies rely on existing clinical techniques and established treatment measures, and so could potentially be of immediate use in the design of an artificial pancreas.

@Article{Kissler+Others-2014-Determination,
author = {Stephen M. Kissler and Cody Cichowitz and Sriram Sankaranarayanan and David M. Bortz},
title = {Determination of personalized diabetes treatment plans using a two-delay model},
year = {2014},
pages = {101-111},
publisher = {Elsevier Press},
journal = {J. Theoretical Biology},
number = {Oct},
volume = {359},
}

This paper presents a controller synthesis approach using disjunctive polyhedral abstract interpretation. Our approach synthesizes infinite time-horizon controllers for safety properties with discrete-time, linear plant model and a switching feedback controller that is suitable for time-triggered implementations. The core idea behind our approach is to perform an abstract interpretation over disjunctions of convex polyhedra to identify states that are potentially uncontrollable. Complementing this set yields the set of controllable states, starting from which, the safety property can be guaranteed by an appropriate control function. Since, a straightforward disjunctive domain is computationally inefficient, we present an abstract domain based on a state partitioning scheme that allows us to efficiently control the complexity of the intermediate representations. Next, we focus on the automatic generation of controller implementation from our final fixed point. We show that a balanced tree approach can yield efficient controller code with guarantees on the worst-case execution time of the controller. Finally, we evaluate our approach on a suite of benchmarks, comparing different instantiations with related synthesis tools. Our evaluation shows that our approach can successfully synthesize controller implementations for small to medium sized benchmarks.

@InProceedings{Ravanbakhsh+Sankaranarayanan-2014-Infinite,
author = {Hadi Ravanbakhsh and Sriram Sankaranarayanan},
title = {Infinite Horizon Safety Controller Synthesis through Disjunctive Polyhedral Abstract Interpretation},
year = {2014},
pages = {15:1-15:10},
publisher = {ACM Press},
booktitle = {Intl. Conference on Embedded Software (EMSOFT)},
}

We propose an approach for computing under- as well as over-approximations for the reachable sets of continuous systems which are defined by non-linear Ordinary Differential Equations (ODEs). Given a compact and connected initial set of states, described by polynomial inequalities, our approach computes under-approximations of the set of states reachable over time. Our approach is based on a simple yet elegant technique to obtain an accurate Taylor model over-approximation for a backward flowmap based on well-known techniques to over-approximate the forward map. Next, we show that this over-approximation can be used to yield both over- and under-approximations for the forward reachable sets. Based on the result, we are able to conclude ‘‘may’’ as well as ‘‘must’’ reachability to prove properties or conclude the existence of counterexamples. A prototype of the approach is implemented and its performance is evaluated over a considerable number of benchmarks.

@InProceedings{Chen+Others-2014-Under,
author = {Xin Chen and Sriram Sankaranarayanan and Erika Abraham},
title = {Under-approximate Flowpipes for Non-linear Continuous Systems},
year = {2014},
pages = {59-66},
publisher = {},
booktitle = {Formal Methods in Computer-Aided Design (FMCAD)},
}

In this paper, we present an approach for finding violations of safety properties of hybrid systems. Existing approaches search for complete system trajectories that begin from an initial state and reach some unsafe state. We present an approach that searches over segmented trajectories, consisting of a sequence of segments starting from any system state. Adjacent segments may have gaps, which our approach then seeks to narrow iteratively. We show that segmented trajectories are actually paths in the abstract state graph obtained by tiling the state space with cells. Instead of creating the prohibitively large abstract state graph explicitly, our approach implicitly performs a randomized search on it using a {em scatter-and-simulate} technique. This involves repeated simulations, graph search to find likeliest abstract counterexamples, and iterative refinement of the abstract state graph. Finally, we demonstrate our technique on a number of case studies ranging from academic examples to models of industrial-scale control systems.

Winner of EMSOFT Best Paper Award

@InProceedings{Zutshi+Others-2014-Multiple,
author = {Aditya Zutshi and Sriram Sankaranarayanan and Jyotirmoy Deshmukh and James Kapinski},
title = {Multiple-Shooting CEGAR-based falsification for hybrid systems},
year = {2014},
pages = {5:1 - 5:10},
publisher = {ACM Press},
booktitle = {Intl. Conference on Embedded Software (EMSOFT)},
}

Software model checking and static analysis have matured over the last decade, enabling their use in automated software verification. However, lack of scalability makes these tools hard to apply in industry practice. Furthermore, approximations in the models of program and environment lead to a profusion of false alarms. This paper proposes DC2, a verification framework using scope-bounding to address the issue of scalability, while retaining enough precision to avoid false alarms in practice. DC2 splits the analysis problem into manageable parts, relying on a combination of three automated techniques: (a) techniques to infer useful specifications for functions in the form of pre- and post-conditions; (b) stub inference techniques that infer abstractions to replace function calls beyond the verification scope; and (c) automatic refinement of pre- and post-conditions using counterexamples that are deemed to be false alarms by a user. The techniques enable DC2 to perform iterative reasoning over the calling environment of functions, to find non-trivial bugs and fewer false alarms.

Based on the DC2 framework, we have developed a software model checking tool for C/C programs called Varvel, which has been in industrial use at
ec for a number of years. In addition to DC2, we describe other scalability and usability improvements in Varvel that have enabled its successful application on numerous large software projects. These include model simplifications, support for witness understanding to improve debugging assistance, and handling of C programs. We present experimental evaluations that demonstrate the effectiveness of DC2 and report on the usage of Varvel in NEC.

@Article{Ivancic+Others-2014-Scope,
author = {Franjo Ivancic and Gogul Balakrishnan and Aarti Gupta and Sriram Sankaranarayanan and Naoto Maeda and Takashi Imoto and Rakesh Pothengil and Mustafa Hussain},
title = {Scope bounded software verification in Varvel},
year = {2014},
pages = {1-14},
publisher = {Springer},
journal = {Journal of Automated Software Engineering (J. ASE)},
number = {},
volume = {},
}

We present static analyses for probabilistic loops using expectation invariants. Probabilistic loops are imperative while-loops augmented with calls to random variable generators. Whereas, traditional program analysis uses Floyd-Hoare style invariants to over-approximate the set of reachable states, our approach synthesizes invariant inequalities involving the expected values of program expressions at the loop head. We first define the notion of expectation invariants, and demonstrate their usefulness in analyzing probabilistic program loops. Next, we present the set of expectation invariants for a loop as a fixed point of the pre-expectation operator over sets of program expressions. Finally, we use existing concepts from abstract interpretation theory to present an iterative analysis that synthesizes expectation invariants for probabilistic program loops. We show how the standard polyhedral abstract domain can be used to synthesize expectation invariants for probabilistic programs, and demonstrate the usefulness of our approach on some examples of probabilistic program loops.

Radhia Cousot Best Paper Award

@InProceedings{Chakarov+Sankaranarayanan-2014-Expectation,
author = {Aleksandar Chakarov and Sriram Sankaranarayanan},
title = {Expectation Invariants as Fixed Points of Probabilistic Programs},
year = {2014},
pages = {85-100},
publisher = {Springer-Verlag},
booktitle = {Static Analysis Symposium (SAS)},
series = {Lecture Notes in Computer Science},
volume = {8723},
}

This paper introduces QUICr, an abstract domain combinator library that lifts any domain for numbers into an efficient domain for numbers and sets of numbers. As a library, it is useful for inferring relational data invariants in programs that manipulate data structures. As a testbed, it allows easy extension of widening and join heuristics, enabling adaptations to new and varied applications. In this paper we present the architecture of the library, guidelines on how to select heuristics, and an example instantiation of the library using the Apron library to verify set-manipulating programs.

Tool Demonstration Paper

QUIC Graphs Project Page

@InProceedings{Cox+Chang+Sankaranarayanan-2014-QUICr,
author = {Arlen Cox and Bor-Yuh Evan Chang and Sriram Sankaranarayanan},
title = {QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers},
year = {2014},
pages = {866-873},
publisher = {Springer-Verlag},
booktitle = {Computer-Aided Verification (CAV)},
series = {Lecture Notes in Computer Science},
volume = {8559},
}

In this paper, we focus on finding positive invariants and Lyapunov functions to establish reachability and stability properties, respectively, of polynomial ordinary differential equations (ODEs). In general, the search for such functions is a hard problem. As a result, numerous techniques have been developed to search for polynomial differential variants that yield positive invariants and polynomial Lyapunov functions that prove stability, for systems defined by polynomial differential equations. However, the systematic search for non-polynomial functions is considered a much harder problem, and has received much less attention.

In this paper, we combine ideas from computer algebra with the Sum-Of-Squares (SOS) relaxation for polynomial positive semi-definiteness to find non polynomial differential variants and Lyapunov functions for polynomial ODEs. Using the well-known concept of Darboux polynomials, we show how Darboux polynomials can, in many instances, naturally lead to specific forms of Lyapunov functions that involve rational function, logarithmic and exponential terms. We demonstrate the value of our approach by deriving non-polynomial Lyapunov functions for numerical examples drawn from the literature.

@InProceedings{Goubault+Others-2014-Finding,
author = {Eric Goubault and Jacques-Henri Jourdan and Sylvie Putot and Sriram Sankaranarayanan},
title = {Finding Non-Polynomial Positive Invariants and Lyapunov Functions for Polynomial Systems through Darboux Polynomials},
year = {2014},
pages = {3571 - 3578},
publisher = {IEEE Press},
booktitle = {Proc. American Control Conference (ACC)},
}

We present a technique that allows us to find Sum-of-Squares Lyapunov functions for hybrid dynamical systems. Given a template form for the Lyapunov function, our technique uses simulation data to infer constraints, the solution of which provides a candidate Lyapunov function. Our technique then uses a global optimizer to search the region of interest for trajectories that violate the Lyapunov conditions for the given function, which are fed back into the procedure as additional constraints. Once the procedure terminates, we use a nonlinear SMT solver to verify the Lyapunov conditions, in order to obtain a proof of soundness of the candidate Lyapunov function (which the global optimizer cannot guarantee). Failures of this check give yet another set of constraints to drive the search procedure.

@InProceedings{Kapinski+Others-2014-Simulation,
author = {James Kapinski and Jyotirmoy V. Deshmukh and Sriram Sankaranarayanan and Nikos Arechiga},
title = {Simulation-guided Lyapunov Analysis for Hybrid Dynamical Systems},
year = {2014},
pages = {133-142},
publisher = {ACM Press},
booktitle = {Hybrid Systems: Computation and Control (HSCC)},
}

We present abstract acceleration techniques for computing loop invariants for numerical programs with linear assignments and conditionals. Whereas abstract interpretation techniques typically over-approximate the set of reachable states iteratively, abstract acceleration captures the effect of the loop with a single, non-iterative transfer function applied to the initial states at the loop head. In contrast to previous acceleration techniques, our approach applies to any linear loop without restrictions. Its novelty lies in the use of the Jordan normal form decomposition of the loop body to derive symbolic expressions for the entries of the matrix modeling the effect of n>=0 iterations of the loop. The entries of such a matrix depend on n through complex polynomial, exponential and trigonometric functions. Therefore, we introduces an abstract domain for matrices that captures the linear inequality relations between these complex expressions. This results in an abstract matrix for describing the fixpoint semantics of the loop. Our approach integrates smoothly into standard abstract interpreters and can handle programs with nested loops and loops containing conditional branches. We evaluate it over small but complex loops that are commonly found in control software, comparing it with other tools for computing linear loop invariants. The loops in our benchmarks typically exhibit polynomial, exponential and oscillatory behaviors that present challenges to existing approaches. Our approach finds non-trivial invariants to prove useful bounds on the values of variables for such loops, clearly outperforming the existing approaches in terms of precision while exhibiting good performance.

@InProceedings{Jeannet+Schrammel+Sankaranarayanan-2014-Abstract,
author = {Bertrand Jeannet and Peter Schrammel and Sriram Sankaranarayanan},
title = {Abstract Acceleration of General Linear Loops},
year = {2014},
pages = {529-540},
publisher = {ACM Press},
booktitle = {Principles of Programming Languages (POPL)},
}

In this paper, we address the problem of performance modeling for transistor-level circuits under process variations. A sparse regression technique is introduced to characterize the relationship between the process parameters and the output responses. This approach relies on repeated simulations to find polynomial approximations of response surfaces. It employs a heuristic to construct sparse polynomial expansions and a stepwise regression algorithm based on LASSO to find low degree polynomial approximations. The proposed technique is able to handle many tens of process parameters with a small number of simulations when compared to an earlier approach using ordinary least squares. We present our approach in the context of statistical model inference (SMI), a recently proposed statistical verification framework for transistor-level circuits. Our experimental evaluation compares percentage yields predicted by our approach with Monte-Carlo simulations and SMI using ordinary least squares on benchmarks with up to 30 process parameters. The sparse-SMI approach is shown to require significantly fewer simulations, achieving orders of magnitude improvement in the run times with small differences in the resulting yield estimates.

@InProceedings{Zhang+Sankaranarayanan+Somenzi-2014-Sparse,
author = {Yan Zhang and Sriram Sankaranarayanan and Fabio Somenzi},
title = {Sparse statistical model inference for analog circuits under process variations},
year = {2014},
pages = {449-454},
publisher = {IEEE Press},
booktitle = {Asia and South Pacific Design Automation Conference (ASP-DAC)},
}

We present a Monte-Carlo optimization technique for finding system behaviors that falsify a metric temporal logic (MTL) property. Our approach performs a random walk over the space of system inputs guided by a robustness metric defined by the MTL property. Robustness is guiding the search for a falsifying behavior by exploring trajectories with smaller robustness values. The resulting testing framework can be applied to a wide class of cyber-physical systems (CPS). We show through experiments on complex system models that using our framework can help automatically falsify properties with more consistency as compared to other means, such as uniform sampling.

Click here to access the S-Taliro tool

@Article{Abbas+Others-2013-Probabilistic,
author = {Houssam Abbas and Georgios Fainekos and Sriram Sankaranarayanan and Franjo Ivancic and Aarti Gupta},
title = {Probabilistic Temporal Logic Falsification of Cyber-Physical Systems},
year = {2013},
pages = {95},
publisher = {ACM Press},
journal = {ACM Transactions on Embedded Computing Systems (TECS)},
number = {12s},
volume = {12},
}

We propose a general framework for static analysis of concurrent multi-threaded programs in the presence of various types of synchronization primitives such as locks and pairwise rendezvous. In order to capture interference between threads, we use the notion of a transaction, i.e., a sequence of statements in a thread that can be executed atomically, without sacrificing the soundness of the analysis while yielding precise results. These transactions are delineated automatically, and are captured in the form of a transaction graph over the global control state space of the program. Starting from a coarse transaction graph, constructed by exploiting scheduling constraints related to synchronizations and partial order reduction, we iteratively refine the graph by removing statically unreachable nodes using the results of various analyses. Specifically, we use abstract interpretation to automatically derive program invariants, based on abstract domains of increasing precision. Progressive refinement of the transaction graph enhances scalability of the static analyses, yielding more precise invariants. We demonstrate the benefits of this framework in an application to find data race bugs in concurrent programs, where our static analyses serve to reduce the number of false warnings captured by an initial lockset analysis. This framework also facilitates use of model checking on the remaining warnings to generate concrete error traces, where we leverage the preceding static analyses to generate small program slices and the derived invariants to improve performance. We describe our experimental results on a suite of Linux device drivers.

@Article{Kahlon+Sankaranarayanan+Gupta-2013-Static,
author = {Vineet Kahlon and Sriram Sankaranarayanan and Aarti Gupta},
title = {Static analysis for concurrent programs with applications to data race detection},
year = {2013},
pages = {321-336},
publisher = {Springer-Verlag},
journal = {STTT},
number = {4},
volume = {15},
}

This paper examines techniques for finding falsifying trajectories of hybrid systems using an approach that we call trajectory splicing. Many formal verification techniques for hybrid systems, including flowpipe construction, can identify plausible abstract counterexamples for property violations. However, there is often a gap between the reported abstract counterexamples and the concrete system trajectories. Our approach starts with a candidate sequence of disconnected trajectory segments, each segment lying inside a discrete mode. However, such disconnected segments do not form concrete violations due to the gaps that exist between the ending state of one segment and the starting state of the subsequent segment. Therefore, trajectory splicing uses local optimization to minimize the gap between these segments, effectively splicing them together to form a concrete trajectory. We demonstrate the use of our approach for falsifying safety properties of hybrid systems using standard optimization techniques. As such, our approach is not restricted to linear systems. We compare our approach with other falsification approaches including uniform random sampling and a robustness guided falsification approach used in the tool S-Taliro. Our preliminary evaluation clearly shows the potential of our approach to search for candidate trajectory segments and use them to find concrete property violations.

Invited Session on Formal Methods in Control

@InProceedings{Zutshi+Others-2013-Trajectory,
author = {Zutshi, Aditya and Sankaranarayanan, Sriram and Deshmukh, Jyotirmoy and Kapinski, James},
title = {A trajectory splicing approach to concretizing counterexamples for hybrid systems},
year = {2013},
pages = {3918-3925},
publisher = {IEEE Press},
booktitle = {IEEE Conference on Decision and Control (CDC)},
}

This paper studies the effect of parameter variation on the behavior of analog circuits at the transistor (netlist) level. It is well known that variation in key circuit parameters can often adversely impact the correctness and performance of analog circuits during fabrication. An important problem lies in characterizing a safe subset of the parameter space for which the circuit can be guaranteed to satisfy the design specification. Due to the sheer size and complexity of analog circuits, a formal approach to the problem remains out of reach, especially at the transistor level. Therefore, we present a statistical model inference approach that exploits recent advances in statistical verification techniques. Our approach uses extensive circuit simulations to infer polynomials that approximate the behavior of a circuit. A procedure inspired by statistical model checking is then introduced to produce “statistically sound” models that extend the polynomial approximation. The resulting model can be viewed as a statistically guaranteed over-approximation of the circuit behavior. The proposed technique is demonstrated with two case studies in which it identifies subsets of parameters that satisfy the design specifications.

Yan Zhang's thesis extends this work substantially

@InProceedings{Zhang+Sankaranarayanan+Somenzi+Chen+Abraham-2013-From,
author = {Yan Zhang and Sriram Sankaranarayanan and Fabio Somenzi and Xin Chen and Erika Abraham},
title = {From statistical model checking to statistical model inference: characterizing the effect of process variations in analog circuits},
year = {2013},
pages = {662-669},
publisher = {IEEE/ACM Press},
booktitle = {International Conference on Computer-Aided Design (ICCAD)},
}

We investigate linear programming relaxations to synthesize Lyapunov functions that establish the stability of a given system over a bounded region. In particular, we attempt to discover functions that are more readily useful inside symbolic verification tools for proving the correctness of control systems. Our approach searches for a Lyapunov function, given a parametric form with unknown coefficients, by constructing a system of linear inequality constraints over the unknown parameters. We examine two complementary ideas for the linear programming relaxation, including interval evaluation of the polynomial form and “Handelman representations” for positive polynomials over polyhedral sets. Our approach is implemented as part of a branch-and-relax scheme for discovering Lyapunov functions. We evaluate our approach using a prototype implementation, comparing it with techniques based on Sum-of-Squares (SOS) programming. A comparison with SOSTOOLS is carried out over a set of benchmarks gathered from the related work. The evaluation suggests that our approach using Simplex is generally fast, and discovers Lyapunov functions that are simpler and easy to check. They are suitable for use inside symbolic formal verification tools for reasoning about continuous systems.

Invited Session on Reliable methods for control, state estimation and parameter identification of uncertain dynamic systems

The results of this paper are subsumed by this preprint

@InProceedings{Sankaranarayanan+Others-2013-Lyapunov,
author = {Sriram Sankaranarayanan and Xin Chen and Erika Abraham},
title = {Lyapunov Function Synthesis Using Handelman Representations},
year = {2013},
pages = {576-581},
publisher = {},
booktitle = {IFAC conference on Nonlinear Control Systems (NOLCOS)},
}

We initiate the study of regular real analysis, or the analysis of real functions that can be encoded by automata on infinite words. It is known that omega-automata can be used to represent relations between real vectors, reals being represented in exact precision as infinite streams. The regular functions studied here constitute the functional subset of such relations. We show that some classic questions in function analysis can become elegantly computable in the context of regular real analysis. Specifically, we present an automata-theoretic technique for reasoning about limit behaviors of regular functions, and obtain, using this method, a decision procedure to verify the continuity of a regular function. Several other decision procedures for regular functions - for finding roots, fixpoints, minima, etc. - are also presented. At the same time, we show that the class of regular functions is quite rich, and includes functions that are highly challenging to encode using traditional symbolic notation.

@InProceedings{Chaudhuri+Sankaranarayanan+Vardi-2013-Regular,
author = {Swarat Chaudhuri and Sriram Sankaranarayanan and Moshe Vardi},
title = {Regular Real Analysis},
year = {2013},
pages = {509-518},
publisher = {IEEE Press},
booktitle = {IEEE Symposium on Logic in Computer Science (LICS)},
}

We present techniques for the analysis of infinite state probabilistic programs to synthesize probabilistic invariants and prove almost-sure termination. Our analysis is based on the notion of (super) martingales from probability theory. First, we define the concept of (super) martingales for loops in probabilistic programs. Next, we present the use of concentration of measure inequalities to bound the values of martingales with high probability. This directly allows us to infer probabilistic bounds on assertions involving the program variables. Next, we present the notion of a super martingale ranking function (SMRF) to prove almost sure termination of probabilistic programs. Finally, we extend constraint-based techniques to synthesize martingales and super-martingale ranking functions for probabilistic programs. We present some applications of our approach to reason about invariance and termination of small but complex probabilistic programs.

Resources pertaining to our probabilistic program analysis project are here

@InProceedings{Chakarov+Sankaranarayanan-2013-Probabilistic,
author = {Aleksandar Chakarov and Sriram Sankaranarayanan},
title = {Probabilistic Program Analysis using Martingales},
year = {2013},
pages = {511-526},
publisher = {Springer-Verlag},
booktitle = {Computer-Aided Verification (CAV)},
series = {Lecture Notes in Computer Science},
volume = {8044},
}

The tool Flow* performs Taylor model-based flowpipe construction for non-linear (polynomial) hybrid systems. Flow* combines well-known Taylor model arithmetic techniques for guaranteed approximations of the continuous dynamics in each mode with a combination of approaches for handling mode invariants and discrete transitions. Flow* supports a wide variety of optimizations including adaptive step sizes, adaptive selection of approximation orders and the heuristic selection of template directions for aggregating flowpipes. This paper describes Flow* and demonstrates its performance on a series of non-linear continuous and hybrid system benchmarks. Our comparisons show that Flow* is competitive with other tools.

Flow* can be downloaded here and case-studies using the tool are here

@InProceedings{Chen+Abraham+Sankaranarayanan-2013-Flow,
author = {Xin Chen and Erika Abraham and Sriram Sankaranarayanan},
title = {Flow*: An Analyzer for Non-Linear Hybrid Systems},
year = {2013},
pages = {258-263},
publisher = {Springer-Verlag},
booktitle = {Computer-Aided Verification (CAV)},
series = {Lecture Notes in Computer Science},
volume = {8044},
}

We propose an approach for the static analysis of probabilistic programs that sense, manipulate, and control based on uncertain data. Examples include programs used in risk analysis, medical decision making and cyber-physical systems. Correctness properties of such programs take the form of queries that seek the probabilities of assertions over program variables. We present a static analysis approach that provides guaranteed interval bounds on the values (assertion probabilities) of such queries. First, we observe that for probabilistic programs, it is possible to conclude facts about the behavior of the entire program by choosing a finite, adequate set of its paths. We provide strategies for choosing such a set of paths and verifying its adequacy. The queries are evaluated over each path by a combination of symbolic execution and probabilistic volume-bound computations. Each path yields interval bounds that can be summed up with a “coverage” bound to yield an interval that encloses the probability of assertion for the program as a whole. We demonstrate promising results on a suite of benchmarks from many different sources including robotic manipulators and medical decision making programs.

ACM SIGPLAN Distinguished Paper Award.

Resources pertaining to our probabilistic program analysis project are here

@InProceedings{Sankaranarayanan+Chakarov+Gulwani-2013-Static,
author = {Sriram Sankaranarayanan and Aleksandar Chakarov and Sumit Gulwani},
title = {Static Analysis for Probabilistic Programs: Inferring Whole Program Properties from Finitely Many Paths},
year = {2013},
pages = {447-458},
publisher = {ACM Press},
booktitle = {ACM conference on Programming Languages Design and Implementation (PLDI)},
}

In this paper, we present a promising approach to systematically testing graphical user interfaces (GUI) in a platform independent manner. Our framework uses standard computer vision techniques through a python-based scripting language (Sikuli script) to identify key graphical elements in the screen and automatically interact with these elements by simulating keypresses and pointer clicks. The sequence of inputs and outputs resulting from the interaction is analyzed using grammatical inference techniques that can infer the likely internal states and transitions of the GUI based on the observations. Our framework handles a wide variety of user interfaces ranging from traditional pull down menus to interfaces built for mobile platforms such as Android and iOS. Furthermore, the automaton inferred by our approach can be used to check for potentially harmful patterns in the interface's internal state machine such as design inconsistencies (eg,. a keypress does not have the intended effect) and mode confusion that can make the interface hard to use. We describe an implementation of the framework and demonstrate its working on a variety of interfaces including the user-interface of a safety critical insulin infusion pump that is commonly used by type-1 diabetic patients.

@InProceedings{Givens+Others-2013-Exploring,
author = {Paul Givens and Aleksandar Chakarov and Sriram Sankaranarayanan and Tom Yeh},
title = {Exploring the Internal State of User Interfaces by Combining Computer Vision Techniques with Grammatical Inference},
year = {2013},
pages = {1165-1168},
publisher = {ACM Press},
booktitle = {Proc. International Conference on Software Engg. (NIER track)},
}

Programs written in modern languages perform intricate manipulations of containers such as arrays, lists, dictionaries, and sets. We present an abstract interpretation-based framework for automatically inferring relations between the set of values stored in these containers. Relations include inclusion relations over unions and intersections, as well as quantified relationships with scalar variables. We develop an abstract domain constructor that builds a container domain out of a Quantified Union-Intersection Constraint (QUIC) graph parameterized by an arbitrary base domain. We instantiate our domain with a polyhedral base domain and evaluate it on programs extracted from the Python test suite. Over traditional, non-relational domains, we find significant precision improvements with minimal performance cost.

QUIC Graphs Project Page

@InProceedings{Cox+Chang+Sankaranarayanan-2013-QUIC,
author = {Arlen Cox and Bor-Yuh Evan Chang and Sriram Sankaranarayanan},
title = {QUIC Graphs: Relational Invariant Generation for Containers},
year = {2013},
pages = {401-425},
publisher = {Springer-Verlag},
booktitle = {European Colloquium on Object-Oriented Programming (ECOOP)},
series = {Lecture Notes in Computer Science},
volume = {7920},
}

We propose an approach for verifying non-linear hybrid systems using higher-order Taylor models that are a combination of bounded degree polynomials over the initial conditions and time, bloated by an interval. Taylor models are an effective means for computing rigorous bounds on the complex time trajectories of non-linear differential equations. As a result, Taylor models have been successfully used to verify properties of non-linear continuous systems. However, the handling of discrete (controller) transitions remains a challenging problem. In this paper, we provide techniques for handling the effect of discrete transitions on Taylor model flowpipe construction. We explore various solutions based on two ideas: domain contraction and range over-approximation. Instead of explicitly computing the intersection of a Taylor model with a guard set, domain contraction makes the domain of a Taylor model smaller by cutting away parts for which the intersection is empty. It is complemented by range over-approximation that translates Taylor models into commonly used representations such as template polyhedra or zonotopes, on which intersections with guard sets have been previously studied. We provide an implementation of the techniques described in the paper and evaluate the various design choices over a set of challenging benchmarks.

Flow* tool can be downloaded here

@InProceedings{Chen+Abraham+Sankaranarayanan-2012-Taylor,
author = {Xin Chen and Erika Abraham and Sriram Sankaranarayanan},
title = {Taylor Model Flowpipe Construction for Non-linear Hybrid Systems},
year = {2012},
pages = {183-192},
publisher = {IEEE Press},
booktitle = {Real Time Systems Symposium (RTSS)},
}

Digital filters are simple yet ubiquitous components of a wide variety of digital processing and control systems. Errors in the filters can be catastrophic. Traditionally digital filters have been verified using methods from control theory and extensive testing. We study two alternative verification techniques: bit-precise analysis and real-valued error approximations. In this paper, we empirically evaluate several variants of these two fundamental approaches for verifying fixed-point implementations of digital filters. We design our comparison to reveal the best possible approach towards verifying real-world designs of infinite impulse response (IIR) digital filters. Our study reveals broader insights into cases where bit-reasoning is absolutely necessary and suggests efficient approaches using modern satisfiability-modulo-theories (SMT) solvers.

Click here to download the filter verification tool

@InProceedings{Cox+Others-2012-Bit,
author = {Arlen Cox and Sriram Sankaranarayanan and Bor-Yuh Evan Chang},
title = {A Bit too Precise? Bounded Verification of Quantized Digital Filters},
year = {2012},
pages = {33-42},
publisher = {},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS)},
series = {Lecture Notes in Computer Science},
volume = {7214},
}

Randomized testing is a popular approach for checking properties of large embedded system designs. It is well known that a uniform random choice of test inputs is often sub-optimal. Ideally, the choice of inputs has to be guided by choosing the right input distributions in order to expose corner-case violations. However, this is also known to be a hard problem, in practice. In this paper, we present an application of the cross-entropy method for adaptively choosing input distributions for falsifying temporal logic properties of hybrid systems. We present various choices for representing input distribution families for the cross-entropy method, ranging from a complete partitioning of the input space into cells to a factored distribution of the input using graphical models.

Finally, we experimentally compare the falsification approach using the cross-entropy method to other stochastic and heuristic optimization techniques implemented inside the tool S-Taliro over a set of benchmark systems. The performance of the cross entropy method is quite promising. We find that sampling inputs using the cross-entropy method guided by trace robustness can discover violations faster, and more consistently than the other competing methods considered.

@InProceedings{Sankaranarayanan+Fainekos-2012-Falsification,
author = {Sriram Sankaranarayanan and Georgios E. Fainekos},
title = {Falsification of temporal properties of hybrid systems using the cross-entropy method},
year = {2012},
pages = {125-134},
publisher = {ACM},
booktitle = {HSCC},
}

S-TALIRO is a software toolbox that performs stochastic search for system trajectories that falsify realtime temporal logic specifications. S-TaLiRo is founded on the notion of robustness of temporal logic specifications. In this paper, we present a dynamic programming algorithm for computing the robustness of temporal logic specifications with respect to system trajectories. We also demonstrate that typical automotive functional requirements can be captured and falsified using temporal logics and S-TALIRO.

Invited Session on Verification of Automotive Control Systems

see S-Taliro page

@InProceedings{Fainekos+Others-2012-Verification,
author = {Georgios Fainekos and Sriram Sankaranarayanan and Koichi Ueda and Hakan Yazarel},
title = {Verification of Automotive Control Applications using S-Taliro},
year = {2012},
pages = {3567-3572},
publisher = {IEEE Press},
booktitle = {American Control Conference (ACC)},
}

In this paper, we define timed relational abstractions for verifying sampled data control systems. Sampled data control systems consist of a plant, modeled as a hybrid system and a synchronous controller, modeled as a discrete transition system. The controller computes control inputs and/or sends control events to the plant based on the periodically sampled state of the plant. The correctness of the system depends on the controller design as well as an appropriate choice of the controller sampling period.

Our approach constructs a timed relational abstraction of the hybrid plant by replacing the continuous plant dynamics by relations. These relations map a state of the plant to states reachable within the sampling time period. We present techniques for building timed relational abstractions, while taking care of discrete transitions that can be taken by the plant between samples. The resulting abstractions are better suited for the verification of sampled data control systems. The abstractions focus on the states that can be observed by the controller at the sample times, while abstracting away behaviors between sample times conservatively. The resulting abstractions are discrete, infinite-state transition systems. Thus conventional verification tools can be used to verify safety properties of these abstractions. We use k-induction to prove safety properties and bounded model checking (BMC) to find potential falsifications. We present our idea, its implementation and results on many benchmark examples.

Click here

@InProceedings{Zutshi+Others-2012-Timed,
author = {Aditya Zutshi and Sriram Sankaranarayanan and Ashish Tiwari},
title = {Timed Relational Abstractions for Sampled Data Control Systems},
year = {2012},
pages = {343-361},
publisher = {Springer-Verlag},
booktitle = {Computer-Aided Verification (CAV)},
series = {Lecture Notes in Computer Science},
volume = {7358},
}

We present a case study on the use of robustness-guided and statistical model checking approaches for simulating risks due to insulin infusion pump usage by diabetic patients. Insulin infusion pumps allow for a continuous delivery of insulin with varying rates and delivery profiles to help patients self-regulate their blood glucose levels. However, the use of infusion pumps and continuous glucose monitors can pose risks to the patient including chronically elevated blood glucose levels (hyperglycemia) or dangerously low glucose levels (hypoglycemia). In this paper, we use mathematical models of the basic insulin-glucose regulatory system in a diabetic patient, insulin infusion pumps, and the user’s interaction with these pumps defined by commonly used insulin infusion strategies for maintaining normal glucose levels. These strategies include common guidelines taught to patients by physicians and certified diabetes educators and have been implemented in commercially available insulin bolus calculators. Furthermore, we model the failures in the devices themselves along with common errors in the usage of the pump. We compose these models together and analyze them using two related techniques: (a) robustness guided state-space search to explore worst-case scenarios and (b) statistical model checking techniques to assess the probabilities of hyper- and hypoglycemia risks. Our technique can be used to identify the worst-case effects of the combination of many different kinds of failures and place high confidence bounds on their probabilities.

Our infusion pump analysis project page has more details.

@InProceedings{Sankaranarayanan+Fainekos-2012-Simulating,
author = {Sankaranarayanan, Sriram and Fainekos, Georgios},
title = {Simulating Insulin Infusion Pump Risks by In-Silico Modeling of the Insulin-Glucose Regulatory System},
year = {2012},
pages = {322-341},
publisher = {Springer-Verlag},
booktitle = {Computational Methods in Systems Biology (CMSB)},
series = {Lecture Notes in Computer Science},
volume = {7605},
}

One of the important challenges in robotics is the automatic synthesis of provably correct controllers from high level specifications. One class of such algorithms operates in two steps: (i) high level discrete controller synthesis and (ii) low level continuous controller synthesis. In this class of algorithms, when phase (i) fails, then it is desirable to provide feedback to the designer in the form of revised specifications that can be achieved by the system. In this paper, we address the minimal revision problem for specification automata. That is, we construct automata specifications that are as “close” as possible to the initial user intent, by removing the minimum number of constraints from the specification that cannot be satisfied. We prove that the problem is computationally hard and we encode it as a satisfiability problem. Then, the minimal revision problem can be solved by utilizing efficient SAT solvers.

@InProceedings{Kim+Fainekos+Sankaranarayanan-2012-Revision,
author = {Kangjin Kim and Georgios E. Fainekos and Sriram Sankaranarayanan},
title = {On the revision problem of specification automata},
year = {2012},
pages = {5171-5176},
publisher = {IEEE Press},
booktitle = {ICRA},
}

Modern object-oriented programming languages such as C provide convenient abstractions and data encapsulation mechanisms for software developers. However, these features also complicate testing and static analysis of programs that utilize object-oriented programming concepts. In particular, the C language exhibits features such as multiple inheritance, static and dynamic typecasting that make static analyzers for C quite hard to implement. In this paper, we present an approach where static analysis is performed by lowering the original C program into a semantically equivalent C program. However, unlike existing translation mechanisms that utilize complex pointer arithmetic operations, virtual-base offsets, virtual-function pointer tables, and calls to run-time libraries to model C features, our translation is targeted towards making static program analyzers for C easier to write and provide more precise results. We have implemented our ideas in a framework for C called CILpp that is analogous to the popular C Intermediate Language (CIL) framework. We evaluate the effectiveness of our translation in a bug finding tool that uses abstract interpretation and model checking. The bug finding tool uncovered several previously unknown bugs in C open source projects.

@InProceedings{Yang+Others-2012-Object,
author = {Jing Yang and Gogul Balakrishnan and Naoto Maeda and Franjo Ivancic and Aarti Gupta and Nishant Sinha and Sriram Sankaranarayanan and Naveen Sharma},
title = {Object Model Construction for Inheritance in C and Its Applications to Program Analysis},
year = {2012},
pages = {144-164},
publisher = {Springer-Verlag},
booktitle = {Compiler Construction (CC)},
series = {Lecture Notes in Computer Science},
volume = {7210},
}

We examine the problem of inferring invariants for parametrized systems. Parametrized systems are concurrent systems consisting of an a priori unbounded number of process instances running the same program. Such systems are commonly encountered in many situations including device drivers, distributed systems, and robotic swarms. In this paper we describe a technique that enables leveraging off-the-shelf invariant generators designed for sequential programs to infer invariants of parametrized systems. The central challenge in invariant inference for parametrized systems is that näıvely exploding the transition system with all interleavings is not just impractical but impossible. In our approach, the key enabler is the notion of a reflective abstraction that we prove has an important correspondence with inductive invariants. This correspondence naturally gives rise to an iterative invariant generation procedure that alternates between computing candidate invariants and creating reflective abstractions.

@InProceedings{Sanchez+Others-2012-Invariant,
author = {Alejandro Sanchez and Sriram Sankaranarayanan and Cesar Sanchez and Bor-Yuh Evan Chang},
title = {Invariant Generation for Parametrized Systems using Self-Reflection},
year = {2012},
pages = {146-163},
publisher = {Springer-Verlag},
booktitle = {Static Analysis Symposium (SAS)},
series = {Lecture Notes in Computer Science},
volume = {7460},
}

We consider different piecewise linear (PWL) models for nonlinear devices in the context of formal DC operating point and transient analyses of analog circuits. PWL models allow us to encode a verification problem as constraints in linear arithmetic, which can be solved efficiently using modern SMT solvers. Numerous approaches to piecewise linearization are possible, including piecewise constant, simplicial piecewise linearization and canonical piecewise linearization. We address the question of which PWL modeling approach is the most suitable for formal verification by experimentally evaluating the performance of various PWL models in terms of running time and accuracy for the DC operating point and transient analyses of several analog circuits. Our results are quite surprising: piecewise constant (PWC) models, the simplest approach, seem to be the most suitable in terms of the trade-off between modeling precision and the overall analysis time. Contrary to expectations, more sophisticated device models do not necessarily provide significant gains in accuracy, and may result in increased running time. We also present evidence suggesting that PWL models may not be suitable for certain transient analyses.

@InProceedings{Zhang+Sankaranarayanan+Somenzi-2012-Piecewise,
author = {Yan Zhang and Sriram Sankaranarayanan and Fabio Somenzi},
title = {Piecewise linear modeling of nonlinear devices for formal verification of analog circuits},
year = {2012},
pages = {196-203},
publisher = {IEEE Press},
booktitle = {Formal Methods in Computer-Aided Design ( FMCAD 2012 )},
}

We present a model-based approach to synthesizing insulin infusion pump usage parameters against varying meal scenarios and physiological conditions. Insulin infusion pumps are commonly used by type-1 diabetic patients to control their blood glucose levels. The amounts of insulin to be infused are calculated based on parameters such as insulin-to-carbohydrate ratios and correction factors that need to be calibrated carefully for each patient. Frequent and careful calibration of these parameters is essential for avoiding complications such as hypoglycemia and hyperglycemia. In this paper, we propose to synthesize optimal parameters for meal bolus calculation starting from models of the patient's insulin-glucose regulatory system and the infusion pump. Various off-the-shelf global optimization techniques are used to search for parameter values that minimize a penalty function defined over the predicted glucose sensor readings. The penalty function “rewards” glucose levels that lie within the prescribed ranges and “penalizes” the occurrence of hypoglycemia and hyperglycemia. We evaluate our approach using a model of the insulin-glucose regulatory system proposed by Dalla Man et al. Using this model, we compare various strategies for optimizing pump usage parameters for a virtual population of in-silico patients.

Invited Paper appeared in special session on Cyber-Physical Systems

@InProceedings{Sankaranarayanan+Miller+Raghunathan+Ravanbakhsh+Fainekos-2012-Model,
author = {Sriram Sankaranarayanan and Christopher Miller and Rangarajan Raghunathan and Hadi Ravanbakhsh and Georgios E. Fainekos},
title = {A model-based approach to synthesizing insulin infusion pump usage parameters for diabetic patients},
year = {2012},
pages = {1610-1617},
publisher = {IEEE Press},
booktitle = {Allerton Conference},
}

Electronic, software-managed mechanisms using, for example, radio-frequency identification (RFID) cards, enable great flexibility in specifying access control policies to physical spaces. For example, access rights may vary based on time of day or could differ in normal versus emergency situations. With such fine-grained control, understanding and reasoning about what a policy permits becomes surprisingly difficult requiring knowledge of permission levels, spatial layout, and time. In this paper, we present a formal modeling framework, called Access Nets, suitable for describing a combination of access permissions, physical spaces, and temporal constraints. Furthermore, we provide evidence that model checking techniques are effective in reasoning about physical access control policies. We describe our results from a tool that uses reachability analysis to validate security policies.

supplementary materials: tar.gz , requires YICES SMT solver from SRI.

@InProceedings{Frohardt+Others-2011-Access,
author = {Robert Frohardt and Bor-Yuh Evan Chang and Sriram Sankaranarayanan},
title = {Access Nets: Modeling Access to Physical Spaces},
year = {2011},
pages = {184-198},
publisher = {Springer-Verlag},
booktitle = {Verification, Model Checking, and Abstract Interpretation (VMCAI)},
series = {Lecture Notes in Computer Science},
volume = {6538},
}

Infusion pumps are commonly used in home/hospital care to inject drugs into a patient at programmable rates over time. However, in practice, a combination of faults including software errors, mechanical failures and human error can lead to catastrophic situations, causing death or serious harm to the patient. Dependability analysis techniques such as failure mode effect analysis (FMEA) can be used to predict the worst case outcomes of such faults and facilitate the development of remedies against them. In this paper, we present the use of model-checking to automate the dependability analysis of programmable, real-time medical devices. Our approach uses timed and hybrid automata to model the real-time operation of the medical device and its interactions with the care giver and the patient. Common failure modes arising from device failures and human error are modeled in our framework. Specifically, we use “mistake models” derived from human factor studies to model the effects of mistakes committed by the operator. We present a case-study involving an infusion pump used to manage pain through the infusion of analgesic drugs. The dynamics of analgesic drugs are modeled by empirically validated pharmacokinetic models. Using model checking, our technique can systematically explore numerous combinations of failures and characterize the worse case effects of these failures.

Our infusion pump analysis project has more details.

@InProceedings{Sankaranarayanan+Others-2011-Model,
author = {Sriram Sankaranarayanan and Hadjar Homaei and Clayton Lewis},
title = {Model-Based Dependability Analysis of Programmable Drug Infusion Pumps},
year = {2011},
pages = {317-334},
publisher = {},
booktitle = {Formal Methods for Timed Systems (FORMATS)},
series = {Lecture Notes in Computer Science},
volume = {6919},
}

Software model checking and static analysis have matured over the last decade, enabling their use in automated software verification. However, lack of scalability makes these tools hard to apply. Furthermore, approximations in the models of program and environment lead to a profusion of false alarms. This paper proposes DC2, a verification framework using scope-bounding to bridge these gaps. DC2 splits the analysis problem into manageable parts, relying on a combination of three automated techniques: (a) techniques to infer useful specifications for functions in the form of pre- and post-conditions; (b) stub inference techniques that infer abstractions to replace function calls beyond the verification scope; and (c) automatic refinement of pre- and post-conditions from false alarms identified by a user. DC2 enables iterative reasoning over the calling environment, to help in finding non-trivial bugs and fewer false alarms. We present an experimental evaluation that demonstrates the effectiveness of DC2 on several open-source and industrial software projects.

@InProceedings{IvancicBGSMTIM11,
author = {Franjo Ivancic and Gogul Balakrishnan and Aarti Gupta and Sriram Sankaranarayanan and Naoto Maeda and Hiroki Tokuoka and Takashi Imoto and Yoshiaki Miyazaki},
title = {DC2: A framework for scalable, scope-bounded software verification},
year = {2011},
pages = {133-142},
publisher = {IEEE Press},
booktitle = {Automated Software Engg. (ASE)},
}

S-TaLiRo is a Matlab (TM) toolbox that searches for trajectories of minimal robustness in Simulink/Stateflow diagrams. It can analyze arbitrary Simulink models or user defined functions that model the system. At the heart of the tool, we use randomized testing based on stochastic optimization techniques including Monte-Carlo methods and Ant-Colony Optimization. Among the advantages of the toolbox is the seamless integration inside the Matlab environment, which is widely used in the industry for model-based development of control software. We present the architecture of S-TaLiRo and its working on an application example.

S-Taliro tool available online

@InProceedings{Annapureddy+Others-2011-STaliro,
author = {Yashwanth Annpureddy and Che Liu and Georgios E. Fainekos and Sriram Sankaranarayanan},
title = {S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems},
year = {2011},
pages = {254-257},
publisher = {Springer},
booktitle = {Tools and Algorithms for Construction and Analysis of Systems (TACAS)},
series = {Lecture Notes in Computer Science},
volume = {6605},
}

Methods in object-oriented concurrent libraries often encapsulate internal synchronization details. As a result of information hiding, clients calling the library methods may cause thread safety violations by invoking methods in an unsafe manner. This is frequently a cause of deadlocks. Given a concurrent library, we present a technique for inferring interface contracts that specify permissible concurrent method calls and patterns of aliasing among method arguments. In this work, we focus on deriving contracts that guarantee deadlock-free execution for the methods in the library. The contracts also help client developers by documenting required assumptions about the library methods. Alternatively, the contracts can be statically enforced in the client code to detect potential deadlocks in the client. Our technique combines static analysis with a symbolic encoding scheme for tracking lock dependencies, allowing us to synthesize contracts using a SMT solver. Additionally, we investigate extensions of our technique to reason about deadlocks in libraries that employ signaling primitives such as wait-notify for cooperative synchronization. Our prototype tool analyzes over a million lines of code for some widely-used Java libraries within an hour, thus demonstrating its scalability and efficiency. Furthermore, the contracts inferred by our approach have been able to pinpoint real deadlocks in clients, i.e. deadlocks that have been a part of bug-reports filed by users and developers of client code.

Journal version of ASE 2009 paper. DOI:10.1007/s10515-011-0085-0

@Article{Deshmukh+Emerson+Sankaranarayanan-2011-Symbolic,
author = {Jyotirmoy V. Deshmukh and E. Allen Emerson and Sriram Sankaranarayanan},
title = {Symbolic modular deadlock analysis},
year = {2011},
pages = {325-362},
publisher = {},
journal = {Autom. Softw. Eng.},
number = {3-4},
volume = {18},
}

We present techniques for determining the precision gap between Andersen's points-to analysis and precise flow-insensitive points-to analysis in practice. While previous work has shown that such a gap may exist, no efficient algorithm for precise flow-insensitive analysis is known, making measurement of the gap on real-world programs difficult. We give an algorithm for precise flow-insensitive analysis of programs with finite memory, based on a novel technique for refining any points-to analysis with a search for flow-insensitive witnesses. We give a compact symbolic encoding of the technique that enables computing the search using a tuned SAT solver. We also present extensions of the algorithm that enable computing lower and upper bounds on the precision gap in the presence of dynamic memory allocation. In our experimental evaluation over a suite of small- to medium-sized C programs, we never observed a precision gap between Andersen's analysis and the precise analysis. In other words, Andersen's analysis computed a precise flow-insensitive result for all of our benchmarks. Hence, we conclude that while better algorithms for the precise flow-insensitive analysis are still of theoretical interest, their practical impact for C programs is likely to be negligible.

@InProceedings{Blackshear+Others-2011-Flow,
author = {Sam Blackshear and Bor-Yuh Evan Chang and Sriram Sankaranarayanan and Manu Sridharan},
title = {The Flow-Insensitive Precision of Andersen's Analysis in Practice},
year = {2011},
pages = {60-76},
publisher = {},
booktitle = {SAS},
series = {Lecture Notes in Computer Science},
volume = {6887},
}

In this paper, we define relational abstractions of hybrid systems. A relational abstraction is obtained by replacing the continuous dynamics in each mode by a binary transition relation that relates a state of the system to any state that can potentially be reached at some future time instant using the continuous dynamics. We construct relational abstractions by reusing template-based invariant generation techniques for continuous systems described by Ordinary Differential Equations (ODE). As a result, we abstract a given hybrid system as a purely discrete, infinite-state system. We apply k-induction to this abstraction to prove safety properties, and use bounded model-checking to find potential falsifications. We present the basic underpinnings of our approach and demonstrate its use on many benchmark systems to derive simple and usable abstractions.

Supplementary Materials Available here and here.

@InProceedings{Tiwari+Sankaranarayanan-2011-Relational,
author = {Sriram Sankaranarayanan and Ashish Tiwari},
title = {Relational Abstractions for Continuous and Hybrid Systems},
year = {2011},
pages = {686-702},
publisher = {Springer-Verlag},
booktitle = {Computer-Aided Verification (CAV)},
series = {Lecture Notes in Computer Science},
volume = {6806},
}

Template polyhedra generalize weakly relational domains by specifying arbitrary fixed linear expressions on the left-hand sides of inequalities and undetermined constants on the right. The domain operations required for analysis over template polyhedra can be computed in polynomial time using linear programming. In this paper, we introduce the generalized template polyhedral domain that extends template polyhedra using fixed left-hand side expressions with bilinear forms involving program variables and unknown parameters to the right. We prove that the domain operations over generalized templates can be defined as the ‘‘best possible abstractions’’ of the corresponding polyhedral domain operations. The resulting analysis can straddle the entire space of linear relation analysis starting from the template domain to the full polyhedral domain. We show that analysis in the generalized template domain can be performed by dualizing the join, post-condition and widening operations. We also investigate the special case of template polyhedra wherein each bilinear form has at most two parameters. For this domain, we use the special properties of two dimensional polyhedra and techniques from fractional linear programming to derive domain operations that can be implemented in polynomial time over the number of variables in the program and the size of the polyhedra. We present applications of generalized template polyhedra to strengthen previously obtained invariants by converting them into templates. We describe an experimental evaluation of an implementation over several benchmark systems.

@InProceedings{Colon+Sankaranarayanan-2011-Generalizing,
author = {Michael Colon and Sriram Sankaranarayanan},
title = {Generalizing the Template Polyhedral Domain},
year = {2011},
pages = {176-195},
publisher = {Springer-Verlag},
booktitle = {European Symposium on Programming (ESOP)},
series = {Lecture Notes in Computer Science},
volume = {6602},
}

In this paper, we investigate formalisms for specifying periodic signals using time and frequency domain specifications along with algorithms for the signal recognition and generation problems for such specifications. The time domain specifications are in the form of hybrid automata whose continuous state variables generate the desired signals. The frequency domain specifications take the form of an “envelope” that constrains the possible power spectra of the periodic signals with a given frequency cutoff. The combination of time and frequency domain specifications yields mixed-domain specifications that constrain a signal to belong to the intersection of the both specifications. We show that the signal recognition problem for periodic signals specified by hybrid automata is NP-complete, while the corresponding problem for frequency domain specifications can be approximated to any desired degree by linear programs, which can be solved in polynomial time. The signal generation problem for time and frequency domain specifications can be encoded into linear arithmetic constraints that can be solved using existing SMT solvers. We present some preliminary results based on an implementation that uses the SMT solver Z3 to tackle the signal generation problems.

Link to the published version

@InProceedings{Chakarov+Sankaranarayanan+Fainekos-2011-Combining,
author = {Aleksandar Chakarov and Sriram Sankaranarayanan and Georgios E. Fainekos},
title = {Combining Time and Frequency Domain Specifications for Periodic Signals},
year = {2011},
pages = {294-309},
publisher = {Springer-Verlag},
booktitle = {Runtime Verification (RV)},
series = {Lecture Notes in Computer Science (LNCS)},
volume = {7186},
}

The inclusion-exclusion principle is a well-known mathematical principle used to count the number of elements in the union of a collection of sets in terms of intersections of sub-collections.We present an algorithm for counting the number of solutions of a given k-SAT formula using the inclusion-exclusion principle. The key contribution of our work consists of a novel subsumption pruning technique. Subsumption pruning exploits the alternating structure of the terms involved in the inclusion-exclusion principle to discover term cancellations that can account for the individual contributions of a large number of terms in a single step.

Huck Bennett's MS thesis (Chapter 3) has more details, including some generalizations to Bonferroni inequalities.

@InProceedings{Bennett+Sankaranarayanan-2011-Model,
author = {Huxley Bennett and Sriram Sankaranarayanan},
title = {Model Counting Using the Inclusion-Exclusion Principle},
year = {2011},
pages = {362-363},
publisher = {Springer-Verlag},
booktitle = {Theory and Applications of Satisfiability Testing - SAT 2011},
series = {Lecture Notes in Computer Science},
volume = {6695},
}

We present abstraction techniques that transform a given non-linear dynamical system into a linear system, such that, invariant properties of the resulting linear abstraction can be used to infer invariants for the original system. The abstraction techniques rely on a change of bases transformation that associates each state variable of the abstract system with a function involving the state variables of the original system. We present conditions under which a given change of basis transformation for a non-linear system can define an abstraction.

Furthermore, we present a technique to discover, given a non-linear system, if a change of bases transformation involving degree-bounded polynomials yielding a linear system abstraction exists. If so, our technique yields the resulting abstract linear system, as well. This approach is further extended to search for a change of bases transformation that abstracts a given non-linear system into a system of linear differential inclusions. Our techniques enable the use of analysis techniques for linear systems to infer invariants for non-linear systems. We present preliminary evidence of the practical feasibility of our ideas using a prototype implementation.

Please see extended version

@InProceedings{Sankaranarayanan-2011-Automatic,
author = {Sriram Sankaranarayanan},
title = {Automatic Abstraction of Non-Linear Systems Using Change of Variables Transformations},
year = {2011},
pages = {143-152},
publisher = {ACM Press},
booktitle = {Hybrid Systems: Computation and Control (HSCC)},
}

We present a Monte-Carlo optimization technique for finding inputs to a system that falsify a given Metric Temporal Logic (MTL) property. Our approach performs a random walk over the space of inputs guided by a robustness metric defined by the MTL property. Robustness can be used to guide our search for a falsifying trajectory by exploring trajectories with smaller robustness values. We show that the notion of robustness can be generalized to consider hybrid system trajectories. The resulting testing framework can be applied to non-linear hybrid systems with external inputs. We show through numerous experiments on complex systems that using our framework can help automatically falsify properties with more consistency as compared to other means such as uniform sampling.

@InProceedings{Nghiem+Sankaranarayanan+Others-2010-Monte-Carlo,
author = {Truong Nghiem and Sriram Sankaranarayanan and Georgios E. Fainekos and Franjo Ivancic and Aarti Gupta and George J. Pappas},
title = {Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems},
year = {2010},
pages = {211-220},
publisher = {ACM Press},
booktitle = {Hybrid Systems: Computation and Control},
}

We propose a novel integration of interval constraint propagation (ICP) with SMT solvers for linear real arithmetic (LRA) to decide nonlinear real arithmetic problems. We use ICP to search for interval solutions of the nonlinear constraints, and use the LRA solver to either validate the solutions or provide constraints to incrementally refine the search space for ICP. This serves the goal of separating the linear and nonlinear solving stages, and we show that the proposed methods preserve the correctness guarantees of ICP. Experimental results show that such separation is useful for enhancing efficiency.

@InProceedings{Gao+Others-2010-Integrating,
author = {Sicun Gao and Malay K. Ganai and Franjo Ivancic and Aarti Gupta and Sriram Sankaranarayanan and Edmund M. Clarke},
title = {Integrating {ICP} and {LRA} Solvers for Deciding Nonlinear Real Arithmetic Problems},
year = {2010},
pages = {81-89},
publisher = {IEEE Press},
booktitle = {Formal Methods for Computer-Aided Design (FMCAD)},
}

We present computational techniques for automatically generating algebraic (polynomial equality) invariants for algebraic hybrid systems. Such systems involve ordinary differential equations with multivariate polynomial right-hand sides. Our approach casts the problem of generating invariants for differential equations as the greatest fixed point of a monotone operator over the lattice of ideals in a polynomial ring. We provide an algorithm to compute this monotone operator using basic ideas from commutative algebraic geometry. However, the resulting iteration sequence does not always converge to a fixed point, since the lattice of ideals over a polynomial ring does not satisfy the descending chain condition. We then present a bounded-degree relaxation based on the concept of ‘‘pseudo ideals’’, due to Colon, that restricts ideal membership using multipliers with bounded degrees. We show that the monotone operator on bounded degree pseudo ideals is convergent and generates fixed points that can be used to generate useful algebraic invariants for non-linear systems. The technique for continuous systems is then extended to consider hybrid systems with multiple modes and discrete transitions between modes. We have implemented the exact, non-convergent iteration over ideals in combination with the bounded degree iteration over pseudo ideals to guarantee convergence. This has been applied to automatically infer useful and interesting polynomial invariants for some benchmark non-linear systems

@InProceedings{Sankaranarayanan-2010-Automatic,
author = {Sriram Sankaranarayanan},
title = {Automatic Invariant Generation for Hybrid Systems using Ideal Fixed Points},
year = {2010},
pages = {211-230},
publisher = {ACM Press},
booktitle = {Hybrid Systems: Computation and Control},
}

Software model checking has recently been successful in discovering bugs in production software. Most tools have targeted heap related programming mistakes and control-heavy programs. However, real-time and embedded controllers implemented in software are susceptible to computational numeric instabilities. We target verification of numerical programs that use floating-point types, to detect loss of numerical precision incurred in such programs. Techniques based on abstract interpretation have been used in the past for such analysis. We use bounded model checking (BMC) based on Satisfiability Modulo Theory (SMT) solvers, which work on a mixed integer-real model that we generate for programs with floating points. We have implemented these techniques in our software verification platform. We report experimental results on benchmark examples to study the effectiveness of model checking on such problems, and the effect of various model simplifications on the performance of model checking.

@InProceedings{Ivancic+Others-2010-Numerical,
author = {Franjo Ivancic and Malay Ganai and Sriram Sankaranarayanan and Aarti Gupta},
title = {Numerical stability analysis of floating-point computations using software model checking},
year = {2010},
pages = {49-58},
publisher = {},
booktitle = {Formal Methods and Models for Codesign (MEMOCODE)},
}

Path-sensitivity is often a crucial requirement for verifying safety properties of programs. As it is infeasible to enumerate and analyze each path individually, analyses compromise by soundly merging information about executions along multiple paths. However, this frequently results in a loss of precision. We present a program analysis technique that we call Satisfiability Modulo Path Programs (SMPP), based on a path-based decomposition of a program. It is inspired by insights that have driven the development of modern SMT(Satisfiability Modulo Theory) solvers. SMPP symbolically enumerates path programs using a SAT formula over control edges in the program. Each enumerated path program is verified using an oracle, such as abstract interpretation or symbolic execution, to either find a proof of correctness or report a potential violation. If a proof is found, then SMPP extracts a sufficient set of control edges and corresponding interference edges, as a form of proof-based learning. Blocking clauses derived from these edges are added back to the SAT formula to avoid enumeration of other path programs guaranteed to be correct, thereby improving performance and scalability. We have applied SMPP in the F-Soft program verification framework, to verify properties of real-world C programs that require path-sensitive reasoning. Our results indicate that the precision from analyzing individual path programs, combined with their efficient enumeration by SMPP, can prove properties as well as indicate potential violations in the large.

@InProceedings{Harris+Others-2010-Satisfiability,
author = {William R. Harris and Sriram Sankaranarayanan and Franjo Ivancic and Aarti Gupta},
title = {Satisfiability Modulo Path Programs},
year = {2010},
pages = {71-82},
publisher = {ACM Press},
booktitle = {ACM Principles of Programming Languages (POPL’10)},
}

We propose a static analysis framework for concurrent programs based on reduction of thread interleavings using sound invariants on the top of partial order techniques. Starting from a product graph that represents transactions, we iteratively refine the graph to remove statically unreachable nodes in the product graph using the results of these analyses. We use abstract interpretation to automatically derive program invariants, based on abstract domains of increasing precision. We demonstrate the benefits of this framework in an application to find data race bugs in concurrent programs, where our static analyses serve to reduce the number of false warnings captured by an initial lockset analysis. This framework also facilitates use of model checking on the remaining warnings to generate concrete error traces, where we leverage the preceding static analyses to generate small program slices and the derived invariants to improve scalability. We describe our experimental results on a suite of Linux device drivers.

@InProceedings{Kahlon+Others-2009-Semantic,
author = {Vineet Kahlon and Sriram Sankaranarayanan and Aarti Gupta},
title = {Semantic Reduction of Thread Interleavings in Concurrent Programs},
year = {2009},
pages = {124-138},
publisher = {},
booktitle = {TACAS},
series = {Lecture Notes in Computer Science},
volume = {5505},
}

We present a methodology and a toolkit for improving simulation coverage of SimulinkStateflow models of hybrid systems using symbolic analysis of simulation traces. We propose a novel instrumentation scheme that allows the simulation engine of SimulinkStateflow to output, along with the concrete simulation trace, the symbolic transformers needed for our analysis. Given a simulation trace, along with the symbolic transformers, our analysis computes a set of initial states that would lead to traces with the same sequence of discrete components at each step of the simulation. Such an analysis relies critically on the use of convex polyhedra to represent sets of states. However, the exponential complexity of the polyhedral operations implies that the performance of the analysis would degrade rapidly with the increasing size of the model and the simulation traces. We propose a new representation, called the bounded vertex representation, which allows us to perform under-approximate computations while fixing the complexity of the representation a priori. Using this representation we achieve a trade-off between the complexity of the symbolic computation and the quality of the under-approximation. We demonstrate the benefits of our approach over existing simulation and verification methods with case studies.

@InProceedings{Kanade+Others-2009-Generating,
author = {Aditya Kanade and Rajeev Alur and Franjo Ivancic and S. Ramesh and Sriram Sankaranarayanan and K. C. Shashidhar},
title = {Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models},
year = {2009},
pages = {430-445},
publisher = {Springer-Verlag},
booktitle = {Computer-Aided Verification (CAV)},
series = {Lecture Notes in Computer Science},
volume = {5643},
}

We present a simple yet useful technique for refining the control structure of loops that occur in imperative programs. Loops containing complex control flow are common in synchronous embedded controllers derived from modelling languages such as Lustre, Esterel, and Simulink/Stateflow. Our approach uses a set of labels to distinguish different control paths inside a given loop. The iterations of the loop are abstracted as a finite state automaton over these labels. We then use static analysis techniques to identify infeasible iteration sequences. Such forbidden sequences are subtracted from the initial language to obtain a refinement. In practice, the refinement of control flow sequences often simplifies the control flow patterns in the loop, identifying nested loops, unrolling and unwinding automatically. We have applied the refinement technique to improve the precision of abstract interpretation in the presence of widening. Our experiments on a set of complex reactive loop benchmarks clearly show the utility of our refinement techniques. Other potentially useful applications include termination analysis and reverse engineering models from source code.

@InProceedings{Balakrishnan+Others-2009-Refining,
author = {Gogul Balakrishnan and Sriram Sankaranarayanan and Franjo Ivancic and Aarti Gupta},
title = {Refining the control structure of loops using static analysis},
year = {2009},
pages = {49-58},
publisher = {ACM Press},
booktitle = {Embedded Software (EMSOFT)},
}

This paper proposes a framework for determining the correctness and robustness of simulations of hybrid systems. The focus is on simulations generated from model-based design environments and, in particular, Simulink. The correctness and robustness of the simulation is guaranteed against floating-point rounding errors and system modeling uncertainties. Toward that goal, self-validated arithmetics, such as interval and affine arithmetic, are employed for guaranteed simulation of discrete-time hybrid systems. In the case of continuous-time hybrid systems, self-validated arithmetics are utilized for over-approximations of reachability computations.

@InProceedings{Fainekos+Others-2009-Robustness,
author = {Georgios E. Fainekos and Sriram Sankaranarayanan and Franjo Ivancic and Aarti Gupta},
title = {Robustness of Model-Based Simulations},
year = {2009},
pages = {345-354},
publisher = {IEEE Press},
booktitle = {Real-Time Systems Symposium (RTSS)},
}

Methods in object-oriented concurrent libraries hide internal synchronization details. However, information hiding may result in clients causing thread safety violations by invoking methods in an unsafe manner. Given such a library, we present a technique for inferring interface contracts that specify permissible concurrent method calls and patterns of aliasing among method arguments, such that the derived contracts guarantee deadlock free execution for the methods in the library. The contracts also help client developers by documenting required assumptions about the library methods. Alternatively, the contracts can be statically enforced in the client code to detect potential deadlocks in the client. Our technique combines static analysis with a symbolic encoding for tracking lock dependencies, allowing us to synthesize contracts using a SMT solver. Our prototype tool analyzes over a million lines of code for some widely-used Java libraries within an hour, thus demonstrating its scalability and efficiency. Furthermore, the contracts inferred by our approach have been able to pinpoint real deadlocks in clients, i.e. deadlocks that have been a part of bug-reports filed by users and developers of the client code.

ACM SIGSOFT distinguished paper award

@InProceedings{Deshmukh+Others-2009-Symbolic,
author = {Jyotirmoy Deshmukh and E. Allen Emerson and Sriram Sankaranarayanan},
title = {Symbolic Deadlock Analysis in Concurrent Libraries and their Clients},
year = {2009},
pages = {480-491},
publisher = {ACM Press},
booktitle = {Automated Software Engg. (ASE)},
}

As networked systems grow in complexity, they are increasingly vulnerable to denial-of-service (DoS) attacks involving resource exhaustion. A single malicious ‘‘input of coma’’ can trigger high-complexity behavior such as deep recursion in a carelessly implemented server, exhausting CPU time or stack space and making the server unavailable to legitimate clients. These DoS attacks exploit the semantics of the target application, are rarely associated with network traffic anomalies, and are thus extremely difficult to detect using conventional methods. We present SAFER, a static analysis tool for identifying potential DoS vulnerabilities and the root causes of resource-exhaustion attacks before the software is deployed. Our tool combines taint analysis with control dependency analysis to detect high-complexity control structures whose execution can be triggered by untrusted network inputs. When evaluated on real-world networked applications, SAFER discovered previously unknown DoS vulnerabilities in the expat XML parser and the SQLite library, as well as a new attack on a previously patched version of the wu-ftpd server. This demonstrates the importance of understanding and repairing the root causes of DoS vulnerabilities rather than simply blocking known malicious inputs.

@InProceedings{Chang+Jiang+Ivancic+Sankaranarayanan+Shmatikov-2009-Inputs,
author = {Richard Chang and Guofei Jiang and Franjo Ivancic and Sriram Sankaranarayanan and Vitaly Shmatikov},
title = {Inputs of Coma: Static Detection of Denial-of-Service Vulnerabilities},
year = {2009},
pages = {186-199},
publisher = {IEEE Press},
booktitle = {Computer Security Foundations (CSF)},
}

We present a technique for detecting semantically infeasible paths in programs using abstract interpretation. Our technique uses a sequence of path-insensitive forward and backward runs of an abstract interpreter to infer paths in the CFG that cannot be exercised in concrete executions of the program. We then present a syntactic language refinement (SLR) technique that automatically excludes semantically infeasible paths from the program during the static analysis. This allows us to iteratively prove more properties. Specifically, our technique simulates the effect of a path-sensitive analysis by performing syntactic language refinement over an underlying path-insensitive static analyzer. Finally, we present experimental results to quantify the impact of our technique on an abstract interpreter for C programs.

@InProceedings{Balakrishnan+Others-08-SLR,
author = {Gogul Balakrishnan and Sriram Sankaranarayanan and Franjo Ivancic and Ou Wei and Aarti Gupta},
title = {SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic Language Refinement},
year = {2008},
pages = {238-254},
publisher = {Springer-Verlag},
booktitle = {SAS},
series = {Lecture Notes in Computer Science},
volume = {5079},
}

We propose techniques for the verification of hybrid systems using template polyhedra, i.e., polyhedra whose inequalities have fixed expressions but with varying constant terms. Given a hybrid system description and a set of template linear expressions as inputs, our technique constructs over-approximations of the reachable states using template polyhedra. The advantages of using template polyhedra are that operations used in symbolic model checking such as intersection, union and post-condition across discrete transitions over template polyhedra can be computed efficiently without using expensive vertex enumeration. Additionally, the verification of hybrid systems requires techniques to handle the continous dynamics inside locations. A key contribution of the paper is a new flowpipe construction algorithm using template polyhedra. Our technique uses higher-order Taylor series approximations along with repeated optimization problems to bound the terms in the Taylor series expansion. The location invariant is used to enclose the remainder term of the Taylor series, and thus make our technique sound. As a result, we can compute flowpipe segments using template polyhedra that leads to a precise treatment of the continuous dynamics. Finally, we have implemented our approach as a part of the tool TimePass for verifying reachability properties of affine hybrid automata.

@InProceedings{Sankaranarayanan+Dang+Ivancic-08-Symbolic,
author = {Sriram Sankaranarayanan and Thao Dang and Franjo Ivancic},
title = {Symbolic Model Checking of Hybrid Systems Using Template Polyhedra},
year = {2008},
pages = {188-202},
publisher = {Springer-Verlag},
booktitle = {TACAS},
series = {Lecture Notes in Computer Science},
volume = {4963},
}

In this paper, we present a policy iteration technique that computes an over-approximation of the time trajectories of a system using template polyhedra. Such polyhedra are obtained by conjoining a set of inequality templates with varying constant coefficients. Given a set of template expressions, we show the existence of a smallest template polyhedron that is a positive invariant w.r.t to the dynamics of the continuous variables, and hence, an over-approximation the time trajectories. Thus, we derive a time elapse operator for template polyhedra using policy iteration that computes tight over-approximations of the time trajectories. We exploit the result of the policy iteration to improve the precision of Taylor series-based flowpipe construction. Finally, we incorporate our ideas inside a prototype tool for safety verification of affine hybrid systems, with promising results on benchmarks.

@InProceedings{Sankaranarayanan+Dang+Ivancic-08-Policy,
author = {Sriram Sankaranarayanan and Thao Dang and Franjo Ivancic},
title = {A Policy Iteration Technique for Time Elapse over Template Polyhedra},
year = {2008},
pages = {654-657},
publisher = {Springer-Verlag},
booktitle = {HSCC},
series = {Lecture Notes in Computer Science},
volume = {4981},
}

An invariant of a system is a predicate that holds for every reachable state. In this paper, we present techniques to generate invariants for hybrid systems. This is achieved by reducing the invariant generation problem to a constraint solving problem using methods from the theory of ideals over polynomial rings. We extend our previous work on the generation of algebraic invariants for discrete transition systems in order to generate algebraic invariants for hybrid systems. In doing so, we present a new technique to handle consecution across continuous differential equations. The techniques we present allow a trade-off between the complexity of the invariant generation process and the strength of the resulting invariants.

Special Issue For HSCC 2004

@Article{FMSD-Inv,
author = {Sriram Sankaranarayanan and Henny Sipma and Zohar Manna},
title = {Constructing Invariants for Hybrid Systems},
year = {2008},
pages = {25-55},
publisher = {},
journal = {Formal Methods in System Design},
number = {1},
volume = {32},
}

We present a technique to learn data preconditions for procedures written in an imperative programming language. Given a procedure and an set of predicates over its inputs, our technique enumerates different truth assignments to the predicates, deriving test cases from each feasible truth assignment. The predicates themselves are provided by the user and/or automatically produced from the program description using heuristics. The enumeration of truth assignments is performed by using randomized SAT solvers with a theory satisfiability checker capable of generating unsatisfiable cores. For each combination of truth values chosen by our sampler, the corresponding set of test cases are generated and exectued. Based on the result of the execution, the truth combination is classified as safe or buggy. Finally, a decision tree classifier is used to generate a boolean formula over the input predicates that explains the truth table generated in this process. The resulting boolean formula forms a precondition for the function under test. We apply our techniques on a wide variety of functions, including functions in the standard C library. Our experiments show that the proposed learning technique is quite robust. In many cases, it successfully learns a precondition that captures a safe and permissive calling environment required for the execution of the function.

@InProceedings{Sankaranarayanan+Others-08-Dynamic,
author = {Sriram Sankaranarayanan and Swarat Chaudhuri and Franjo Ivancic and Aarti Gupta},
title = {Dynamic inference of likely data preconditions over predicates by tree learning},
year = {2008},
pages = {295-306},
publisher = {ACM Press},
booktitle = {ISSTA},
}

Software libraries are ubiquitous for organizing widely useful functionalities in order to promote modularity and code reuse. A typical software library is used by client programs through an API that hides library internals from the client. Typically, the rules governing the correct usage of the API are documented informally. As a result, the behaviour of the library under some corner cases may not be well understood by the programmer. We propose a methodology for learning interface specifications using inductive logic programming (ILP). Our technique runs several unit tests on the library in order to generate relations describing the operation of the library. The data collected from these tests are used by an inductive learner to obtain rich Prolog specifications. Such specifications capture essential properties of the library. They may be used for applications such as reverse engineering, and also to construct checks on that enforce proper API usage.

@InProceedings{Sankaranarayanan+Others-08-Mining,
author = {Sriram Sankaranarayanan and Franjo Ivancic and Aarti Gupta},
title = {Mining library specifications using inductive logic programming},
year = {2008},
pages = {131-140},
publisher = {ACM Press},
booktitle = {Intl. Symp. on Software Engg. (ICSE)},
}

Interval analysis seeks static lower and upper bounds on the values of program variables. These bounds are useful, especially for inferring invariants to prove buffer overflow checks. In practice, however, intervals by themselves are inadequate as invariants due to the lack of relational information among the variables. In this paper, we present a technique for deriving symbolic bounds on the variable values. We study a restricted class of polyhedra whose constraints are stratified with respect to some variable ordering provided by the user, or chosen heuristically. We define a notion of normalization for such constraints and demonstrate polynomial time domain operations on the resulting domain of symbolic range constraints. The abstract domain is intended to complement widely used domains such as intervals and octagons for use in buffer overflow analysis. Finally, we study the impact of our analysis on commercial software using an overflow analyzer for the C language.

@InProceedings{Sankaranarayanan+Others-07-Program,
author = {Sriram Sankaranarayanan and Franjo Ivancic and Aarti Gupta},
title = {Program Analysis Using Symbolic Ranges},
year = {2007},
pages = {366-383},
publisher = {},
booktitle = {SAS},
series = {Lecture Notes in Computer Science},
volume = {4634},
}

We present new techniques for fast, accurate and scalable static race detection in concurrent programs. Focusing our analysis on Linux device drivers allowed us to identify the unique challenges posed by debugging large-scale real-life code and also pinpointed drawbacks in existing race warning generation methods. This motivated the development of new techniques that helped us in improving both the scalability as well as the accuracy of each of the three main steps in a race warning generation system. The first and most crucial step in data race detection is automatic shared variable discovery. Towards that end, we present a new, efficient dataflow algorithm for shared variable detection which is more effective than existing correlation-based techniques that failed to detect shared variables responsible for data races in majority of the drivers in our benchmark suite. Secondly, accuracy of race warning generation strongly hinges on the accuracy of the alias analysis used to compute aliases for lock pointers. We formulate a new scalable context sensitive alias analysis that effectively combines a divide and conquer strategy with function summarization and is demonstrably more efficient than existing BDD-based techniques. Finally, we provide a new warning reduction technique that leverages lock acquisition patterns to yield provably better warning reduction than existing lockset based methods.

@InProceedings{Kahlon+Others-07-Fast,
author = {Vineet Kahlon and Yu Yang and Sriram Sankaranarayanan and Aarti Gupta},
title = {Fast and Accurate Static Data-Race Detection for Concurrent Programs},
year = {2007},
pages = {226-239},
publisher = {},
booktitle = {Computer-Aided Verification (CAV)},
series = {Lecture Notes in Computer Science},
volume = {4590},
}

We study techniques for synthesizing synchronous controllers for affine plants with disturbances, based on safety specifications. Our plants are modeled in terms of discrete linear systems whose variables are partitioned into system, control, and disturbance variables. We synthesize non-blocking controllers that satisfy a user-provided safety specification by means of a fixed point iteration over the control precondition state transformer. Using convex polyhedra to represent sets of states, we present both precise and approximate algorithms for computing control precon- ditions and discuss strategies for forcing convergence of the iteration. We present technique for automatically deriving controllers from the result of the analysis, and demonstrate our approach on examples.

@Article{Slanina+Others-2007-Controller,
author = {Matteo Slanina and Sriram Sankaranarayanan and Henny B. Sipma and Zohar Manna},
title = {Controller Synthesis of Discrete Linear Plants Using Polyhedra},
year = {2007},
pages = {1-14},
publisher = {},
journal = {REACT Technical Report (Stanford University)},
number = {1},
volume = {1},
}

The systematic exploration of the space of all the behaviours of a software system forms the basis of numerous approaches to verification. However, existing approaches face many challenges with scalability and precision. We propose a framework for validating programs based on statistical sampling of inputs guided by statically generated constraints, that steer the simulations towards more ‘‘desirable’’ traces. Our approach works iteratively: each iteration first simulates the system on some inputs sampled from a restricted space, while recording facts about the simulated traces. Subsequent iterations of the process attempt to steer the future simulations away from what has already been seen in the past iterations. This is achieved by two separate means: (a) we perform symbolic executions in order to guide the choice of inputs, and (b) we sample from the input space using a probability distribution specified by means of previously observed test data using a Markov Chain Monte-Carlo (MCMC) technique. As a result, the sampled inputs generate traces that are likely to be significantly different from the observations in the previous iterations in some user specified ways. We demonstrate that our approach is effective. It can rapidly isolate rare behaviours of systems that reveal more bugs and improve coverage.

@InProceedings{Sankaranarayanan+Others-07-State,
author = {Sriram Sankaranarayanan and Richard M. Chang and Guofei Jiang and Franjo Ivancic},
title = {State space exploration using feedback constraint generation and Monte-Carlo sampling},
year = {2007},
pages = {321-330},
publisher = {ACM Press},
booktitle = {ESEC/SIGSOFT FSE},
}

Polyhedral analysis infers invariant linear equalities and inequalities of imperative programs. However, the exponential complexity of polyhedral operations such as image computation and convex hull limits the applicability of polyhedral analysis. Weakly relational domains such as intervals and octagons address the scalability issue by considering polyhedra whose constraints are drawn from a restricted, user-specified class. On the other hand, these domains rely solely on candidate expressions provided by the user. Therefore, they often fail to produce strong invariants. We propose a polynomial time approach to strongly relational analysis. We provide efficient implementations of join and post condition operations, achieving a trade off between performance and accuracy. We have implemented a strongly relational polyhedral analyzer for a subset of the C language. Initial experimental results on benchmark examples are encouraging.

@InProceedings{Sankaranarayanan+Others-06-Efficient,
author = {Sriram Sankaranarayanan and Michael Colon and Henny B. Sipma and Zphar Manna},
title = {Efficient Strongly Relational Polyhedral Analysis},
year = {2006},
pages = {111-125},
publisher = {},
booktitle = {VMCAI},
series = {Lecture Notes in Computer Science},
volume = {3855},
}

The convexity of numerical domains such as polyhedra, oc tagons, intervals and linear equalities enables tractable analysis of soft ware for buffer overflows, null pointer dereferences and floating point errors. However, convexity also causes the analysis to fail in many common cases. Powerset extensions can remedy this shortcoming by considering disjunctions of predicates. Unfortunately, analysis using powerset domains can be exponentially more expensive as compared to analysis on the base domain. In this paper, we prove structural properties of fixed points computed in commonly used powerset extensions. We show that a fixed point computed on a powerset extension is also a fixed point in the base domain computed on an ‘‘elaboration’’ of the program's CFG structure. Using this insight, we build analysis algorithms that approach path sensitive static analysis algorithms by performing the fixed point computation on the base domain while discovering an ‘‘elaboration’’ on the fly. Using restrictions on the nature of the elaborations, we design algorithms that scale polynomially in terms of the number of disjuncts. We have implemented a lighteight static analyzer for C programs with encouraging initial results.

@InProceedings{Sankaranarayanan+Ivancic+Shlyakhter+Gupta-06-Static,
author = {Sriram Sankaranarayanan and Franjo Ivancic and Ilya Shlyakhter and Aarti Gupta},
title = {Static Analysis in Disjunctive Numerical Domains},
year = {2006},
pages = {3-17},
publisher = {},
booktitle = {SAS},
series = {Lecture Notes in Computer Science},
volume = {4134},
}

We investigate techniques for automatically generating symbolic approximations to the time solution of a system of differential equations. This is an important primitive operation for the safety analysis of continuous and hybrid systems. In this paper we design a time elapse operator that computes a symbolic over-approximation of time solutions to a continous system starting from a given inital region. Our approach is iterative over the cone of functions (drawn from a suitable universe) that are non negative over the initial region. At each stage, we iteratively remove functions from the cone whose Lie derivatives do not lie inside the current iterate. If the iteration converges, the set of states defined by the final iterate is shown to contain all the time successors of the initial region. The convergence of the iteration can be forced using abstract interpretation operations such as widening and narrowing. We instantiate our technique to linear hybrid systems with piecewise-affine dynamics to compute polyhedral approximations to the time successors. Using our prototype implementation TimePass, we demonstrate the performance of our technique on benchmark examples.

@InProceedings{Sankaranarayanan+Others-06-Fixed,
author = {Sriram Sankaranarayanan and Henny Sipma and Zohar Manna},
title = {Fixed Point Iteration for Computing the Time Elapse Operator},
year = {2006},
pages = {537-551},
publisher = {},
booktitle = {HSCC},
series = {Lecture Notes in Computer Science},
volume = {3927},
}

We present a specification language and algorithms for the online and offline monitoring of synchronous systems including circuits and embedded systems. Such monitoring is useful not only for testing, but also under actual deployment. The specification language is simple and expressive; it can describe both correctness/failure assertions along with interesting statistical measures that are useful for system profiling and coverage analysis. The algorithm for online monitoring of queries in this language follows a partial evaluation strategy: it incrementally constructs output streams from input streams, while maintaining a store of partially evaluated expressions for forward references. We identify a class of specifications, characterized syntactically, for which the algorithm's memory requirement is independent of the length of the input streams. Being able to bound memory requirements is especially important in online monitoring of large input streams. We extend the concepts used in the online algorithm to construct an efficient offline monitoring algorithm for large traces. We have implemented our algorithm and applied it to two industrial systems, the PCI bus protocol and a memory controller. The results demonstrate that our algorithms are practical and that our specification language is sufficiently expressive to handle specifications of interest to industry.

@InProceedings{Angelo+Others-05-Lola,
author = {Ben D. Angelo and Sriram Sankaranarayanan and Cesar Sanchez and Many Others},
title = {{LOLA:} Runtime Monitoring of Synchronous Systems},
year = {2005},
pages = {166-174},
publisher = {IEEE computer society},
booktitle = {Proc. TIME’05},
}

We present an extension to linear-time temporal logic (LTL) that combines the temporal specification with the collection of statistical data. By collecting statistics over runtime executions of a program we can answer complex queries, such as ‘‘what is the average number of packet transmissions’’ in a communication protocol, or ‘‘how often does a particular process enter the critical section while another process remains waiting’’ in a mutual exclusion algorithm. To decouple the evaluation strategy of the queries from the definition of the temporal operators, we introduce algebraic alternating automata as an automata-based intermediate representation. Algebraic alternating automata are an extension of alternating automata that produce a value instead of acceptance or rejection for each trace. Based on the translation of the formulas from the query language to algebraic alternating automata, we obtain a simple and efficient query evaluation algorithm. The approach is illustrated with examples and experimental results.

@Article{FMSD-RV,
author = {Bernd Finkbeiner and Sriram Sankaranarayanan and Henny Sipma},
title = {Collecting Statistics over Runtime Executions},
year = {2005},
pages = {253-274},
publisher = {},
journal = {Formal Methods In System Design},
number = {3},
volume = {27},
}

We present a method for generating linear invariants for large systems. The method performs forward propagation in an abstract domain consisting of arbitrary polyhedra of a predefined fixed shape. The basic operations on the domain like abstraction, intersection, join and inclusion tests are all posed as linear optimization queries, which can be solved efficiently by existing LP solvers. The number and dimensionality of the LP queries are polynomial in the program dimensionality, size and the number of target invariants. The method generalizes similar analyses in the interval, octagon, and octahedra domains, without resorting to polyhedral manipulations. We demonstrate the performance of our method on some benchmark programs.

Prototype tool LpInv implements techniques presented.

@InProceedings{Sankaranarayanan+Others-05-Scalable,
author = {Sriram Sankaranarayanan and Henny B. Sipma and Zohar Manna},
title = {Scalable Analysis of Linear Systems using Mathematical Programming},
year = {2005},
pages = {25-41},
publisher = {},
booktitle = {Verification, Model-Checking and Abstract-Interpretation (VMCAI 2005)},
series = {Lecture Notes in Computer Science},
volume = {3385},
}

We present a new technique for the generation of non-linear (algebraic) invariants of a program. Our technique uses the theory of ideals over the real and complex numbers to reduce the non-linear invariant generation problem to a numerical constraint solving problem. So far, the literature on invariant generation has concentrated almost exclusively on the construction of linear invariants of linear programs. There has been very little progress toward non-linear invariant generation. In this paper, we demonstrate a technique that encodes the conditions for a given template assertion being an invariant into a set of constraints, such that all the solutions to these constraints correspond to non-linear (algebraic) loop invariants of the program. We discuss some trade-offs between the completeness of the technique and the tractability of the constraint-solving problem generated. The application of the technique is demonstrated on a few examples.

@InProceedings{Sankaranarayanan+Others-2004-Non-Linear,
author = {Sriram Sankaranarayanan and Henny Sipma and Zohar Manna},
title = {Non-linear Loop Invariant Generation using Groebner Bases},
year = {2004},
pages = {318-330},
publisher = {ACM Press},
booktitle = {ACM Principles of Programming Languages (POPL)},
}

Linear-relations analysis of transition systems discovers linear invariant relationships among the variables of the system. These relationships help establish important safety and liveness properties. Efficient techniques for the analysis of systems using polyhedra have been explored, leading to the development of successful tools like HyTech. However, existing techniques rely on the use of approximations such as widening and extrapolation in order to ensure termination. In an earlier paper, we demonstrated the use of Farkas Lemma to provide a translation from the linear-relations analysis problem into a system of constraints on the unknown coefficients of a candidate invariant. However, since the constraints in question are non-linear, a naive application of the method does not scale. In this paper, we show that by some efficient simplifications and approximations to the quantifier elimination procedure, not only does the method scale to higher dimensions, but also enjoys performance advantages for some larger examples

Stanford Invariant Generator tool

@InProceedings{Sankaranarayanan+Others-04-Constraint,
author = {Sriram Sankaranarayanan and Henny B. Sipma and Zohar Manna},
title = {Constraint-based Linear-Relations Analysis},
year = {2004},
pages = {53-69},
publisher = {Springer-Verlag},
booktitle = {Static Analysis Symposium (SAS 2004)},
series = {Lecture Notes in Computer Science},
volume = {3148},
}

An invariant of a system is a predicate that holds for every reachable state. In this paper, we present techniques to generate invariants for hybrid systems by reducing the invariant generation problem to a constraint solving problem, using methods from the theory of ideals over polynomial rings. We extend our previous work on the generation of algebraic invariants for discrete transition systems in order to generate algebraic invariants for hybrid systems. In doing so, we present a new technique to handle consecution across continuous differential equations. The techniques we present allow a trade-off between the complexity of the invariant generation process and the strength of the resulting invariants.

Award Paper: Invited to appear in special issue of formal methods in systems design

@InProceedings{Sankaranarayanan+Others-04-Constructing,
author = {Sriram Sankaranarayanan and Henny B. Sipma and Zohar Manna},
title = {Constructing Invariants for Hybrid Systems},
year = {2004},
pages = {539-555},
publisher = {Springer-Verlag},
booktitle = {Hybrid Systems: Computation and Control (HSCC 2004)},
series = {Lecture Notes in Computer Science},
volume = {2993},
}

Event correlation is a service provided by middleware platforms that allows components in a publish/subscribe architecture to subscribe to patterns of events rather than individual events. Event correlation improves the scalability and performance of distributed systems, increases their analyzability, while reducing their complexity by moving functionality to the middleware. To ensure that event correlation is provided as a standard and reliable service, it must possess well-defined and unambiguous semantics. In this paper we present a language and formal model for event correlation with operational semantics defined in terms of transducers. The language has been motivated by an avionics application and includes constructs for modes in addition to the more common constructs such as selection, accumulation and sequential composition. Prototype event processing engines for this language have been implemented in both C and Java and are now being integrated with third-party event channels.

@InProceedings{Sanchez+Others-03-Event,
author = {Cesar Sanchez and Sriram Sankaranarayanan and Henny Sipma and Ting Zhang and David Dill},
title = {Event Correlation: Language and Semantics},
year = {2003},
pages = {323-339},
publisher = {},
booktitle = {EMSOFT},
series = {Lecture Notes in Computer Science},
volume = {2855},
}

Petri nets have been widely used to model and analyze concurrent systems. Their wide-spread use in this domain is, on one hand, facilitated by their simplicity and expressiveness. On the other hand, the analysis of Petri nets for questions like reachability, boundedness and deadlock freedom can be surprisingly hard. In this paper, we model Petri nets as transition systems. We exploit the special structure in these transition systems to provide an exact and closed-form characterization of all its inductive linear invariants. We then exploit this characterization to provide an invariant generation technique that we demonstrate to be efficient and powerful in practice. We compare our work with those in the literature and discuss extensions.

Invited Paper for Zohar Manna festschrif

@InProceedings{Sankaranarayanan+Others-03-Petri,
author = {Sriram Sankaranarayanan and Henny B. Sipma and Zohar Manna},
title = {Petri Net Analysis using Invariant Generation},
year = {2003},
pages = {682-701},
publisher = {Springer-Verlag},
booktitle = {Verification: Theory and Practice},
series = {Lecture Notes in Computer Science},
volume = {2772},
}

We present a new method for the generation of linear invariants which reduces the problem to a non-linear constraint solving problem. Our method, based on Farkas’ Lemma, synthesizes linear invariants by extracting non-linear constraints on the coefficients of a target invariant from a program. These constraints guarantee that the linear invariant is inductive. We then apply existing techniques, including specialized quantifier elimination methods over the reals, to solve these non-linear constraints. Our method has the advantage of being complete for inductive invariants. To our knowledge, this is the first sound and complete technique for generating inductive invariants of this form. We illustrate the practicality of our method on several examples, including cases in which traditional methods based on abstract interpretation with widening fail to generate sufficiently strong invariants.

Stanford Invariant Generator tool

@InProceedings{Colon+Sankaranarayanan+Sipma-03-Linear,
author = {Michael Colon and Sriram Sankaranarayanan and Henny Sipma},
title = {Linear Invariant Generation using Non-linear Constraint Solving},
year = {2003},
pages = {420-433},
publisher = {Springer-Verlag},
booktitle = {Computer-Aided Verification (CAV)},
series = {Lecture Notes in Computer Science},
volume = {2725},
}

By collecting statistics over runtime executions of a program we can answer complex queries, such as ‘‘what is the average number of packet retransmissions’’ in a communication protocol, or ‘‘how often does process P1 enter the critical section while process P2 waits’’ in a mutual exclusion algorithm. We present an extension to linear-time temporal logic that combines the temporal specification with the collection of statistical data. By translating formulas of this language to alternating automata we obtain a simple and efficient query evaluation algorithm. We illustrate our approach with examples and experimental results.

Invited to appear in special issue in J. Formal Methods in Systems Design

@InProceedings{Finkbeiner+Sankaranarayanan+Sipma-02-Collecting,
author = {Bernd Finkbeiner and Sriram Sankaranarayanan and Henny Sipma},
title = {Collecting Statistics over Runtime Executions},
year = {2002},
pages = {36-54},
publisher = {},
booktitle = {Runtime Verification (RV 2002)},
series = {Elec. Notes Theor. Comp. Sci},
volume = {70},
}

This paper introduces a branching time temporal query language called Min-max CTL which is similar in syntax to the popular temporal logic, CTL. However unlike CTL, Min-max CTL can express timing queries on a timed model. We show that interesting timing queries involving a combination of min and max can be expressed in Min-max CTL. While model checking using most timed temporal logics is PSPACE complete or harder, we show that many practical timing queries, where we are interested in the worst case or best case timings, can be answered in polynomial time by querying the system using Min-max CTL.

@Article{MinMaxCTL,
author = {Pallab Dasgupta and Partha P. Chakrabarti and Jatinder Deka and Sriram Sankaranarayanan},
title = {Min-max Computation Tree Logic},
year = {2001},
pages = {137-162},
publisher = {},
journal = {Artificial Intelligence},
number = {1},
volume = {127},
}