Natarajan Shankar

141 papers A* 18A 11B 13C 5Misc 2Journal 32Unranked 53

Year	Rank	Type	Title / Venue / Authors
2026	—	`conf`	PVS as a Proof Obligation Generator. On the Pursuit of Insight and Elegance Natarajan Shankar
2025	J	`jnl`	It's the Specification, Stupid! Commun. ACM Manfred Broy, Harald Ruess, Natarajan Shankar
2024	—	`conf`	MoXI: An Intermediate Language for Symbolic Model Checking. SPIN Kristin Yvonne Rozier, Rohit Dureja, Ahmed Irfan, Chris Johannsen, Karthik Nukala, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi
2024	—	`conf`	Robust Verification of PEG Parser Interpreters. SP (Workshops) Natarajan Shankar, Zephyr Lucas
2024	—	`conf`	The MoXI Model Exchange Tool Suite. CAV (1) Chris Johannsen, Karthik Nukala, Rohit Dureja, Ahmed Irfan, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi, Kristin Yvonne Rozier
2024	—	`ch.`	What Is a Garbage Collector? An Exercise in Compositional Refinement. The Practice of Formal Methods (I) Klaus Havelund, Natarajan Shankar
2023	C	`conf`	An Augmented MetiTarski Dataset for Real Quantifier Elimination Using Machine Learning. CICM John Hester, Briland Hitaj, Grant O. Passmore, Sam Owre, Natarajan Shankar, Eric Yeh
2023	C	`conf`	CoProver: A Recommender System for Proof Construction. CICM Eric Yeh, Briland Hitaj, Sam Owre, Maena Quemener, Natarajan Shankar
2023	J	`jnl`	CoProver: A Recommender System for Proof Construction. CoRR Eric Yeh, Briland Hitaj, Sam Owre, Maena Quemener, Natarajan Shankar
2023	B	`conf`	Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community. FMCAD Kristin Y. Rozier, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi
2023	J	`jnl`	Evidential Transactions with Cyberlogic. CoRR Harald Ruess, Natarajan Shankar
2023	J	`jnl`	Revisiting Variable Ordering for Real Quantifier Elimination using Machine Learning. CoRR John Hester, Briland Hitaj, Grant O. Passmore, Sam Owre, Natarajan Shankar, Eric Yeh
2022	—	`conf`	CDSAT for Nondisjoint Theories with Shared Predicates: Arrays With Abstract Length. SMT Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar
2022	—	`conf`	Capturing the iccMAX calculatorElement: A Case Study on Format Design. SP (Workshops) Vijay H. Kothari, Prashant Anantharaman, Sean W. Smith, Briland Hitaj, Prashanth Mundkur, Natarajan Shankar, Letitia W. Li, Iavor Diatchki, William Harris
2022	J	`jnl`	Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs. J. Autom. Reason. Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar
2022	J	`jnl`	DesCert: Design for Certification. CoRR Natarajan Shankar, Devesh Bhatt, Michael D. Ernst, Minyoung Kim, Srivatsan Varadarajan, Suzanne Millstein, Jorge Navas, Jason Biatek, Huascar Sanchez, Anitha Murugesan, Hao Ren
2022	—	`conf`	Requirements-Driven Model Checking and Test Generation for Comprehensive Verification. NFM Devesh Bhatt, Hao Ren, Anitha Murugesan, Jason Biatek, Srivatsan Varadarajan, Natarajan Shankar
2021	J	`jnl`	2018 CAV award. Formal Methods Syst. Des. Kim G. Larsen, Natarajan Shankar, Pierre Wolper, Somesh Jha
2021	—	`conf`	Semantic parsing of geometry statements using supervised machine learning on synthetic data. CICM Workshops Salwa Tabet Gonzalez, Stéphane Graham-Lengrand, Julien Narboux, Natarajan Shankar
2021	—	`ch.`	The First Fifteen Years of the Verified Software Project. Theories of Programming Peter Müller, Natarajan Shankar
2021	—	`ch.`	The Verified Software Initiative: A Manifesto. Theories of Programming Tony Hoare, Jayadev Misra, Gary T. Leavens, Natarajan Shankar
2020	J	`jnl`	A Verified Packrat Parser Interpreter for Parsing Expression Grammars. CoRR Clement Blaudeau, Natarajan Shankar
2020	B	`conf`	A verified packrat parser interpreter for parsing expression grammars. CPP Clement Blaudeau, Natarajan Shankar
2020	J	`jnl`	Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness. J. Autom. Reason. Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar
2020	B	`conf`	Model-Centered Assurance for Autonomous Systems. SAFECOMP Susmit Jha, John Rushby, Natarajan Shankar
2020	—	`conf`	Research Report: The Parsley Data Format Definition Language. SP (Workshops) Prashanth Mundkur, Linda Briesemeister, Natarajan Shankar, Prashant Anantharaman, Sameed Ali, Zephyr Lucas, Sean W. Smith
2020	B	`conf`	The Correctness of a Code Generator for a Functional Language. VMCAI Nathanaël Courant, Antoine Séré, Natarajan Shankar
2019	—	`conf`	A Refinement Proof for a Garbage Collector. From Reactive Systems to Cyber-Physical Systems Klaus Havelund, Natarajan Shankar
2019	A	`conf`	SOTER: A Runtime Assurance Framework for Programming Safe Robotics Systems. DSN Ankush Desai, Shromona Ghosh, Sanjit A. Seshia, Natarajan Shankar, Ashish Tiwari
2019	J	`jnl`	TeLEx: learning signal temporal logic from positive examples using tightness metric. Formal Methods Syst. Des. Susmit Jha, Ashish Tiwari, Sanjit A. Seshia, Tuhin Sahai, Natarajan Shankar
2018	J	`jnl`	Alonzo Church Award 2018 - Call for Nominations. Bull. EATCS Thomas Eiter, Javier Esparza, Catuscia Palamidessi, Gordon D. Plotkin, Natarajan Shankar
2018	—	`ed.`	Automated Formal Methods, AFM@NFM 2017, Moffett Field, CA, USA, May 19-20, 2017. AFM@NFM Bruno Dutertre, Natarajan Shankar
2018	—	`ch.`	Combining Model Checking and Deduction. Handbook of Model Checking Natarajan Shankar
2018	—	`conf`	Duality-Based Nested Controller Synthesis from STL Specifications for Stochastic Linear Systems. FORMATS Susmit Jha, Sunny Raj, Sumit Kumar Jha, Natarajan Shankar
2018	B	`conf`	Proofs in conflict-driven theory combination. CPP Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar
2018	J	`jnl`	SOTER: Programming Safe Robotics System using Runtime Assurance. CoRR Ankush Desai, Shromona Ghosh, Sanjit A. Seshia, Natarajan Shankar, Ashish Tiwari
2017	—	`conf`	A Brief Introduction to the PVS2C Code Generator. AFM@NFM Natarajan Shankar
2017	J	`jnl`	Alonzo Church Award 2017 - Call for Nominations. Bull. EATCS Natarajan Shankar, Catuscia Palamidessi, Gordon D. Plotkin, Moshe Y. Vardi
2017	—	`conf`	Formalizing Hoare Logic in PVS. SETSS Natarajan Shankar
2017	A	`conf`	Satisfiability Modulo Theories and Assignments. CADE Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar
2017	B	`conf`	TeLEx: Passive STL Learning Using Only Positive Examples. RV Susmit Jha, Ashish Tiwari, Sanjit A. Seshia, Tuhin Sahai, Natarajan Shankar
2016	—	`conf`	ARSENAL: Automatic Requirements Specification Extraction from Natural Language. NFM Shalini Ghosh, Daniel Elenius, Wenchao Li, Patrick Lincoln, Natarajan Shankar, Wilfried Steiner
2016	—	`conf`	Code Generation Using a Formal Model of Reference Counting. NFM Gaspard Férey, Natarajan Shankar
2016	—	`conf`	Contract-Based Verification of Complex Time-Dependent Behaviors in Avionic Systems. NFM Devesh Bhatt, Arunabh Chattopadhyay, Wenchao Li, David Oglesby, Sam Owre, Natarajan Shankar
2016	—	`conf`	Double Helix and RAVEN: A System for Cyber Fault Tolerance and Recovery. CISRC Michele Co, Jack W. Davidson, Jason D. Hiser, John C. Knight, Anh Nguyen-Tuong, Westley Weimer, Jonathan Burket, Gregory L. Frazier, Tiffany M. Frazier, Bruno Dutertre, Ian A. Mason, Natarajan Shankar, Stephanie Forrest
2016	A*	`ed.`	Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016 LICS Martin Grohe, Eric Koskinen, Natarajan Shankar
2015	Misc	`conf`	Automated software winnowing. SAC Gregory Malecha, Ashish Gehani, Natarajan Shankar
2015	A*	`conf`	Design and verification for transportation system security. DAC Bowen Zheng, Wenchao Li, Peng Deng, Léonard Gérard, Qi Zhu, Natarajan Shankar
2015	C	`conf`	Design and verification of multi-rate distributed systems. MEMOCODE Wenchao Li, Léonard Gérard, Natarajan Shankar
2015	J	`jnl`	Identifying Negative Cost Cycles in Strongly Polynomial Space. Nord. J. Comput. Natarajan Shankar, K. Subramani, Pavlos Eirinakis
2014	C	`conf`	A framework for high-assurance quasi-synchronous systems. MEMOCODE Robin Larrieu, Natarajan Shankar
2014	J	`jnl`	Automatically Extracting Requirements Specifications from Natural Language. CoRR Shalini Ghosh, Daniel Elenius, Wenchao Li, Patrick Lincoln, Natarajan Shankar, Wilfried Steiner
2014	J	`jnl`	Reverse Engineering Digital Circuits Using Structural and Functional Analyses. IEEE Trans. Emerg. Top. Comput. Pramod Subramanyan, Nestan Tsiskaridze, Wenchao Li, Adrià Gascón, Wei Yang Tan, Ashish Tiwari, Natarajan Shankar, Sanjit A. Seshia, Sharad Malik
2014	—	`conf`	Software engineering and automated deduction. FOSE Willem Visser, Nikolaj S. Bjørner, Natarajan Shankar
2014	—	`conf`	The Gradual Verifier. NASA Formal Methods Stephan Arlt, Cindy Rubio-González, Philipp Rümmer, Martin Schäf, Natarajan Shankar
2014	—	`conf`	The Semantics of Datalog for the Evidential Tool Bus - (Extended Abstract). Specification, Algebra, and Software Simon Cruanes, Stijn Heymans, Ian A. Mason, Sam Owre, Natarajan Shankar
2013	A	`conf`	Automated Reasoning, Fast and Slow. CADE Natarajan Shankar
2013	J	`jnl`	EFSMT: A Logical Framework for Cyber-Physical Systems. CoRR Chih-Hong Cheng, Natarajan Shankar, Harald Ruess, Saddek Bensalem
2013	A*	`conf`	JBernstein: A Validity Checker for Generalized Polynomial Constraints. CAV Chih-Hong Cheng, Harald Ruess, Natarajan Shankar
2013	B	`conf`	Tool Integration with the Evidential Tool Bus. VMCAI Simon Cruanes, Grégoire Hamon, Sam Owre, Natarajan Shankar
2013	—	`conf`	WordRev: Finding word-level structures in a sea of bit-level gates. HOST Wenchao Li, Adrià Gascón, Pramod Subramanyan, Wei Yang Tan, Ashish Tiwari, Sharad Malik, Natarajan Shankar, Sanjit A. Seshia
2012	B	`conf`	Automatic Dimensional Analysis of Cyber-Physical Systems. FM Sam Owre, Indranil Saha, Natarajan Shankar
2012	A*	`conf`	ModelRob: A Simulink Library for Model-Based Development of robot manipulators. ICRA Indranil Saha, Natarajan Shankar
2012	—	`conf`	The Architecture of Inference from SMT to ETB. SMT@IJCAR Natarajan Shankar
2011	J	`jnl`	A mechanical verification of the stressing algorithm for negative cost cycle detection in networks. Sci. Comput. Program. Natarajan Shankar, K. Subramani
2011	J	`jnl`	SimCheck: a contract type system for Simulink. Innov. Syst. Softw. Eng. Pritam Roy, Natarajan Shankar
2011	—	`conf`	Solving the First Verified Software Competition Problems Using PVS. Formal Modeling: Actors, Open Systems, Biological Systems Sam Owre, Natarajan Shankar
2011	B	`conf`	The 1st Verified Software Competition: Experience Report. FM Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark A. Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, Benjamin Weiß
2010	—	`conf`	Rewriting, Inference, and Proof. WRLA Natarajan Shankar
2010	—	`conf`	SimCheck: An Expressive Type System for Simulink. NASA Formal Methods Pritam Roy, Natarajan Shankar
2010	—	`conf`	The Mechanical Verification of a DPLL-Based Satisfiability Solver. LSFA Natarajan Shankar, Marc Vaucher
2010	—	`conf`	Unraveling a Card Trick. Essays in Memory of Amir Pnueli Tony Hoare, Natarajan Shankar
2009	J	`jnl`	Automated deduction for verification. ACM Comput. Surv. Natarajan Shankar
2009	—	`conf`	System Support for Forensic Inference. IFIP Int. Conf. Digital Forensics Ashish Gehani, Florent Kirchner, Natarajan Shankar
2009	J	`jnl`	The verified software initiative: A manifesto. ACM Comput. Surv. C. A. R. Hoare, Jayadev Misra, Gary T. Leavens, Natarajan Shankar
2008	—	`conf`	A Brief Overview of PVS. TPHOLs Sam Owre, Natarajan Shankar
2008	—	`conf`	Fixpoints and Search in PVS. LASER Summer School Natarajan Shankar
2008	B	`conf`	Trust and Automation in Verification Tools. ATVA Natarajan Shankar
2008	—	`ed.`	Verified Software: Theories, Tools, Experiments, Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings VSTTE Natarajan Shankar, Jim Woodcock
2007	A*	`conf`	A Tutorial on Satisfiability Modulo Theories. CAV Leonardo Mendonça de Moura, Bruno Dutertre, Natarajan Shankar
2006	A	`ed.`	Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings IJCAR Ulrich Furbach, Natarajan Shankar
2005	—	`conf`	Inference Systems for Logical Algorithms. FSTTCS Natarajan Shankar
2004	—	`conf`	Justifying Equality. D/PDPAR@IJCAR Leonardo Mendonça de Moura, Harald Rueß, Natarajan Shankar
2004	A*	`conf`	SAL 2. CAV Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar, Maria Sorea, Ashish Tiwari
2004	A	`conf`	The ICS Decision Procedures for Embedded Deduction. IJCAR Leonardo Mendonça de Moura, Sam Owre, Harald Rueß, John M. Rushby, Natarajan Shankar
2003	J	`jnl`	Invisible formal methods for embedded control systems. Proc. IEEE Ashish Tiwari, Natarajan Shankar, John M. Rushby
2002	—	`conf`	Combining Shostak Theories. RTA Natarajan Shankar, Harald Rueß
2002	A	`conf`	Formal Verification of a Combination Decision Procedure. CADE Jonathan Ford, Natarajan Shankar
2002	—	`conf`	Little Engines of Proof. FME Natarajan Shankar
2002	A*	`conf`	Little Engines of Proof. LICS Natarajan Shankar
2002	—	`conf`	Verification by Abstraction. 10th Anniversary Colloquium of UNU/IIST Natarajan Shankar
2001	A	`conf`	A Technique for Invariant Generation. TACAS Ashish Tiwari, Harald Rueß, Hassen Saïdi, Natarajan Shankar
2001	A*	`conf`	Deconstructing Shostak. LICS Harald Rueß, Natarajan Shankar
2001	A*	`conf`	ICS: Integrated Canonizer and Solver. CAV Jean-Christophe Filliâtre, Sam Owre, Harald Rueß, Natarajan Shankar
2001	C	`conf`	Static Analysis for Safe Destructive Updates in a Functional Language. LOPSTR Natarajan Shankar
2001	—	`conf`	Using Decision Procedures with a Higher-Order Logic. TPHOLs Natarajan Shankar
2000	B	`conf`	Combining Theorem Proving and Model Checking through Symbolic Analysis. CONCUR Natarajan Shankar
2000	—	`conf`	Symbolic Analysis of Transition Systems. Abstract State Machines Natarajan Shankar
1999	—	`conf`	A case-study in component-based mechanical verification of fault-tolerant programs. WSS Sandeep S. Kulkarni, John M. Rushby, Natarajan Shankar
1999	A*	`conf`	Abstract and Model Check While You Prove. CAV Hassen Saïdi, Natarajan Shankar
1999	J	`jnl`	Modular Verification of SRT Division. Formal Methods Syst. Des. Harald Rueß, Natarajan Shankar, Mandayam K. Srivas
1999	—	`conf`	Principles and Pragmatics of Subtyping in PVS. WADT Natarajan Shankar, Sam Owre
1998	—	`conf`	Fair Synchronous Transition Systems and Their Liveness Proofs. FTRTFT Amir Pnueli, Natarajan Shankar, Eli Singerman
1998	—	`conf`	PVS: An Experience Report. FM-Trends Sam Owre, John M. Rushby, Natarajan Shankar, David W. J. Stringer-Calvert
1998	J	`jnl`	Subtypes for Specifications: Predicate Subtyping in PVS. IEEE Trans. Software Eng. John M. Rushby, Sam Owre, Natarajan Shankar
1998	—	`conf`	Verifying a self-stabilizing mutual exclusion algorithm. PROCOMET Shaz Qadeer, Natarajan Shankar
1997	Misc	`conf`	Industrial Strength Formal Verification Techniques for Hardware Designs. VLSI Design Sreeranga P. Rajan, Natarajan Shankar, Mandayam K. Srivas
1997	A	`conf`	Integration in PVS: Tables, Types, and Model Checking. TACAS Sam Owre, John M. Rushby, Natarajan Shankar
1997	—	`conf`	Lazy Compositional Verification. COMPOS Natarajan Shankar
1996	—	`conf`	Experiments in Theorem Proving and Model Checking for Protocol Verification. FME Klaus Havelund, Natarajan Shankar
1996	A*	`conf`	Modular Verification of SRT Division. CAV Harald Rueß, Natarajan Shankar, Mandayam K. Srivas
1996	A	`conf`	On Shostak's Decision Procedure for Combinations of Theories. CADE David Cyrluk, Patrick Lincoln, Natarajan Shankar
1996	A*	`conf`	PVS: Combining Specification, Proof Checking, and Model Checking. CAV Sam Owre, S. Rajan, John M. Rushby, Natarajan Shankar, Mandayam K. Srivas
1996	B	`conf`	PVS: Combining Specification, Proof Checking, and Model Checking. FMCAD Natarajan Shankar
1996	J	`jnl`	Steps Toward Mechanizing Program Transformations Using PVS. Sci. Comput. Program. Natarajan Shankar
1996	—	`conf`	Unifying Verification Paradigms. FTRTFT Natarajan Shankar
1995	A*	`conf`	An Integration of Model Checking with Automated Proof Checking. CAV S. Rajan, Natarajan Shankar, Mandayam K. Srivas
1995	B	`conf`	Computer-Aided Computing. MPC Natarajan Shankar
1995	A*	`conf`	Decision Problems for Second-Order Linear Logic LICS Patrick Lincoln, Andre Scedrov, Natarajan Shankar
1995	J	`jnl`	Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE Trans. Software Eng. Sam Owre, John M. Rushby, Natarajan Shankar, Friedrich W. von Henke
1994	—	`conf`	A Tutorial on Using PVS for Hardware Verification. TPCD Sam Owre, John M. Rushby, Natarajan Shankar, Mandayam K. Srivas
1994	—	`conf`	Effective Theorem Proving for Hardware Verification. TPCD David Cyrluk, S. Rajan, Natarajan Shankar, Mandayam K. Srivas
1994	—	`book`	Metamathematics, machines, and Gödels's proof. Natarajan Shankar
1994	—	`conf`	Proof Search (Tutorial). ICLP Workshop: Proof-Theoretical Extensions on Logic Programming Roy Dyckhoff, Natarajan Shankar
1994	A*	`conf`	Proof Search in First-Order Linear Logic and Other Cut-Free Sequent Calculi LICS Patrick Lincoln, Natarajan Shankar
1994	—	`conf`	Towards a Duration Calculus Proof Assistant in PVS. FTRTFT Jens Ulrik Skakkebæk, Natarajan Shankar
1994	—	`conf`	Using Proof Theory to Optimize Proof Search. ICLP Workshop: Proof-Theoretical Extensions on Logic Programming Natarajan Shankar
1993	J	`jnl`	David A. McAllester, Ontic: A Knowledge Representation System for Mathematics. Artif. Intell. Natarajan Shankar
1993	—	`conf`	Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned. FME Sam Owre, John M. Rushby, Natarajan Shankar, Friedrich W. von Henke
1993	J	`jnl`	Linearizing Intuitionistic Implication. Ann. Pure Appl. Log. Patrick Lincoln, Andre Scedrov, Natarajan Shankar
1993	A*	`conf`	Verification of Real-Time Systems Using PVS. CAV Natarajan Shankar
1992	J	`jnl`	Decision Problems for Propositional Linear Logic. Ann. Pure Appl. Log. Patrick Lincoln, John C. Mitchell, Andre Scedrov, Natarajan Shankar
1992	—	`conf`	Mechanical Verification of a Generalized Protocol for Byzantine Fault Tolerant Clock Synchronization. FTRTFT Natarajan Shankar
1992	A	`conf`	PVS: A Prototype Verification System. CADE Sam Owre, John M. Rushby, Natarajan Shankar
1992	A	`conf`	Proof Search in the Intuitionistic Sequent Calculus. CADE Natarajan Shankar
1991	—	`conf`	From formal verification to silicon compilation. Compcon Jeffrey Joyce, Erwin Liu, John M. Rushby, Natarajan Shankar, Roberto Suaya, Friedrich W. von Henke
1991	A*	`conf`	Linearizing Intuitionistic Implication LICS Patrick Lincoln, Andre Scedrov, Natarajan Shankar
1990	A*	`conf`	Decision Problems for Propositional Linear Logic FOCS Patrick Lincoln, John C. Mitchell, Andre Scedrov, Natarajan Shankar
1988	J	`jnl`	A mechanical proof of the Church-Rosser theorem. J. ACM Natarajan Shankar
1988	J	`jnl`	Efficient Parallel Circuits and Algorithms for Division. Inf. Process. Lett. Natarajan Shankar, V. Ramachandran
1985	J	`jnl`	Towards Mechanical Metamathematics. J. Autom. Reason. Natarajan Shankar