Ashish Tiwari

Research Interests

Current Professional Activities

• Program Committees/External Review Committee: Please consider submitting to the following conferences:
  • CADE 2013
  • FroCoS 2013
  • FOSSACS 2013
  • FORMATS 2011
  • FSTTCS 2011
  • POPL 2012 (ERC)
  • HSCC 2012, HSCC 2013 (mid Apr)
  • Past PC Participation . Click here for New Talks .
• Projects
  • Invariants for continuous and hybrid systems.
  • SMT-Solving, Reals, Applications.
  • Fault-tolerant distributed systems
  • Verification and Synthesis using SMT Solvers
  • Certificate-Based Verification: Tools and Benchmarks
  • Relational Abstraction

Research Publications (reverse chronological order)

• With Steven Eker, Markus Krummenacker, Alexander Shearer, Ingrid Keseler, Carolyn Talcott, and Peter Karp, "Computing minimal nutrient sets from metabolic networks via linear constraint solving". BioMed Central BMC Bioinformatics 14:114, 2013. URL.
• With Aditya Zutshi and Sriram Sankaranarayanan, "Timed Relational Abstractions For Sampled Data Control Systems". , In CAV 2012.
• Ashish Tiwari, "HybridSal Relational Abstracter". In CAV 2012.
• Ashish Tiwari, "Compositionally analyzing a PI controller family", In Proc. IEEE Conf. on Decision and Control, CDC 2011.
• With Susmit Jha and Sanjit Seshia, "Synthesis of Optimal Switching Logic for Hybrid Systems". In Proc. EMSOFT 2011.
• With Sriram Sankaranarayanan, "Relational Abstractions for Continuous and Hybrid Systems", In CAV 2011: 686-702.
• With Thomas Sturm, "Verification and synthesis using real quantifier elimination". In ISSAC 2011.
• With Sumit Gulwani, Susmit Jha and Ramarathnam Venkatesan, "Synthesis of loop-free programs". PLDI 2011.
• With Sumit Gulwani and Vijay Korthikanti, "Synthesizing geometry constructions". 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. Vol 13, Issue 6 (2011), 519-535.
• 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 Carles Creus, Guillem Godoy and Francesc Massanes, "Non-linear rewrite closure and weak normalization." In LICS'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.
• Ashish Tiwari, "Abstractions for Hybrid Systems" , In FMSD 2008.
• With S. Gulwani and Bill McCloskey, "Lifting Abstract Interpreters to Quantified Abstract Domains". (Full version). In POPL 2008.
• With Alessandro Abate, Yu Bai, Nathalie Sznajder, and Carolyn Talcott. "Quantitative and Probabilitic Modeling in Pathway Logic". In BIBE 2007. (Won the Best Student Paper Award)
• With A. Abate and S. Sastry, "Box invariance for biologically-inspired dynamical systems". In CDC 2007.
• With S. Gulwani, "Logical Interpretation: Static Program Analysis Using Theorem Proving". In CADE-21, 2007. (Invited Paper)
• With Guillem Godoy, "Termination of rewriting with right-flat rules". In Proc. RTA 2007.
• With Sumit Gulwani, Static Analysis of Heap Manipulating Low-level Software(in pdf). slides(in ppt). In Proc. CAV 2007.
• With C. Talcott, M. Knapp, P. Lincoln, and K. Laderoute, "Analyzing Pathways using SAT-based approaches". In Algebraic Biology 2007, July 2-4, 2007, Hagenberg, Austria.
• With Sumit Gulwani, Computing Procedure Summaries for Interprocedural Analysis". In ESOP 2007.
• With Sumit Gulwani, "Assertion checking unified"(in ps). In VMCAI 2007. Preliminary version also available as MSR-TR-2006-99.
• With Rajesh Kumar and Bruce Krogh, "EOLC: Efficiently modeling inconsistency for commonsense reasoning". In MVLPA 2006 .
• With Alessandro Abate, "Box invariance of Hybrid and Switched Systems", In 2nd IFAC Conference on Analysis and Design of Hybrid Systems, ADHS 2006. Full paper .
• With S. Gulwani, "Combining abstract interpreters". PLDI 2006. This paper introduces the logical product of two logical lattices. It then shows that abstract interpreters over the individual logical lattices can be combined to yield the most precise abstract interpreter over the logical product under certain conditions on the logical theories defining the logical lattices. The combination result (and the conditions) are inspired by the Nelson-Oppen combination result for deciding satisfiability in the disjoint union of stably-infinite theories.
• With S. Gulwani, "Assertion Checking in the Combined Abstraction of Linear Arithmetic and Uninterpreted Functions" . ESOP 2006. This paper shows that assertion checking over the combination of two logical lattices can be hard, even when it is PTime over the individual lattices.
• With Linda Briesemeister and Phil A. Porras, "Model checking of worm quarantine and counter-quarantine under a group defense", SRI Technical Report, Oct 2005.
• With G. Godoy, "Confluence of shallow right-linear rewrite systems". In CSL 2005. We show that the following problem is surprisingly decidable: given a shallow and right-linear rewrite system, determine if it is confluent. (Preliminary version, to be revised)
• A. Tiwari, "An algebraic approach to the satisfiability of nonlinear constraints". In CSL 2005. This paper presents a pragmatic and powerful sound and refutationally complete method for testing satisfiability of nonlinear constraints over the reals. (Preliminary version, to be revised)
• With Guillem Godoy, Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules . In CADE 2005. (Preliminary version, to be revised)
• With E. Rodriguez-Carbonell, "Generating Polynomial Invariants for Hybrid Systems", In Hybrid Systems: Computation and Control 2005.
• With S. Gulwani and G. Necula, "Join Algorithms for the theory of uninterpreted functions", In K. Lodaya and M. Mahajan (eds.) FSTTCS 2004, Vol 3328 of LNCS, p.311-323, 2004. In postscript.
• A. Tiwari, "Termination of linear programs" . In CAV 2004. This paper shows decidability of termination for a class of linear loop programs.
• With Guillem Godoy, "Deciding fundamental properties of right-ground or right-variable systems by rewrite closure". In IJCAR 2004. This paper shows decidability of properties such as reachability, joinability, confluence, and termination for TRSs containing right-ground or collapsing rules.
• With Leonardo de Moura, Sam Owre, Harald Ruess, John Rushby, N. Shankar, and Maria Sorea, SAL 2 . In CAV 2004.
• With Guillem Godoy and Rakesh Verma, "Confluence characterization using rewrite closure with application to right ground systems". This paper presents a solution of open problem #63 from the RTA list of open problems. In AAECC.
• With P. Lincoln, " "Symbolic systems biology: Hybrid modeling and analysis of biological networks" , In HSCC 2004.
• With N. Berregeb and R. Robbana, "Toward Automatic Proofs of Observational Properties" , Discrete Mathematics and Theoretical Computer Science 6(2), 143--162, 2004.
• With G. Khanna, " Nonlinear Systems: Approximating Reach Sets ", In HSCC 2004.
• With Guillem Godoy and Rakesh Verma, "Deciding confluence of certain term rewriting systems in polynomial time", Annals of Pure and Applied Logic , APAL 130(1-3):33-59, December 2004.
• Ashish Tiwari, "Abstraction based theorem proving: An example from the theory of reals", In the proceedings of the PDPAR 2003 workshop, colocated with CADE 2003 .
• Ashish Tiwari, "Approximate Reachability for Linear Systems", In the Proceedings of Hybrid Systems: Computation and Control, HSCC 2003.
• With Ronojoy Ghosh and Claire Tomlin, "Automated Symbolic Reachability Analysis with Application to Delta-Notch Signaling Automata", In the Proceedings of Hybrid Systems: Computation and Control, HSCC 2003.
• With Guillem Godoy and Rakesh Verma, "On the confluence of linear shallow term rewrite systems", In STACS 2003 , 20th International Symposium on Theoretical Aspects of Computer Science, Feb 27--Mar 01, 2003.
• With N. Shankar and J. Rushby, "Invisible formal methods for embedded control systems", In Proc of the IEEE, Special issue on Embedded Systems, Jan 2003.
• With Guillem Godoy and Robert Nieuwenhuis, "Classes of Term Rewrite Systems with Polynomial Confluence Problems", (journal article) In TOCL , Volume 5, Number 2 (April 2004). pdf.
• Ashish Tiwari, "Polynomial Time Algorithms for Deciding Confluence of Certain Term Rewrite Systems" , In IEEE Symposium on Logic in Computer Science, LICS 2002. Context.
• With G. Khanna, "Series of Abstractions for Hybrid Automata" , In Hybrid Systems: Computation and Control, HSCC 2002.
• With Leo Bachmair and Laurent Vigneron, "Abstract Congruence Closure" , J. of Automated Reasoning 31(2), 2003, pp. 129--168, Kluwer Academic Publishers.
• Ashish Tiwari, "Rewrite Closures for Ground and Cancellative AC Theories" , In FST&TCS 2001, LNCS 2245.
• With Harald Ruess, Hassen Saidi and N. Shankar, "Automatic Generation of Invariants" , In TACAS 2001 - Tools and Algorithms for the Construction and Analysis of Systems.
• S. Bensalem, et. al., "An overview of SAL", In Langley Workshop on Formal Methods, LFMW 2000 .
• With Leo Bachmair, "Abstract Congruence Closure and Specializations" , 17th Intl Conference on Automated Deduction, CADE 2000 .
• With Leo Bachmair and Harald Ruess, "Rigid E-Unification Revisited" , 17th Intl Conference on Automated Deduction, CADE 2000 .
• With R. K. Ahuja and James B. Orlin, "A Greedy Genetic Algorithm for the Quadratic Assignment Problem", Working paper, Sloan School of Management, WP\#3826-95, June 1995. Also in Computers and Operations Research 27 (10), Sept. 2000, pp. 917--934.
• With Leo Bachmair, I.V. Ramakrishnan, and L. Vigneron, "Congruence Closure modulo Associativity and Commutativity", Workshop on Frontiers of Combining Systems, FroCos 2000 , LNAI 1794.
• With Leo Bachmair, C. Ramakrishnan and I.V. Ramakrishnan, "Normalization via Rewrite Closures" , Rewriting Techniques and Applications, Proceedings of the 10th RTA-1999 .
• With Leo Bachmair, "D-bases for Polynomial Ideals over Commutative Noetherian Rings" , Rewriting Techniques and Applications, Proceedings of the 8th RTA-1997 , pp. 113-127.

Disseration/Conference Tutorials/Talks

• Invited talk at LICS 2011, Fields Institute, Toronto, Jun 21, 2011. New!
• Invited talk at RTA 2011, Novi Sad, Serbia, May 31, 2011. New!
• Talk at MSR, Redmond, Mar 25, 2011. New!
• Talk at ISSAC 2011, San Jose, June 11, 2011. New!
• Invited talk at ISSAC 2011, Munich, July 26, 2010.
• Slides of the talk at FroCoS'09
• 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)
• Stochastic modeling and analysis of biological networks, Workshop on Biosecurity (in pdf), May 8, 2007, Baltimore.
• Combining abstract interpreters, Stanford talk (in pdf).
• With Harald Ruess and N. Shankar, On Shostak's Combination of Decision Procedures. Tutorial at CADE 2002, Copenhagen. Click on the above link for slides.
• Decision procedures in automated deduction, Dissertation pdf , Department of Computer Science, State University of New York at Stony Brook, 2000. Advisor Prof. Leo Bachmair.
• Decision procedures summer school: Aug 9-11, Stanford .

Software

• HybridSal
• HybridSal Relational Abstractor New!
• Draper clock sync model in SAL
• Heuristic Nonlinear Solver
• Documentation for HybridSal . SBML2HybridSal .
• Ashish Tiwari and Laurent Vigneron, Implementation of Abstract Congruence Closure with randomly generated CC problem instances (gzipped tar file) , see the CADE 2000 paper for details.
• Ashish Tiwari, R. K. Ahuja, and J. Orlin, GA source code (tar file) , see the QAP paper for details. Click here (tar file) for the benchmark data for QAP.
• Ashish Tiwari, Linking QEPCAD with PVS .

Other Papers

• With Sumit Gulwani, "Assertion checking unified"(in pdf). Microsoft Research Technical Report MSR-TR-2006-99.
• A. Tiwari, Formal Semantics and Analysis Methods for Simulink Stateflow Models .
• Leo Bachmair and Ashish Tiwari, "Congruence Closure and Syntactic Unification", In 14th Intl Workshop on Unification, UNIF 2000 .

Talks

• Talk (pdf) at Numerical abstractions for software verification 2, affiliated to CPSWeek 2009 (Apr 2009).
• Talk (pdf) at Numerical abstractions for software verification, affiliated to CAV 2008 (July 8, 2008).
• Invited Talk at CADE-21, 2007.
• Hybrid modeling and analysis of biological networks. Talk at the Workshop on Logic in Systems Biology, LSB, co-located with FLoC 2006, Aug 15, 2006.
• Hybrid modeling and analysis of genetic networks. Talk at Univ of Notre Dame, Feb 27, 2004.
• "Symbolic techniques for verification of hybrid systems" (ps) , Talk at CMU, Sep 30, 2003. (HybridAbstraction + Composition + Systems Biology)
• BioSpice DC Talk (pdf).
• Dagstuhl 2005 Talk (assertion checking and unification) (pdf).
• "Symbolic methods for verification of hybrid systems" (ps) , Presentation at the NASA Ames Research Center, Mountain View, CA, June 17, 2003. Talks with the only slightly different content were also given at Dagstuhl Seminar on Theorem Proving and Infinite State Model-Checking (April 21--25, 2003), and MPI Saarbrucken (April 30--May 2, 2003).
• "Symbolic methods for verification of hybrid systems" (ps) , Presentation at the Hybrid Systems Seminar series, University of Pennsylvania, Philadelphia, Feb 28, 2003.
• "Combining Decision Procedures" (pdf) , Presentation at the Stanford Logic Seminar, Oct 15, 2002. Also available in in postscript .
• "SRI/UT Proposal Slides for NEST" (pdf) , Also available in 4up format (pdf) .
• Al Mok, "SRI/UT Demo Plan for NEST" (ppt) , Presentation for the NEST OEP Meeting at St. Louis, Aug 23rd. See here and here for postscript.
• With Pat Lincoln and John Rushby, "Formal Composition for Time-Triggered Systems" , Presentation for the MoBIES PI meeting at New York on July 25th.
• A. Tiwari, "Stanford Talk" .
• A. Tiwari, "Uniform description of efficient decision procedures using extended signatures" , MacLean Hall, Computer Science Department, University of Iowa, Iowa City, Mar 1, 2002. In pdf
• A. Tiwari, "Formal Methods for Analysis of Hybrid Systems" , Room 339, Cory Hall, UC Berkeley, Feb 11, 2002.
• A. Tiwari, "Formal Methods for Analysis of Hybrid Systems" , Durand 026, Stanford University, Dec 07, 2001.
• A. Tiwari, "Formal Composition for Time-Triggered Systems" , Presented at MoBIES ESWG meeting at Dearbon.
• Ashish Tiwari, "Abstract Congruence Closure and Applications", Dagstuhl seminar on Deduction, Seminar No. 99091, Report No. 232, U. Furbach (Koblenz), H. Ganzinger (MPI-Saarbrücken), D. Kapur (Albany), 28 Feb--5 March 1999.
• Ashish Tiwari, "Grobner bases for polynomial ideals over commutative Noetherian rings", Talk given at Chennai Mathematical Institute, Jan. 1999.
• Ashish Tiwari, "Decision Procedures in Automated Deduction", Preliminary Examination Report, PhD Proposal, SUNY at Stony Brook, Nov 1998.

Miscellaneous Areas: Reports

• Ashish Tiwari, "Adding BDD's to the Concurrency Factory's Local Model Checker", CSE 635 Asynchronous Systems, Project Report, Spring 1997.
• Zhong Li and Ashish Tiwari, "Addition Chain Heuristics/RSA Public Key Cryptosystem", CSE 502 Computer Architecture, Project Report, Spring 1996.
• Ashish Tiwari, "Identifying Mathematical and Logical Sequences", CSE 539 Expert Systems, Project Report, Spring 1996.
• Ashish Tiwari, "Group Testing", (.ps.Z) CSE 648 Advanced Algorithms, Project Report, Fall 1995.
• Ashish Tiwari, "Sweeping a 3-D Tetrahedral Complex", CSE 528 Computer Graphics, Project Report, Fall 1995. Appeared as part of "Fast Rendering of Irregular Grids", by Claudio T.Silva, J.S.B. Mitchell and Arie E. Kaufman, ACM/IEEE Volume Visualization Symposium 1996, pp. 15--22.

Teaching

• Fall 2003: CS359: Little Engines of Proof, Stanford University.
• Automata Theory, Summer (1997) term special couse for incoming graduate students, SUNY-Stony Brook.
• Teaching Assistant for CSE 113 "Foundations of Computer Science I", Fall 1995, Instructor: Prof. P.B.Henderson.
• Teaching Assistant for CSE 213, "Foundations of Computer Science II", Spring 1996, Instructor: Prof. Leo Bachmair.
• Teaching Assistant for CSE 506, "Operating Systems", Spring 1996, Instructor: Prof. Gene Stark.

Miscellaneous: Useful Links/Upcoming Conferences

• SRI Insider IEEE info.
• Personal Page, for photographs.
• Past PC participation:
  • RTA 2012 :
    • Call for papers in pdf [ Updated: Dec 19, 2011 ].
    • Call for papers in text [ Updated: Dec 19, 2011 ].
  • Co-organized TPTPA: Theorem proving tools in program analysis: Tutorial on theorem proving techniques and tools, Co-located with POPL 2011 in Austin, Texas.
  • Steering Committee Member and Publicity Chair for RTA (2005-2008).
  • CAV 2011 (Jan14-Mar19-Jul16-20)
  • ISSAC 2011 (Jan 8/14-Mar 4-Jun 8-11), part of FCRC , Jun 4-11, San Jose.
  • IJCAR 2010 , part of FLoC 2010 . Deadline: Jan 15/22, 2010
  • LPAR 2010
  • VSTTE 2010
  • HSCC 2009,2011.
  • RTA 2009
  • Algebraic Biology 2009 was cancelled.
  • ADDCT 2009, Montreal, Canada, Aug 2009. (Program co-chair). Paper deadline May 1.
  • LPAR 2008, CMU Campus, Qatar.
  • CEDAR 2008(19May)
  • LICS 2008, Pittsburgh
  • IJCAR 2008, Sydney, 2008.
  • AB 2008, Hagenberg, Austria, July 31-Aug 2, 2008.
  • ADDCT 2007, Bremen, Germany, July 15, 2007. (Program co-chair)
  • CSL 2007, Lausanne, Sept 11-15, 2007.
  • CAV 2007, Berlin, July 3-7, 2007.
  • FSTTCS 2007, Delhi, Dec 2007.
  • SMT 2007, Berlin, July 1-2, 2007.
  • Algebraic Biology 2007, July 2-4, 2007, Hagenberg, Austria.
  • HSCC 2006: Hybrid Systems: Computation and Control, Mar 29--31, Santa Barbara (Program Chair).
  • RTA 2006: Rewriting Techniques and Applications, Aug 12-15, 2006, Seattle, Wasington
  • PDPAR 2006: Pragmatics of Decision Procedures in Automated Reasoning, Aug 21, 2006, Seattle, Wasington
  • FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, Dec 13-15, 2006, Indian Statistical Institute (ISI), Kolkata
  • LPAR-12, 2005: 12th Intl. Conf. on Logic for Programming Artificial Intelligence and Reasoning, Montego Bay, Jamaica, 2nd-6th Dec 2005.
  • FroCoS 2005: Frontiers of Combining Systems, Sept 19-21, 2005, Vienna.
  • CADE-20, 2005: Conf. on Automated Deduction.
  • HSCC-2005: Hybrid Systems: Computation and Control, Mar 9--11, Zurich.
  • IJCAR 2004: Intl Joint Conf on Automated Reasoning .
  • RTA 2004: Intl Conf on Rewriting Techniques and Applications.
  • HSCC 2003: Hybrid Systems: Computation and Control .
  • RTA 2003: Rewriting Techniques and Applications RTA 2003. See also RDP03-RTA page.
  • PDPAR 2003: Pragmatics of Decision Procedures in Automated Reasoning 2003.
• Stefan Ratschan, Applications of the decision procedure for reals .
• Funding: NSF CISE page , NIH guide for grants and contracts, with links to PAs and RFAs , Darpa solicitations .
• Generic conference pages: FSTTCS, LPAR, CSL , IEEE Symposium on Logic in Computer Science , LICS newsletter ,
• DBLP, my link .

Off : EL 270, SRI Intl., 333 Ravenswood Ave, Menlo Park, CA 94025. Tel : 650-859-4774
Web : Personal home page