Ashish Tiwari and Bruno Dutertre

Results

Publications

• Parasara Sridhar Duggirala and Ashish Tiwari, "Safety verification for linear systems", In EMSOFT 2013. (Best Paper Award )
• Sergio Mover, Alessandro Cimatti, Ashish Tiwari and Stefano Tonetta, "Time-aware relational abstraction for Hybrid systems", In EMSOFT 2013.
• Aditya Zutshi, Sriram Sankaranarayanan, and Ashish Tiwari, "Timed Relational Abstractions For Sampled Data Control Systems". , In CAV 2012.
• Ashish Tiwari, "HybridSal Relational Abstracter". In CAV 2012.
• Bruno Dutertre, Arvind Easwaran, Brendan Hall, and Wilfried Steiner. "Model-Based Analysis of Timed-Triggered Ethernet", 31st IEEE/AIAA Digital Avionics Systems Conference (DASC) October 2012. (Best paper of the track award)
• Sriram Sankaranarayanan and Ashish Tiwari, "Relational Abstractions for Continuous and Hybrid Systems", In CAV 2011: 686-702.
• Thomas Sturm and Ashish Tiwari, "Verification and Synthesis Using Real Quantifier Elimination". In ISSAC 2011.
• Ankur Taly and Sumit Gulwani and Ashish Tiwari, "Synthesizing switching logic using constraint solving", In Intl. journal on software tools for technology transfer (STTT) 13(6): 519-535 (2011). SpringerLink.
• Ashish Tiwari, "Compositionally analyzing a PI controller formally", In Proc. IEEE Conf. on Decision and Control, CDC 2011.
• Susmit Jha, Sanjit Seshia, Ashish Tiwari. "Synthesis of Optimal Switching Logic for Hybrid Systems". In Proc. EMSOFT 2011.
• Sumit Gulwani, Susmit Jha, Ashish Tiwari and Ramarathnam Venkatesan, "Synthesis of loop-free programs". PLDI 2011.
• Ashish Tiwari, Rewriting in practice. In RTA 2011.
• Wilfried Steiner and Bruno Dutertre, SMT-based formal verification of a TTEthernet synchronization function. In FMICS 2010, LNCS 6371, pp 148-163, 2010. Springer-Verlag.
• Luis Barguno, Guillem Godoy, Eduard Huntingford and Ashish Tiwari, "Termination of rewriting with right-flat rules modulo permutative theories", Volume 6, Issue 3, Paper 8, LMCS 2010.
• Susmit Jha , Sumit Gulwani, Sanjit Seshia, Ashish Tiwari. "Synthesizing Switching Logic for Safety and Dwell-Time Requirements", ICCPS 2010.
• Susmit Jha, Sumit Gulwani, Sanjit Seshia, Ashish Tiwari. "Oracle-guided component-based program synthesis", ICSE 2010.
• Ankur Taly and Ashish Tiwari, "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.
• Ankur Taly and Ashish Tiwari, "Deductive Verification of Continuous Dynamical Systems", In FSTTCS'09.

Tools

• Reduce and Reduce at Sourceforge
• Redlog (Reduce/Redlog can now call qepcad for performing quantifier elimination.)
• Yices
• nlyices
• nonlinear unsatisfiability checker
• HybridSal Relational Abstractor -- A verification tool for hybrid dynamical systems; it can be used to generate nonlinear satisfiability problems.

• slfq
• qepcad
• Singular
• Bernstein strategy in PVS
• nlsat in Z3

Talks/Lectures

• Bruno Dutertre gave lectures on SMT solving and applications at the following events.
  • "Summer School in Formal Techniques" held at Menlo College, Atherton, CA, May 22-27, 2011.
  • "SAT/SMT Solver Summer School 2011" held at MIT, Cambridge MA, June 12-17, 2011.
  • Second International SAT/SMT Summer School held at Trento, Italy, June 12-15, 2012.
  • Second Summer School on Formal Techniques held at Menlo College, Atherton, CA, May 27-June 1, 2012.
• Talks by Ashish:
  • Invited talk at LICS 2011, Fields Institute, Toronto, Jun 21, 2011.
  • Invited talk at RTA 2011, Novi Sad, Serbia, May 31, 2011.
  • Invited talk at ISSAC 2011, Munich, July 26, 2010.

Acknowledgments