Ashish Tiwari's Homepage

: Verification, Synthesis, Abstraction, Computability and Control, Applications to Air/Ground Vehicles

2023

A. Khatry, Y. Bajpai, P. Gupta, S. Gulwani, A. Tiwari. Augmented embeddings for custom retrievals.
Z. Liu, S. Deep, A. Fariha, F. Psallidas, A. Tiwari, A. Floratou. Rapidash: Efficient constraint discovery via rapid verification.

A. Khatry, J. Cahoon, J. Henkel, S. Deep, V. Emani, A. Floratou, S. Gulwani, V. Le, M. Raza, S. Shi, M. Singh, A. Tiwari. From words to code: Harnessing data for program synthesis from natural language.
J. Cambronero, S. Gulwani, V. Le, D. Perelman, A. Radhakrishna, C. Simon, A. Tiwari. FlashFill++: Scaling programming by example by cutting to the chase. Proc. ACM Program. Lang. 7(POPL):952-981 (2023)

2022

Z. Wu, V. Le, A. Tiwari, S. Gulwani, A. Radhakrishna, I. Radicek, G. Soares, X. Wang, Z. Li, T. Xie. NL2Viz: Natural language to visualization via contrained syntax-directed synthesis. ESEC/FSE 2022.
Y. Zhang, Y. Bajpai, P. Gupta, A. Ketkar, M. Allamanis, T. Barik, S. Gulwani, A. Radhakrishna, M. Raza, G. Soares, A. Tiwari. Overwatch: Learning patterns in code edit sequences. OOPSLA 2022, Proc ACM on Prog Lang, Vol 6, Issue OOPSLA2, pp 395-423, 2022.
R. Bavishi, H. Joshi, J. Cambronero, A. Fariha, S. Gulwani, V. Le, I. Radicek, A. Tiwari. Neurosymbolic repair for low-code formula languages. Proceedings of the ACM on Programming Languages, Volume 6, Issue OOPSLA2, Article No.: 164, pp 1093-1122.
Andreas Brandstätter, Scott A. Smolka, Scott D. Stoller, Ashish Tiwari, Radu Grosu: Towards drone flocing using relative distance measurements, REoCAS 2022, part of ISOLA 2022.
Gabriel Poesia, Oleksandr Polozov, Vu Le, Ashish Tiwari, Gustavo Soares, Christopher Meek, Sumit Gulwani: Synchromesh: Reliable code generation from pre-trained language models. ICLR 2022. CoRR abs/2201.11227 (2022)
Andreas Brandstätter, Scott A. Smolka, Scott D. Stoller, Ashish Tiwari, Radu Grosu: Multi-Agent Spatial Predictive Control with Application to Drone Flocking (Extended Version). CoRR abs/2203.16960 (2022)

2021

Kia Rahmani, Mohammad Raza, Sumit Gulwani, Vu Le, Daniel Morris, Arjun Radhakrishna, Gustavo Soares, Ashish Tiwari: Multi-modal program inference: a marriage of pre-trained language models and component-based synthesis. Proc. ACM Program. Lang. 5(OOPSLA): 1-29 (2021)
Shouvik Roy, Usama Mehmood, Radu Grosu, Scott A. Smolka, Scott D. Stoller, Ashish Tiwari: Distributed Control for Flocking Maneuvers via Acceleration-Weighted Neighborhooding. ACC 2021: 2745-2750
Anna Fariha, Ashish Tiwari, Arjun Radhakrishna, Sumit Gulwani, Alexandra Meliou: Conformance Constraint Discovery: Measuring Trust in Data-Driven Systems. SIGMOD Conference 2021: 499-512
Anna Fariha, Ashish Tiwari, Alexandra Meliou, Arjun Radhakrishna, Sumit Gulwani: CoCo: Interactive Exploration of Conformance Constraints for Data Understanding and Data Cleaning. SIGMOD Conference 2021: 2706-2710. ACM Sigmod Comprehensive Reproducibility Award
Ashish Tiwari. Linear invariants for linear systems. CoRR abs/2107.09642, 2021.
Ashish Tiwari. A conjecture equivalent to the Collatz conjecture. CoRR abs/2108.06922, 2021.

2020

Xiang Gao, Shraddha Barke, Arjun Radhakrishna, Gustavo Soares, Sumit Gulwani, Alan Leung, Nachiappan Nagappan, Ashish Tiwari: Feedback-driven semi-supervised synthesis of program transformations. Proc. ACM Program. Lang. 4(OOPSLA): 219:1-219:30 (2020)
Shouvik Roy, Usama Mehmood, Radu Grosu, Scott A. Smolka, Scott D. Stoller, Ashish Tiwari: Learning Distributed Controllers for V-Formation. ACSOS 2020: 119-128
Usama Mehmood, Shouvik Roy, Radu Grosu, Scott A. Smolka, Scott D. Stoller, Ashish Tiwari: Neural Flocking: MPC-Based Supervised Learning of Flocking Controllers. FoSSaCS 2020: 1-16
Anna Fariha, Ashish Tiwari, Arjun Radhakrishna, Sumit Gulwani: ExTuNe: Explaining Tuple Non-conformance. SIGMOD Conference 2020: 2741-2744
Ashish Tiwari, Arjun Radhakrishna, Sumit Gulwani, Daniel Perelman. Information-theoretic user interaction: Significant inputs for program synthesis. CoRR abs/2006.12638. 2020

2019

Anders Miltner, Sumit Gulwani, Vu Le, Alan Leung, Arjun Radhakrishna, Gustavo Soares, Ashish Tiwari, Abhishek Udupa. On the fly synthesis of edit suggestions. PACMPL 3(OOPSLA) 2019.
Susmit Jha, Ashish Tiwari, Sanjit A. Seshia, Tuhin Sahai, Natarajan Shankar. TeLEx: Learning signal temporal logic from positive examples using tightness metric. Formal Methods Syst. Des. 54(3): 364-387 (2019)
A. Desai, S. Ghosh, S. A. Seshia, N. Shankar, and A. Tiwari. SOTER: A runtime assurance framework for programming safe robotics systems. DSN 2019. pp 138-150.
Souradeep Dutta, Xin Chen, Susmit Jha, Sriram Sankaranarayanan and Ashish Tiwari. Sherlock - A Tool For Verification Of Neural Network Feedback Systems". HSCC 2019. (Best Demo/poster award)

2018

Marcell Vazquez-Chanlatte, Susmit Jha, Ashish Tiwari, Mark K. Ho, Sanjit A. Seshia. Learning Specifications from Demonstrations. NIPS2018.
Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan and Ashish Tiwari. Output Range Analysis for Deep Feedforward Neural Networks. In NFM 2018.
Usama Mehmood, Nicola Paoletti, Dung Phan, Radu Grosu, Shan Lin, Scott D. Stoller, Ashish Tiwari, Junxing Yang, and Scott A. Smolka. Declarative vs Rule-based Control for Flocking Dynamics. In SAC 2018.

2017

With Susmit Jha, Sanjit Seshia, and N. Shankar. TeLEx: Passive STL learning using only positive examples. In RV 2017.
With Scott A. Smolka, Lukas Esterle, Anna Lukina, Junxing Yang, and Radu Grosu. Attacking the V: On the resiliency of Adaptive-Horizon MPC. In ATVA 2017.
With Adria Gascon, Brent Carmer and Umang Mathur. Look for the proof to find the program: Decorated-Component-Based Program Synthesis. In CAV 2017.
With Anna Lukina, Lukas Esterle, Christian Hirsch, Ezio Bartocci, Junxing Yang, Scott A. Smolka and Radu Grosu. ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans. In TACAS 2017.

2016

With P. Lincoln. A search-based procedure for nonlinear real arithmetic. pdf. Formal Methods in System Design:48:257, June 2016. doi:10.1007/s10703-016-0245-8
Junxing Yang, Radu Grosu, Scott A. Smolka, and Ashish Tiwari. V-formation as optimal control. In 4th Workshop on Biological Distrbuted Algorithms.
Shalini Ghosh, Patrick Lincoln, Ashish Tiwari, and Jerry Zhu. Trusted machine learning for probabilistic models. In Reliable Machine Learning in the Wild. Workshop colocated with ICML 2016.

2015

With Martin Schaef. Severity levels of inconsistent code. In ATVA 2015.
With Adria Gascon and Manfred Schmidt-Schauss. Two-restricted one context unification is in polynomial time. In CSL 2015.
With Adria Gascon and Manfred Schmidt-Schauss. One context unification problems solvable in polynomial time. In LICS 2015.
With Adria Gascon and Bruno Dutertre. Synthesis Using Dual Interpretation. In CADE 2015.
A. Tiwari. Time-Aware Abstractions in HybridSal. In CAV 2015.
A. Tiwari. "Attacking a feedback controller". In Proc. 7th and 8th Intl. Workshop on Numerical Software Verification, NSV 2015. PDF; see also ENTCS Volume 317, pages 141-153.

2014

With A. Gascon, P. Subramanyan, B. Dutertre, D. Jovanovic, and S. Malik. Template-based Circuit Understanding. In FMCAD 2014.
With Adria Gascon. "Synthesis of a simple self-stabilizing system". In Proceedings 3rd SYNT Workshop. arXiv:1407.5392. EPTCS 157, 2014. pp. 5-16.
With P. Lincoln. "A Nonlinear Real Arithmetic Fragment", In CAV 2014. Click here for benchmarks, code, and pdf of the paper.
With Adria Gascon. "A Synthesized Algorithm for Interactive Consistency", In NFM 2014. To appear. See here for SAL models.
With Bruno Dutertre, Dejan Jovanovic, Thomas de Candia, Patrick Lincoln, John Rushby, Dorsa Sadigh, Sanjit Seshia. "Safety Envelope for Security", In HiCoNS 2014.
With Jan Leike. "Synthesis of polynomial lasso programs", In VMCAI 2014. A slightly modified version is here. Link to software.

2013

With Wenchao Li, Adria Gascon, Pramod Subramanyan, Nestan Tsiskaridze, Wei Yang Tan, Sharad Malik, Natarajan Shankar, and Sanjit A. Seshia, Reverse engineering digital circuits using structural and functional analyses. In IEEE Transactions on Emerging Topics in Computing. TETC special issue on emerging nanoscale architectures for security, trust and reliability.
With Parasara Sridhar Duggirala, "Safety verification for linear systems", In EMSOFT 2013. (Best Paper Award)
With Sergio Mover, Alessandro Cimatti and Stefano Tonetta, "Time-aware relational abstraction for Hybrid systems", In EMSOFT 2013.
With Wenchao Li, Adria Gascon, Pramod Subramanyan, Wei Yang Tan, Sharad Malik, Natarajan Shankar, and Sanjit A. Seshia, "WordRev: Finding word-level structures in a sea of bit-level gates". In IEEE Intl. Symp. on Hardware-Oriented Security and Trust, HOST, June 2-3, 2013, Austin.
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.

2012

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.

2011

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. Used as a basis for a synthesizer that is part of LLVM superoptimizer Souper by Raimondas Sasnauskas and John Regehr.
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.

2010

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. (Most Influential Paper award)
With Adria Gascon, Guillem Godoy, and Manfred Schmidt-Schauss, "Context unification with one context variable", Journal of Symbolic Computation 45(2010), pp 173-193.

2009

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.

2008

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.

2007

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.

2006

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.
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.

2005

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.

2004

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 Problem #63 from the RTA list of open problems. In Applicable Algebra in Engineering, Communication and Computing, AAECC 15(1):13-36 (2004), Springer. Link to paper on journal website.
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.
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.

2003

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.

2002

Ashish Tiwari, "Polynomial Time Algorithms for Deciding Confluence of Certain Term Rewrite Systems" , In IEEE Symposium on Logic in Computer Science, LICS 2002. This paper presents a solution of Problem #12 from the RTA list of open problems.
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.

2001

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.

2000

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", In Computers and Operations Research 27 (10), Sept. 2000, pp. 917--934. See also working paper, Sloan School of Management, WP\#3826-95, June 1995.
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.

1999

With Leo Bachmair, C. Ramakrishnan and I.V. Ramakrishnan, "Normalization via Rewrite Closures" , Rewriting Techniques and Applications, Proceedings of the 10th RTA-1999.

1997

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.

Ashish Tiwari

Research Interests

Current Professional Activities

Research Publications (reverse chronological order)

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

2000

1999

1997

Talks/Conference Tutorials

Softwares/ Other Artifacts

Other Papers/Reports

Teaching

Miscellaneous: Old Links