Project Page for NSF CAREER: Automatic Analysis of Cyber Physical Systems
This page summarizes the publications, theses, software and personnel
for the NSF Award # 0953941
CAREER: Automatic Analysis of Cyber Physical Systems: Bridging the
Gap between Research and Industrial Practice (March 1, 2010 -
Feb 28, 2016). PI: Sankaranarayanan.
Project Goals
The major research goal of this project is to develop new formal
verification techniques for cyber-physical systems that bridge the gap
between the capabilities of existing verification algorithms, and the
capabilities that an industrial strength approach requires. In
particular, we focus on three major themes:
Focus on reasoning about non-linear systems, bridging the gap between the current approaches focused mostly on linear hybrid systems and common industry benchmarks that require the ability to reason about non-linear systems.
Focus on reasoning about the numerical issues in controllers which are typically implemented in fixed/floating points.
Focus on developing tools for models that are closer to formalisms employed in the industry rather than the hybrid automaton.
Finally, the project's major educational goal is to develop courses
that will bridge the gap between existing CS curriculum and the need
for engineers who are trained in the fundamentals of cyber-physical
systems including ideas from optimization, dynamical systems, modeling
& simulation, and control theory.
Publications (Total = 24)
Note: all publications other than invited papers are peer-reviewed.
Pierre Roux, Yuen-Lam Voronin, and Sriram Sankaranarayanan, Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants In Static Analysis Symposium (SAS), Volume 9837 of Lecture Notes in Computer Science pp. TBA (2016). Note: To Appear Sept. 2016
URL Abstract Bib Topics
Semidefinite programming (SDP) solvers are increasingly used as
primitives in many program verification tasks to synthesize and verify
polynomial invariants for a variety of systems including programs,
hybrid systems and stochastic models. On one hand, they provide a
tractable alternative to reasoning about semi-algebraic
constraints. However, the results are often unreliable due to
``numerical issues'' that include a large number of reasons such as
floating point errors, ill-conditioned problems, failure of strict
feasibility, and more generally, the specifics of the algorithms used
to solve SDPs. These issues influence whether the final numerical
results are trustworthy. In this paper, we briefly survey the emerging use of
SDP solvers in the static analysis community. We report on the perils
of using SDP solvers for common invariant synthesis tasks,
characterizing the common failures that can lead to unreliable
answers. Next, we demonstrate existing tools for guaranteed
semidefinite programming that often prove inadequate to our
needs. Finally, we present a solution for verified semidefinite
programming that can be used to check the reliability of the solution
output by the solver and a padding procedure that can check the
presence of a feasible nearby solution to the one output by the
solver. We report on some successful preliminary experiments involving
our padding procedure.
@inproceedings{Roux_Others__2016__Verified,
author = { Pierre Roux, Yuen-Lam Voronin, and Sriram Sankaranarayanan },
title = { Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants },
booktitle = { Static Analysis Symposium (SAS) },
year = { 2016 },
pages = { TBA },
publisher = { Springer },
series = { Lecture Notes in Computer Science },
volume = { 9837 }}
Hadi Ravanbakhsh, and Sriram Sankaranarayanan, Robust Controller Synthesis of Switched Systems Using Counterexample Guided Framework In ACM/IEEE Conference on Embedded Software (EMSOFT), pp. TBA (2016). Note: To Appear (Oct 2016)
URL Abstract Bib Topics
We investigate the problem of synthesizing robust controllers that
ensure that the closed loop satisfies an input reach-while-stay
specification, wherein all trajectories starting from some initial
set I, eventually reach a specified goal set G, while staying
inside a safe set S. Our plant model consists of a continuous-time
switched system controlled by an external switching signal and plant
disturbance inputs. The controller uses a state feedback law to
control the switching signal in order to ensure that the desired
correctness properties hold, regardless of the disturbance actions.
Our approach uses a proof certificate in the form of a robust
control Lyapunov-like function (RCLF) whose existence guarantees the
reach-while-stay specification. A counterexample guided inductive
synthesis (CEGIS) framework is used to find a RCLF by solving a
∃∀∃∀ formula iteratively using quantifier
free SMT solvers. We compare our synthesis scheme against a common
approach that fixes disturbances to nominal values and synthesizes
the controller, ignoring the disturbance. We demonstrate that the
latter approach fails to yield a robust controller over some
benchmark examples, whereas our approach does.
Finally, we consider the problem of translating the RCLF synthesized
by our approach into a control implementation. We outline the series
of offline and real-time computation steps needed. The synthesized
controller is implemented and simulated using the
Matlab(tm)/Simulink(tm) model-based design framework, and illustrated
on some examples.
@inproceedings{Ravanbakhsh_Sankaranarayanan__2016__Robust,
author = { Hadi Ravanbakhsh, and Sriram Sankaranarayanan },
title = { Robust Controller Synthesis of Switched Systems Using Counterexample Guided Framework },
booktitle = { ACM/IEEE Conference on Embedded Software (EMSOFT) },
year = { 2016 },
pages = { TBA }}
Sriram Sankaranarayanan, Change of Basis Abstractions for Non-Linear Hybrid Systems In Nonlinear Analysis: Hybrid Systems Vol. 19, pp. 107-133 (2016).
URL Abstract Bib Topics Supplementary
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.
@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 }}
2015 (2)
Hadi Ravanbakhsh, and Sriram Sankaranarayanan, Counter-Example Guided Synthesis of Control Lyapunov Functions For Switched Systems In IEEE Control and Decision Conference (CDC), pp. 4232-4239 (2015).
URL Abstract Bib Topics
We investigate the problem of synthesizing switching controllers for
stabilizing continuous-time plants. First, we introduce a class of
control Lyapunov functions (CLFs) for switched systems along with a
switching strategy that yields a closed loop system with a
guaranteed minimum dwell time in each switching mode. However, the
challenge lies in automatically synthesizing appropriate
CLFs. Assuming a given fixed form for the CLF with unknown
coefficients, we derive quantified nonlinear constraints whose
feasible solutions (if any) correspond to CLFs for the original
system.
However, solving quantified nonlinear constraints pose a challenge
to most LMI/BMI-based relaxations. Therefore, we investigate a
general approach called Counter-Example Guided Inductive Synthesis
(CEGIS), that has been widely used in the emerging area of automatic
program synthesis. We show how a LMI-based relaxation can be
formulated within the CEGIS framework for synthesizing CLFs. We
also evaluate our approach on a number of interesting benchmarks,
and compare the performance of the new approach with our previous
work that uses off-the-shelf nonlinear constraint solvers instead of
the LMI relaxation. The results shows synthesizing CLFs by using LMI
solvers inside a CEGIS framework can be a computational feasible
approach to synthesizing CLFs.
@inproceedings{Ravanbakhsh_Sankaranarayanan__2015__Counter,
author = { Hadi Ravanbakhsh, and Sriram Sankaranarayanan },
title = { Counter-Example Guided Synthesis of Control Lyapunov Functions For Switched Systems },
booktitle = { IEEE Control and Decision Conference (CDC) },
year = { 2015 },
pages = { 4232-4239 },
publisher = { IEEE Press }}
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. dnv003, pp. 39 (2015).
URL Abstract Bib Topics
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 = { dnv003 },
year = { 2015 },
pages = { 39 },
publisher = { Oxford University Press }}
2014 (5)
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).
URL Abstract Bib Topics
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 },
booktitle = { Intl. Conference on Embedded Software (EMSOFT) },
year = { 2014 },
pages = { 15:1-15:10 },
publisher = { ACM Press }}
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).
URL Abstract Bib Topics
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, Antoine Girard, and Sriram Sankaranarayanan },
title = { Iterative Computation of Polyhedral Invariants Sets for Polynomial Dynamical Systems },
booktitle = { IEEE Conference on Decision and Control (CDC) },
year = { 2014 },
pages = { 6348-6353 },
publisher = { IEEE Press }}
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).
URL Abstract Bib Topics
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, Sriram Sankaranarayanan, and Erika Abraham },
title = { Under-approximate Flowpipes for Non-linear Continuous Systems },
booktitle = { Formal Methods in Computer-Aided Design (FMCAD) },
year = { 2014 },
pages = { 59-66 },
publisher = { }}
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). Note: Winner of EMSOFT 2015 Best Paper Award
URL Abstract Bib Topics
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 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.
@inproceedings{Zutshi_Others__2014__Multiple,
author = { Aditya Zutshi, Sriram Sankaranarayanan, Jyotirmoy Deshmukh, and James Kapinski },
title = { Multiple-Shooting CEGAR-based falsification for hybrid systems },
booktitle = { Intl. Conference on Embedded Software (EMSOFT) },
year = { 2014 },
pages = { 5:1 - 5:10 },
publisher = { ACM Press }}
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).
URL Abstract Bib Topics
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, Jacques-Henri Jourdan, Sylvie Putot, and Sriram Sankaranarayanan },
title = { Finding Non-Polynomial Positive Invariants and Lyapunov Functions for Polynomial Systems through Darboux Polynomials },
booktitle = { Proc. American Control Conference (ACC) },
year = { 2014 },
pages = { 3571 - 3578 },
publisher = { IEEE Press }}
2013 (6)
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)},
}
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)},
}
2012 (5)
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},
}
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},
}
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.
2011 (3)
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},
}
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)},
}
Theses
Aleksandar Chakarov, Deductive Techniques for Probabilistic Program Analysis, PhD Thesis (July 2016, expected).
Personnel
Sriram Sankaranarayanan (PI).
Aleksandar Chakarov (PhD, CSCI).
Hadi Ravanbakhsh (PhD, CSCI).
Yuen-Lam Voronin (Postdoctoral research associate, CSCI).
Xin Chen (Postdoctoral research associate, CSCI).
Past
Collaborators
Dr. Erika Abraham (RWTH Aachen University).
Profs. Eric Goubault and Sylvie Putot (Ecole Polytechnique, France).
Dr. Pierre Roux (Onera, France).
Software
The Flow* tool is available online.
Upcoming
Polynomial Optimization Solver using Bernstein polynomials.
|