Publications
2016
Sriram Sankaranarayanan, Change of Basis Abstractions for Non-Linear Hybrid Systems In Nonlinear Analysis: Hybrid Systems Vol. 19, pp. 107-133 (2016).
URL Abstract Supplementary Bib Topics Funding
We present abstraction techniques that transform a given non-linear dynamical system into a linear system, or more generally, an algebraic system described by polynomials of bounded degree, so that invariant properties of the resulting abstraction can be used to infer invariants for the original system. The abstraction techniques rely on a change-of-basis 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, the techniques developed here apply to continuous systems defined by Ordinary Differential Equations (ODEs), discrete systems defined by transition systems and hybrid systems that combine continuous as well as discrete subsystems.
The techniques presented here allow us to discover, given a non-linear system, if a change of bases transformation involving degree-bounded polynomials yielding an algebraic abstraction exists. If so, our technique yields the resulting abstract system, as well. 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.
http://www.cs.colorado.edu/~srirams/code/nlsys-release.tar.gz
@article{Sankaranarayanan__2016__Change,
author = { Sriram Sankaranarayanan },
title = { Change of Basis Abstractions for Non-Linear Hybrid Systems },
journal = { Nonlinear Analysis: Hybrid Systems },
volume = { 19 },
year = { 2016 },
pages = { 107-133 },
publisher = { Elsevier }}
Hybrid Systems,Invariant Synthesis
2015
Gregory P. Forlenza, Sriram Sankaranarayanan, and David M. Maahs, Refining the Closed Loop in the Data Age: Research-to-Practice Transitions in Diabetes Technology (Editorial) In Diabetes Technology and Therapeutics Vol. 17(5), pp. 304-306 (2015).
URL Abstract Bib Topics Funding
The editorial analyzes a recent clinical study reporting on
the impact of insulin pump shutoff on patients with
type-1 diabetes. In a broader context, it examines
the need for enhanced formal verification techniques
applied to more sophisticated artificial pancreas
controllers that remain under development.
@article{Forlenza_Others__2015__Refining,
author = { Gregory P. Forlenza, Sriram Sankaranarayanan, and David M. Maahs },
title = { Refining the Closed Loop in the Data Age: Research-to-Practice Transitions in Diabetes Technology (Editorial) },
journal = { Diabetes Technology and Therapeutics },
volume = { 17 },
year = { 2015 },
pages = { 304-306 },
publisher = { Mary Ann Libert Inc. }}
Fraser Cameron, Georgios Fainekos, David M. Maahs, and Sriram Sankaranarayanan, Towards a Verified Artificial Pancreas: Challenges and Solutions for Runtime Verification In Proceedings of Runtime Verification (RV'15), Volume 9333 of Lecture Notes in Computer Science pp. 3-17 (2015).
URL Abstract Note Bib Topics Funding
In this paper, we briefly examine the recent developments in artificial pancreas controllers, that automate the delivery of insulin to patients with type-1 diabetes. We argue the need for offline and online runtime verification for these devices, and discuss challenges that make verification hard. Next, we examine a promising simulation-based falsification approach based on robustness semantics of temporal logics. These ideas are implemented in the tool S-Taliro that automatically searches for violations of metric temporal logic (MTL) requirements for Simulink(tm)/Stateflow(tm) models. We illustrate the use of S-Taliro for finding interesting property violations in a PID-based hybrid closed loop control system.
@inproceedings{Cameron_Fainekos_Maahs_Sankaranarayanan__2015__Towards,
author = { Fraser Cameron, Georgios Fainekos, David M. Maahs, and Sriram Sankaranarayanan },
title = { Towards a Verified Artificial Pancreas: Challenges and Solutions for Runtime Verification },
booktitle = { Proceedings of Runtime Verification (RV'15) },
year = { 2015 },
pages = { 3-17 },
note = { Invited Keynote Paper },
series = { Lecture Notes in Computer Science },
volume = { 9333 }}
Artificial Pancreas,Falsification of Cyber-Physical Systems
Yan Zhang, Sriram Sankaranarayanan, and Benjamin Gyori, Simulation-Guided Parameter Synthesis for the Chance-Constrained Optimization of Control Systems In Proc. International Conference on Computer-Aided Design (ICCAD), pp. TBA (2015).
URL Abstract Bib Topics Funding
We consider the problem of parameter synthesis for black-box systems whose operations are jointly influenced by a set of “tunable parameters” under the control of designers, and a set of uncontrollable stochastic parameters. The goal is to find values of the tunable parameters that ensure the satisfaction of given performance requirements with a high probability. Such problems are common in robust system design, including feedback controllers, biomedical devices, and many others. These can be naturally cast as chance-constrained optimization problems, which however, are hard to solve precisely. We present a simulation-based approach that provides a piecewise approximation of a certain quantile function for the responses of interest. Using the piecewise approximations as objective functions, a collection of local optima are estimated, from which a global search based on simulated annealing is performed. The search yields tunable parameter values at which the performance requirements are satisfied with a high probability, despite variations in the stochastic parameters. Our approach is applied to three benchmarks: an insulin infusion pump model for patients with type-1 diabetes, a robust flight control problem for fixed-wing aircrafts, and an ODE-based apoptosis model from system biology.
@inproceedings{Zhang_Sankaranarayanan_Gyori__2015__Simulation,
author = { Yan Zhang, Sriram Sankaranarayanan, and Benjamin Gyori },
title = { Simulation-Guided Parameter Synthesis for the Chance-Constrained Optimization of Control Systems },
booktitle = { Proc. International Conference on Computer-Aided Design (ICCAD) },
year = { 2015 },
pages = { TBA },
publisher = { ACM Press }}
Learning-Based Parameter Synthesis
Mohamed Amin Ben Sassi, Sriram Sankaranarayanan, Xin Chen, and Erika Abraham, Linear Relaxations of Polynomial Positivity for Polynomial Lyapunov Function Synthesis In IMA Journal of Mathematical Control and Information Vol. TBA(TBA), pp. dnv003 (2015).
URL Abstract Bib
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 }}
2014
Mohamed Amin Ben Sassi, Antoine Girard, and Sriram Sankaranarayanan, Iterative Computation of Polyhedral Invariants Sets for Polynomial Dynamical Systems In IEEE Conference on Decision and Control (CDC) pp. 6348-6353 (2014), IEEE Press.
PDF Abstract Bibtex
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)},
}
Yan Zhang, Sriram Sankaranarayanan, and Fabio Somenzi, Statistically Sound Verification and Optimization for Complex Systems In Automated Techniques for Verification and Analysis (ATVA) Volume 8837 of Lecture Notes in Computer Science, pp. 411-427 (2014).
PDF Abstract Bibtex
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},
}
Stephen M Kissler, Cody Cichowitz, Sriram Sankaranarayanan, and David M Bortz, Determination of personalized diabetes treatment plans using a two-delay model In J. Theoretical Biology Vol. 359(Oct), pp. 101-111 (2014) , Elsevier Press.
PDF Abstract Bibtex
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},
}
Hadi Ravanbakhsh, and Sriram Sankaranarayanan, Infinite Horizon Safety Controller Synthesis through Disjunctive Polyhedral Abstract Interpretation In Intl. Conference on Embedded Software (EMSOFT) pp. 15:1-15:10 (2014), ACM Press.
PDF Abstract Bibtex
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)},
}
Xin Chen, Sriram Sankaranarayanan, and Erika Abraham, Under-approximate Flowpipes for Non-linear Continuous Systems In Formal Methods in Computer-Aided Design (FMCAD) pp. 59-66 (2014).
PDF Abstract Bibtex
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)},
}
Aditya Zutshi, Sriram Sankaranarayanan, Jyotirmoy Deshmukh, and James Kapinski, Multiple-Shooting CEGAR-based falsification for hybrid systems In Intl. Conference on Embedded Software (EMSOFT) pp. 5:1 - 5:10 (2014), ACM Press.
Note: Winner of EMSOFT Best Paper Award
PDF Abstract Bibtex
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)},
}
Franjo Ivancic, Gogul Balakrishnan, Aarti Gupta, Sriram Sankaranarayanan, Naoto Maeda, Takashi Imoto, Rakesh Pothengil, and Mustafa Hussain, Scope bounded software verification in Varvel In Journal of Automated Software Engineering (J. ASE) Vol. pp. 1-14 (2014) , Springer.
PDF Abstract Bibtex
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 = {},
}
Aleksandar Chakarov, and Sriram Sankaranarayanan, Expectation Invariants as Fixed Points of Probabilistic Programs In Static Analysis Symposium (SAS) Volume 8723 of Lecture Notes in Computer Science, pp. 85-100 (2014), Springer-Verlag.
Note: Radhia Cousot Best Paper Award
PDF Abstract Bibtex
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.
@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},
}
Arlen Cox, Bor-Yuh Evan Chang, and Sriram Sankaranarayanan, QUICr: A Reusable Library for Parametric Abstraction of
Sets and Numbers In Computer-Aided Verification (CAV) Volume 8559 of Lecture Notes in Computer Science, pp. 866-873 (2014), Springer-Verlag.
Note: Tool Demonstration Paper
PDF Abstract Supplementary Material Bibtex
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.
@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},
}
Eric Goubault, Jacques-Henri Jourdan, Sylvie Putot, and Sriram Sankaranarayanan, Finding Non-Polynomial Positive Invariants and Lyapunov Functions for Polynomial Systems through Darboux Polynomials In Proc. American Control Conference (ACC) pp. 3571 - 3578 (2014), IEEE Press.
PDF Abstract Bibtex
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)},
}
James Kapinski, Jyotirmoy V Deshmukh, Sriram Sankaranarayanan, and Nikos Arechiga, Simulation-guided Lyapunov Analysis for Hybrid Dynamical Systems In Hybrid Systems: Computation and Control (HSCC) pp. 133-142 (2014), ACM Press.
PDF Abstract Bibtex
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)},
}
Bertrand Jeannet, Peter Schrammel, and Sriram Sankaranarayanan, Abstract Acceleration of General Linear Loops In Principles of Programming Languages (POPL) pp. 529-540 (2014), ACM Press.
PDF Abstract Bibtex
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)},
}
Yan Zhang, Sriram Sankaranarayanan, and Fabio Somenzi, Sparse statistical model inference for analog circuits under process variations In Asia and South Pacific Design Automation Conference (ASP-DAC) pp. 449-454 (2014), IEEE Press.
PDF Abstract Bibtex
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)},
}
2013
Houssam Abbas, Georgios Fainekos, Sriram Sankaranarayanan, Franjo Ivancic, and Aarti Gupta, Probabilistic Temporal Logic Falsification of Cyber-Physical Systems In ACM Transactions on Embedded Computing Systems (TECS) Vol. 12(12s), pp. 95 (2013) , ACM Press.
PDF Abstract Supplementary Material Bibtex
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.
@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},
}
Vineet Kahlon, Sriram Sankaranarayanan, and Aarti Gupta, Static analysis for concurrent programs with applications
to data race detection In STTT Vol. 15(4), pp. 321-336 (2013) , Springer-Verlag.
PDF Abstract Bibtex
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},
}
Aditya Zutshi, Sriram Sankaranarayanan, Jyotirmoy Deshmukh, and James Kapinski, A trajectory splicing approach to concretizing counterexamples for hybrid systems In IEEE Conference on Decision and Control (CDC) pp. 3918-3925 (2013), IEEE Press.
Note: Invited Session on Formal Methods in Control
PDF Abstract Bibtex
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)},
}
Yan Zhang, Sriram Sankaranarayanan, Fabio Somenzi, Xin Chen, and Erika Abraham, From statistical model checking to statistical model inference:
characterizing the effect of process variations in analog
circuits In International Conference on Computer-Aided
Design (ICCAD) pp. 662-669 (2013), IEEE/ACM Press.
PDF Abstract Supplementary Material Bibtex
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)},
}
Sriram Sankaranarayanan, Xin Chen, and Erika Abraham, Lyapunov Function Synthesis Using Handelman Representations In IFAC conference on Nonlinear Control Systems (NOLCOS) pp. 576-581 (2013).
Note: Invited Session on Reliable methods for control, state estimation and parameter identification of uncertain dynamic systems
PDF Abstract Supplementary Material Bibtex
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
@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)},
}
Swarat Chaudhuri, Sriram Sankaranarayanan, and Moshe Vardi, Regular Real Analysis In IEEE Symposium on Logic in Computer Science (LICS) pp. 509-518 (2013), IEEE Press.
PDF Abstract Bibtex
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)},
}
Aleksandar Chakarov, and Sriram Sankaranarayanan, Probabilistic Program Analysis using Martingales In Computer-Aided Verification (CAV) Volume 8044 of Lecture Notes in Computer Science, pp. 511-526 (2013), Springer-Verlag.
PDF Abstract Supplementary Material Bibtex
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.
@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},
}
Xin Chen, Erika Abraham, and Sriram Sankaranarayanan, Flow*: An Analyzer for Non-Linear Hybrid Systems In Computer-Aided Verification (CAV) Volume 8044 of Lecture Notes in Computer Science, pp. 258-263 (2013), Springer-Verlag.
PDF Abstract Supplementary Material Bibtex
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.
@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},
}
Sriram Sankaranarayanan, Aleksandar Chakarov, and Sumit Gulwani, Static Analysis for Probabilistic Programs: Inferring Whole Program Properties from Finitely Many Paths In ACM conference on Programming Languages Design and Implementation (PLDI) pp. 447-458 (2013), ACM Press.
Note: ACM SIGPLAN Distinguished Paper Award.
PDF Abstract Supplementary Material Bibtex
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.
@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)},
}
Paul Givens, Aleksandar Chakarov, Sriram Sankaranarayanan, and Tom Yeh, Exploring the Internal State of User Interfaces by Combining Computer Vision Techniques with Grammatical Inference In Proc. International Conference on Software Engg. (NIER track) pp. 1165-1168 (2013), ACM Press.
PDF Abstract Bibtex
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)},
}
Arlen Cox, Bor-Yuh Evan Chang, and Sriram Sankaranarayanan, QUIC Graphs: Relational Invariant Generation for Containers In European Colloquium on Object-Oriented Programming (ECOOP) Volume 7920 of Lecture Notes in Computer Science, pp. 401-425 (2013), Springer-Verlag.
PDF Abstract Supplementary Material Bibtex
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.
@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},
}
2012
Xin Chen, Erika Abraham, and Sriram Sankaranarayanan, Taylor Model Flowpipe Construction for Non-linear Hybrid Systems In Real Time Systems Symposium (RTSS) pp. 183-192 (2012), IEEE Press.
PDF Abstract Supplementary Material Bibtex
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.
@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)},
}
Arlen Cox, Sriram Sankaranarayanan, and Bor-Yuh Evan Chang, A Bit too Precise? Bounded Verification of Quantized Digital Filters In Tools and Algorithms for the Construction and Analysis of Systems (TACAS) Volume 7214 of Lecture Notes in Computer Science, pp. 33-42 (2012).
PDF Abstract Supplementary Material Bibtex
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.
@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},
}
Sriram Sankaranarayanan, and Georgios E Fainekos, Falsification of temporal properties of hybrid systems using
the cross-entropy method In HSCC pp. 125-134 (2012), ACM.
PDF Abstract Bibtex
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},
}
Georgios Fainekos, Sriram Sankaranarayanan, Koichi Ueda, and Hakan Yazarel, Verification of Automotive Control Applications using S-Taliro In American Control Conference (ACC) pp. 3567-3572 (2012), IEEE Press.
Note: Invited Session on Verification of Automotive Control Systems
PDF Abstract Supplementary Material Bibtex
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
@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)},
}
Aditya Zutshi, Sriram Sankaranarayanan, and Ashish Tiwari, Timed Relational Abstractions for Sampled Data Control Systems In Computer-Aided Verification (CAV) Volume 7358 of Lecture Notes in Computer Science, pp. 343-361 (2012), Springer-Verlag.
PDF Abstract Supplementary Material Bibtex
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.
@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},
}
Sriram Sankaranarayanan, and Georgios Fainekos, Simulating Insulin Infusion Pump Risks by In-Silico Modeling of the Insulin-Glucose Regulatory System In Computational Methods in Systems Biology (CMSB) Volume 7605 of Lecture Notes in Computer Science, pp. 322-341 (2012), Springer-Verlag.
PDF Abstract Supplementary Material Bibtex
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.
@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},
}
Kangjin Kim, Georgios E Fainekos, and Sriram Sankaranarayanan, On the revision problem of specification automata In ICRA pp. 5171-5176 (2012), IEEE Press.
PDF Abstract Bibtex
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},
}
Jing Yang, Gogul Balakrishnan, Naoto Maeda, Franjo Ivancic, Aarti Gupta, Nishant Sinha, Sriram Sankaranarayanan, and Naveen Sharma, Object Model Construction for Inheritance in C and Its
Applications to Program Analysis In Compiler Construction (CC) Volume 7210 of Lecture Notes in Computer Science, pp. 144-164 (2012), Springer-Verlag.
PDF Abstract Bibtex
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},
}
Alejandro Sanchez, Sriram Sankaranarayanan, Cesar Sanchez, and Bor-Yuh Evan Chang, Invariant Generation for Parametrized Systems using Self-Reflection In Static Analysis Symposium (SAS) Volume 7460 of Lecture Notes in Computer Science, pp. 146-163 (2012), Springer-Verlag.
PDF Abstract Bibtex
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},
}
Yan Zhang, Sriram Sankaranarayanan, and Fabio Somenzi, Piecewise linear modeling of nonlinear devices for formal
verification of analog circuits In Formal Methods in Computer-Aided Design ( FMCAD 2012 ) pp. 196-203 (2012), IEEE Press.
PDF Abstract Bibtex
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 )},
}
Sriram Sankaranarayanan, Christopher Miller, Rangarajan Raghunathan, Hadi Ravanbakhsh, and Georgios E Fainekos, A model-based approach to synthesizing insulin infusion
pump usage parameters for diabetic patients In Allerton Conference pp. 1610-1617 (2012), IEEE Press.
Note: Invited Paper appeared in special session on Cyber-Physical Systems
PDF Abstract Bibtex
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},
}
2011
Robert Frohardt, Bor-Yuh Evan Chang, and Sriram Sankaranarayanan, Access Nets: Modeling Access to Physical Spaces In Verification, Model Checking, and Abstract Interpretation (VMCAI) Volume 6538 of Lecture Notes in Computer Science, pp. 184-198 (2011), Springer-Verlag.
PDF Abstract Supplementary Material Bibtex
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.
@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},
}
Sriram Sankaranarayanan, Hadjar Homaei, and Clayton Lewis, Model-Based Dependability Analysis of Programmable Drug
Infusion Pumps In Formal Methods for Timed Systems (FORMATS) Volume 6919 of Lecture Notes in Computer Science, pp. 317-334 (2011).
PDF Abstract Supplementary Material Bibtex
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.
@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},
}
Franjo Ivancic, Gogul Balakrishnan, Aarti Gupta, Sriram Sankaranarayanan, Naoto Maeda, Hiroki Tokuoka, Takashi Imoto, and Yoshiaki Miyazaki, DC2: A framework for scalable, scope-bounded software verification In Automated Software Engg. (ASE) pp. 133-142 (2011), IEEE Press.
PDF Abstract Bibtex
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)},
}
Yashwanth Annpureddy, Che Liu, Georgios E Fainekos, and Sriram Sankaranarayanan, S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid
Systems In Tools and Algorithms for Construction and Analysis of Systems (TACAS) Volume 6605 of Lecture Notes in Computer Science, pp. 254-257 (2011), Springer.
PDF Abstract Supplementary Material Bibtex
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.
@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},
}
Jyotirmoy V Deshmukh, E. Allen Emerson, and Sriram Sankaranarayanan, Symbolic modular deadlock analysis In Autom. Softw. Eng. Vol. 18(3-4), pp. 325-362 (2011) .
Note: Journal version of ASE 2009 paper. DOI:10.1007s10515-011-0085-0 /
PDF Abstract Bibtex
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.
@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},
}
Sam Blackshear, Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Manu Sridharan, The Flow-Insensitive Precision of Andersen's Analysis in
Practice In SAS Volume 6887 of Lecture Notes in Computer Science, pp. 60-76 (2011).
PDF Abstract Bibtex
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},
}
Sriram Sankaranarayanan, and Ashish Tiwari, Relational Abstractions for Continuous and Hybrid Systems In Computer-Aided Verification (CAV) Volume 6806 of Lecture Notes in Computer Science, pp. 686-702 (2011), Springer-Verlag.
PDF Abstract Supplementary Material Bibtex
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.
@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},
}
Michael Colon, and Sriram Sankaranarayanan, Generalizing the Template Polyhedral Domain In European Symposium on Programming (ESOP) Volume 6602 of Lecture Notes in Computer Science, pp. 176-195 (2011), Springer-Verlag.
PDF Abstract Bibtex
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},
}
Aleksandar Chakarov, Sriram Sankaranarayanan, and Georgios E Fainekos, Combining Time and Frequency Domain Specifications for Periodic
Signals In Runtime Verification (RV) Volume 7186 of Lecture Notes in Computer Science (LNCS), pp. 294-309 (2011), Springer-Verlag.
Note: Link to the published version
PDF Abstract Bibtex
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.
@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.
@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},
}
Sriram Sankaranarayanan, Automatic Abstraction of Non-Linear Systems Using Change of Variables Transformations In Hybrid Systems: Computation and Control (HSCC) pp. 143-152 (2011), ACM Press.
Note: Please see extended version
PDF Abstract Bibtex
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.
@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)},
}
2010
Truong Nghiem, Sriram Sankaranarayanan, Georgios E Fainekos, Franjo Ivancic, Aarti Gupta, and George J Pappas, Monte-carlo techniques for falsification of temporal properties
of non-linear hybrid systems In Hybrid Systems: Computation and Control pp. 211-220 (2010), ACM Press.
PDF Abstract Bibtex
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},
}
Sicun Gao, Malay K Ganai, Franjo Ivancic, Aarti Gupta, Sriram Sankaranarayanan, and Edmund M Clarke, Integrating {ICP} and {LRA} Solvers for Deciding Nonlinear Real
Arithmetic Problems In Formal Methods for Computer-Aided Design (FMCAD) pp. 81-89 (2010), IEEE Press.
PDF Abstract Bibtex
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)},
}
Sriram Sankaranarayanan, Automatic Invariant Generation for Hybrid Systems using Ideal Fixed Points In Hybrid Systems: Computation and Control pp. 211-230 (2010), ACM Press.
PDF Abstract Bibtex
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},
}
Franjo Ivancic, Malay Ganai, Sriram Sankaranarayanan, and Aarti Gupta, Numerical stability analysis of floating-point computations using software model checking In Formal Methods and Models for Codesign (MEMOCODE) pp. 49-58 (2010).
PDF Abstract Bibtex
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)},
}
William R Harris, Sriram Sankaranarayanan, Franjo Ivancic, and Aarti Gupta, Satisfiability Modulo Path Programs In ACM Principles of Programming Languages (POPL’10) pp. 71-82 (2010), ACM Press.
PDF Abstract Bibtex
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)},
}
2009
Vineet Kahlon, Sriram Sankaranarayanan, and Aarti Gupta, Semantic Reduction of Thread Interleavings in Concurrent
Programs In TACAS Volume 5505 of Lecture Notes in Computer Science, pp. 124-138 (2009).
PDF Abstract Bibtex
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},
}
Aditya Kanade, Rajeev Alur, Franjo Ivancic, S. Ramesh, Sriram Sankaranarayanan, and K. C. Shashidhar, Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models In Computer-Aided Verification (CAV) Volume 5643 of Lecture Notes in Computer Science, pp. 430-445 (2009), Springer-Verlag.
PDF Abstract Bibtex
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},
}
Gogul Balakrishnan, Sriram Sankaranarayanan, Franjo Ivancic, and Aarti Gupta, Refining the control structure of loops using static analysis In Embedded Software (EMSOFT) pp. 49-58 (2009), ACM Press.
PDF Abstract Bibtex
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)},
}
Georgios E Fainekos, Sriram Sankaranarayanan, Franjo Ivancic, and Aarti Gupta, Robustness of Model-Based Simulations In Real-Time Systems Symposium (RTSS) pp. 345-354 (2009), IEEE Press.
PDF Abstract Bibtex
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)},
}
Jyotirmoy Deshmukh, E. Allen Emerson, and Sriram Sankaranarayanan, Symbolic Deadlock Analysis in Concurrent Libraries and their Clients In Automated Software Engg. (ASE) pp. 480-491 (2009), ACM Press.
Note: ACM SIGSOFT distinguished paper award
PDF Abstract Bibtex
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)},
}
Richard Chang, Guofei Jiang, Franjo Ivancic, Sriram Sankaranarayanan, and Vitaly Shmatikov, Inputs of Coma: Static Detection of Denial-of-Service Vulnerabilities In Computer Security Foundations (CSF) pp. 186-199 (2009), IEEE Press.
PDF Abstract Bibtex
2008
Gogul Balakrishnan, Sriram Sankaranarayanan, Franjo Ivancic, Ou Wei, and Aarti Gupta, SLR: Path-Sensitive Analysis through Infeasible-Path Detection
and Syntactic Language Refinement In SAS Volume 5079 of Lecture Notes in Computer Science, pp. 238-254 (2008), Springer-Verlag.
PDF Abstract Bibtex
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},
}
Sriram Sankaranarayanan, Thao Dang, and Franjo Ivancic, Symbolic Model Checking of Hybrid Systems Using Template
Polyhedra In TACAS Volume 4963 of Lecture Notes in Computer Science, pp. 188-202 (2008), Springer-Verlag.
PDF Abstract Bibtex
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},
}
Sriram Sankaranarayanan, Thao Dang, and Franjo Ivancic, A Policy Iteration Technique for Time Elapse over Template
Polyhedra In HSCC Volume 4981 of Lecture Notes in Computer Science, pp. 654-657 (2008), Springer-Verlag.
PDF Abstract Bibtex
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},
}
Sriram Sankaranarayanan, Henny Sipma, and Zohar Manna, Constructing Invariants for Hybrid Systems In Formal Methods in System Design Vol. 32(1), pp. 25-55 (2008) .
Note: Special Issue For HSCC 2004
PDF Abstract Bibtex
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},
}
Sriram Sankaranarayanan, Swarat Chaudhuri, Franjo Ivancic, and Aarti Gupta, Dynamic inference of likely data preconditions over predicates
by tree learning In ISSTA pp. 295-306 (2008), ACM Press.
PDF Abstract Bibtex
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},
}
Sriram Sankaranarayanan, Franjo Ivancic, and Aarti Gupta, Mining library specifications using inductive logic programming In Intl. Symp. on Software Engg. (ICSE) pp. 131-140 (2008), ACM Press.
PDF Abstract Bibtex
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)},
}
2007
Sriram Sankaranarayanan, Franjo Ivancic, and Aarti Gupta, Program Analysis Using Symbolic Ranges In SAS Volume 4634 of Lecture Notes in Computer Science, pp. 366-383 (2007).
PDF Abstract Bibtex
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},
}
Vineet Kahlon, Yu Yang, Sriram Sankaranarayanan, and Aarti Gupta, Fast and Accurate Static Data-Race Detection for Concurrent
Programs In Computer-Aided Verification (CAV) Volume 4590 of Lecture Notes in Computer Science, pp. 226-239 (2007).
PDF Abstract Bibtex
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},
}
Matteo Slanina, Sriram Sankaranarayanan, Henny B Sipma, and Zohar Manna, Controller Synthesis of Discrete Linear Plants Using Polyhedra In REACT Technical Report (Stanford University) Vol. 1(1), pp. 1-14 (2007) .
PDF Abstract Bibtex
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},
}
Sriram Sankaranarayanan, Richard M Chang, Guofei Jiang, and Franjo Ivancic, State space exploration using feedback constraint generation
and Monte-Carlo sampling In ESEC/SIGSOFT FSE pp. 321-330 (2007), ACM Press.
PDF Abstract Bibtex
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},
}
2006
Sriram Sankaranarayanan, Michael Colon, Henny B Sipma, and Zphar Manna, Efficient Strongly Relational Polyhedral Analysis In VMCAI Volume 3855 of Lecture Notes in Computer Science, pp. 111-125 (2006).
PDF Abstract Bibtex
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},
}
Sriram Sankaranarayanan, Franjo Ivancic, Ilya Shlyakhter, and Aarti Gupta, Static Analysis in Disjunctive Numerical Domains In SAS Volume 4134 of Lecture Notes in Computer Science, pp. 3-17 (2006).
PDF Abstract Bibtex
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},
}
Sriram Sankaranarayanan, Henny Sipma, and Zohar Manna, Fixed Point Iteration for Computing the Time Elapse Operator In HSCC Volume 3927 of Lecture Notes in Computer Science, pp. 537-551 (2006).
PDF Abstract Bibtex
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},
}
2005
Ben D Angelo, Sriram Sankaranarayanan, Cesar Sanchez, and Many Others, {LOLA:} Runtime Monitoring of Synchronous Systems In Proc. TIME’05 pp. 166-174 (2005), IEEE computer society.
PDF Abstract Bibtex
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},
}
Bernd Finkbeiner, Sriram Sankaranarayanan, and Henny Sipma, Collecting Statistics over Runtime Executions In Formal Methods In System Design Vol. 27(3), pp. 253-274 (2005) .
PDF Abstract Bibtex
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},
}
Sriram Sankaranarayanan, Henny B Sipma, and Zohar Manna, Scalable Analysis of Linear Systems using Mathematical Programming In Verification, Model-Checking and Abstract-Interpretation (VMCAI 2005) Volume 3385 of Lecture Notes in Computer Science, pp. 25-41 (2005).
PDF Abstract Supplementary Material Bibtex
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.
@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},
}
2004
Sriram Sankaranarayanan, Henny Sipma, and Zohar Manna, Non-linear Loop Invariant Generation using Groebner Bases In ACM Principles of Programming Languages (POPL) pp. 318-330 (2004), ACM Press.
PDF Abstract Bibtex
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)},
}
Sriram Sankaranarayanan, Henny B Sipma, and Zohar Manna, Constraint-based Linear-Relations Analysis In Static Analysis Symposium (SAS 2004) Volume 3148 of Lecture Notes in Computer Science, pp. 53-69 (2004), Springer-Verlag.
PDF Abstract Supplementary Material Bibtex
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
@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},
}
Sriram Sankaranarayanan, Henny B Sipma, and Zohar Manna, Constructing Invariants for Hybrid Systems In Hybrid Systems: Computation and Control (HSCC 2004) Volume 2993 of Lecture Notes in Computer Science, pp. 539-555 (2004), Springer-Verlag.
Note: Award Paper: Invited to appear in special issue of formal methods in systems design
PDF Abstract Bibtex
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},
}
2003
Cesar Sanchez, Sriram Sankaranarayanan, Henny Sipma, Ting Zhang, and David Dill, Event Correlation: Language and Semantics In EMSOFT Volume 2855 of Lecture Notes in Computer Science, pp. 323-339 (2003).
PDF Abstract Bibtex
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},
}
Sriram Sankaranarayanan, Henny B Sipma, and Zohar Manna, Petri Net Analysis using Invariant Generation In Verification: Theory and Practice Volume 2772 of Lecture Notes in Computer Science, pp. 682-701 (2003), Springer-Verlag.
Note: Invited Paper for Zohar Manna festschrif
PDF Abstract Bibtex
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},
}
Michael Colon, Sriram Sankaranarayanan, and Henny Sipma, Linear Invariant Generation using Non-linear Constraint Solving In Computer-Aided Verification (CAV) Volume 2725 of Lecture Notes in Computer Science, pp. 420-433 (2003), Springer-Verlag.
PDF Abstract Supplementary Material Bibtex
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.
@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},
}
2002
Bernd Finkbeiner, Sriram Sankaranarayanan, and Henny Sipma, Collecting Statistics over Runtime Executions In Runtime Verification (RV 2002) Volume 70 of Elec. Notes Theor. Comp. Sci, pp. 36-54 (2002).
Note: Invited to appear in special issue in J. Formal Methods in Systems Design
PDF Abstract Bibtex
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},
}
2001
Pallab Dasgupta, Partha P Chakrabarti, Jatinder Deka, and Sriram Sankaranarayanan, Min-max Computation Tree Logic In Artificial Intelligence Vol. 127(1), pp. 137-162 (2001) .
PDF Abstract Bibtex
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},
}
|