Ashish Tiwari

Project Summary

An invariant of a dynamical system is a region wherein the system remains in any execution. Invariants are useful for analyzing a system. They provide assurance that a complex, possibly safety-critical, system does not ever get into an undesirable, or unsafe, state. The twin tasks of (a) computing an invariant of a system, and (b) checking if a given expression is indeed an invariant -- are both notoriously difficult. In the context of software systems, the concept of an ``inductive invariant'' partly overcomes these two difficulties.

This project performs a systematic exploration of the concept of inductive invariants for continuous dynamical systems and hybrid systems. It builds a constructive theory of inductive invariants that provides computability and complexity results for generating inductive invariants of different forms for such systems. The challenge is to develop scalable techniques for highly nonlinear, nondeterministic, and stochastic systems with unknown parameters. Such systems arise commonly in engineering and science. The approach for invariant discovery is based on reducing the problem to algorithmic problems in symbolic and numeric computation.

As a case study, invariant generation techniques are used to analyze pharmacodynamic and pharmacokinetic models from biomedical literature and verify the safety of medical devices such as insulin pumps. An invariant for an insulin pump would provide bounds for blood glucose concentrations. Invariants are useful for improving reliability of simulation tools. Invariant generation techniques will play a significant role in any fully or partly automated methodology for certifying complex systems.

Results

Publications

• With Susmit Jha and Sanjit Seshia, "Synthesis of Optimal Switching Logic for Hybrid Systems". In Proc. EMSOFT 2011.
• With Sumit Gulwani, Susmit Jha and Ramarathnam Venkatesan, "Synthesis of loop-free programs". PLDI 2011.
• With Ankur Taly and Sumit Gulwani, "Synthesizing switching logic using constraint solving", In Intl. journal on software tools for technology transfer (STTT). SpringerLink.
• With Ankur Taly, "Switching logic synthesis for reachability", In EMSOFT 2010.
• Ashish Tiwari, "Bounded verification of adaptive flight control systems", Proc. AIAA Infotech@Aerospace, 2010. AIAA-2010-3362.
• With Luis Barguno, Guillem Godoy and Eduard Huntingford, "Termination of rewriting with right-flat rules modulo permutative theories", Volume 6, Issue 3, Paper 8, LMCS 2010.
• With Susmit Jha , Sumit Gulwani, and Sanjit Seshia. "Synthesizing Switching Logic for Safety and Dwell-Time Requirements", ICCPS 2010.
• With Susmit Jha, Sumit Gulwani, and Sanjit Seshia, "Oracle-guided component-based program synthesis", ICSE 2010.
• With Adria Gascon, Guillem Godoy, and Manfred Schmidt-Schauss, "Context unification with one context variable", Journal of Symbolic Computation 45(2010), pp 173-193.
• With Ankur Taly, "Deductive Verification of Continuous Dynamical Systems", In FSTTCS'09. Click here for the paper .
• With Guillem Godoy, "Invariant Checking for Programs with Procedure Calls." In SAS'09.
• With Alessandro Abate and Shankar Sastry, "Box Invariance in biologically-inspired dynamical systems." Automatica:45(7). July 2009. pp. 1601-1610. doi:10.1016/j.automatica.2009.02.028.
• Ashish Tiwari, "Formally analyzing adaptive flight control." In NSV II (co-located with CPSWeek 2009).
• With Guillem Godoy, "Invariant Checking for Programs with Procedure Calls." To appear in SAS'09.
• With Ankur Taly and Sumit Gulwani, "Synthesizing Switching Logic using Constraint Solving." In VMCAI 2009.
• With Carolyn Talcott, "Analyzing a Discrete Model of Aplysia Central Pattern Generator", In CMSB 2008. Final version of paper at Springer LNBI page: Click here or here. Download the sal model.
• With Sumit Gulwani, "Constraint-based Approach for Verification and Synthesis of Hybrid Systems", CAV 2008.
• Ashish Tiwari, "Generating Box Invariants", In HSCC 2008.

Talks

• Tutorial at AB 2008, Hagenberg, Austria, July 31 2008.
• Talk at session on "Symbolic Computation and Deduction in System Design and Verification" of ACA 2008 (July 27-30)
• Talk (pdf) at Numerical abstractions for software verification, affiliated to CAV 2008 (July 8, 2008).

Software and benchmarks

• HybridSal
• HybridSal Relational Abstractor
• Exists-Forall Benchmarks and papers
• Verification and Synthesis using SMT Solvers

Other Professional Activities

• HSCC 2011.
• IJCAR 2010 , part of FLoC 2010 .
• LPAR 2010
• VSTTE 2010
• RTA 2009
• ADDCT 2009, Montreal, Canada, Aug 2009. (Program co-chair).
• HSCC 2009, Apr 15-17, 2009, San Francisco (part of CPSWeek).
• LPAR 2008, CMU Campus, Qatar.

Acknowledgments