Natarajan Shankar

Orcid: 0000-0002-8652-8871

Affiliations:
  • SRI International, Menlo Park, CA, USA


According to our database1, Natarajan Shankar authored at least 128 papers between 1985 and 2024.

Collaborative distances:
  • Dijkstra number2 of two.
  • Erdős number3 of three.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
MoXI: An Intermediate Language for Symbolic Model Checking.
Proceedings of the Model Checking Software - 30th International Symposium, 2024

Robust Verification of PEG Parser Interpreters.
Proceedings of the IEEE Security and Privacy, 2024

The MoXI Model Exchange Tool Suite.
Proceedings of the Computer Aided Verification - 36th International Conference, 2024

2023
Evidential Transactions with Cyberlogic.
CoRR, 2023

Revisiting Variable Ordering for Real Quantifier Elimination using Machine Learning.
CoRR, 2023

CoProver: A Recommender System for Proof Construction.
Proceedings of the Intelligent Computer Mathematics - 16th International Conference, 2023

An Augmented MetiTarski Dataset for Real Quantifier Elimination Using Machine Learning.
Proceedings of the Intelligent Computer Mathematics - 16th International Conference, 2023

Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community.
Proceedings of the Formal Methods in Computer-Aided Design, 2023

2022
Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs.
J. Autom. Reason., 2022

DesCert: Design for Certification.
CoRR, 2022

Capturing the iccMAX calculatorElement: A Case Study on Format Design.
Proceedings of the 43rd IEEE Security and Privacy, 2022

CDSAT for Nondisjoint Theories with Shared Predicates: Arrays With Abstract Length.
Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), 2022

Requirements-Driven Model Checking and Test Generation for Comprehensive Verification.
Proceedings of the NASA Formal Methods - 14th International Symposium, 2022

2021
2018 CAV award.
Formal Methods Syst. Des., 2021

Semantic parsing of geometry statements using supervised machine learning on synthetic data.
Proceedings of the Joint Proceedings of the FMM, FVPS, MathUI,NatFoM, and OpenMath Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2021 co-located with the 14th Conference on Intelligent Computer Mathematics (CICM 2021), Virtual Event, Timisoara, Romania, July 26, 2021

The Verified Software Initiative: A Manifesto.
Proceedings of the Theories of Programming: The Life and Works of Tony Hoare, 2021

The First Fifteen Years of the Verified Software Project.
Proceedings of the Theories of Programming: The Life and Works of Tony Hoare, 2021

2020
Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness.
J. Autom. Reason., 2020

The Correctness of a Code Generator for a Functional Language.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2020

Research Report: The Parsley Data Format Definition Language.
Proceedings of the 2020 IEEE Security and Privacy Workshops, 2020

Model-Centered Assurance for Autonomous Systems.
Proceedings of the Computer Safety, Reliability, and Security, 2020

A verified packrat parser interpreter for parsing expression grammars.
Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

2019
TeLEx: learning signal temporal logic from positive examples using tightness metric.
Formal Methods Syst. Des., 2019

SOTER: A Runtime Assurance Framework for Programming Safe Robotics Systems.
Proceedings of the 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, 2019

A Refinement Proof for a Garbage Collector.
Proceedings of the From Reactive Systems to Cyber-Physical Systems, 2019

2018
Combining Model Checking and Deduction.
Proceedings of the Handbook of Model Checking., 2018

Alonzo Church Award 2018 - Call for Nominations.
Bull. EATCS, 2018

SOTER: Programming Safe Robotics System using Runtime Assurance.
CoRR, 2018

Duality-Based Nested Controller Synthesis from STL Specifications for Stochastic Linear Systems.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2018

Proofs in conflict-driven theory combination.
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017
Alonzo Church Award 2017 - Call for Nominations.
Bull. EATCS, 2017

Formalizing Hoare Logic in PVS.
Proceedings of the Engineering Trustworthy Software Systems - Third International School, 2017

TeLEx: Passive STL Learning Using Only Positive Examples.
Proceedings of the Runtime Verification - 17th International Conference, 2017

A Brief Introduction to the PVS2C Code Generator.
Proceedings of the Automated Formal Methods, 2017

Satisfiability Modulo Theories and Assignments.
Proceedings of the Automated Deduction - CADE 26, 2017

2016
ARSENAL: Automatic Requirements Specification Extraction from Natural Language.
Proceedings of the NASA Formal Methods - 8th International Symposium, 2016

Code Generation Using a Formal Model of Reference Counting.
Proceedings of the NASA Formal Methods - 8th International Symposium, 2016

Contract-Based Verification of Complex Time-Dependent Behaviors in Avionic Systems.
Proceedings of the NASA Formal Methods - 8th International Symposium, 2016

Double Helix and RAVEN: A System for Cyber Fault Tolerance and Recovery.
Proceedings of the 11th Annual Cyber and Information Security Research Conference, 2016

2015
Identifying Negative Cost Cycles in Strongly Polynomial Space.
Nord. J. Comput., 2015

Automated software winnowing.
Proceedings of the 30th Annual ACM Symposium on Applied Computing, 2015

Design and verification of multi-rate distributed systems.
Proceedings of the 13. ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2015

Design and verification for transportation system security.
Proceedings of the 52nd Annual Design Automation Conference, 2015

2014
Reverse Engineering Digital Circuits Using Structural and Functional Analyses.
IEEE Trans. Emerg. Top. Comput., 2014

Automatically Extracting Requirements Specifications from Natural Language.
CoRR, 2014

The Gradual Verifier.
Proceedings of the NASA Formal Methods - 6th International Symposium, NFM 2014, Houston, TX, USA, April 29, 2014

A framework for high-assurance quasi-synchronous systems.
Proceedings of the Twelfth ACM/IEEE International Conference on Formal Methods and Models for Codesign, 2014

Software engineering and automated deduction.
Proceedings of the on Future of Software Engineering, 2014

The Semantics of Datalog for the Evidential Tool Bus - (Extended Abstract).
Proceedings of the Specification, Algebra, and Software, 2014

2013
EFSMT: A Logical Framework for Cyber-Physical Systems.
CoRR, 2013

Tool Integration with the Evidential Tool Bus.
Proceedings of the Verification, 2013

WordRev: Finding word-level structures in a sea of bit-level gates.
Proceedings of the 2013 IEEE International Symposium on Hardware-Oriented Security and Trust, 2013

JBernstein: A Validity Checker for Generalized Polynomial Constraints.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Automated Reasoning, Fast and Slow.
Proceedings of the Automated Deduction - CADE-24, 2013

2012
ModelRob: A Simulink Library for Model-Based Development of robot manipulators.
Proceedings of the IEEE International Conference on Robotics and Automation, 2012

Automatic Dimensional Analysis of Cyber-Physical Systems.
Proceedings of the FM 2012: Formal Methods, 2012

The Architecture of Inference from SMT to ETB.
Proceedings of the 10th International Workshop on Satisfiability Modulo Theories, 2012

2011
A mechanical verification of the stressing algorithm for negative cost cycle detection in networks.
Sci. Comput. Program., 2011

SimCheck: a contract type system for Simulink.
Innov. Syst. Softw. Eng., 2011


Solving the First Verified Software Competition Problems Using PVS.
Proceedings of the Formal Modeling: Actors, Open Systems, Biological Systems, 2011

2010
The Mechanical Verification of a DPLL-Based Satisfiability Solver.
Proceedings of the Fifth Logical and Semantic Frameworks, with Applications Workshop, 2010

Rewriting, Inference, and Proof.
Proceedings of the Rewriting Logic and Its Applications - 8th International Workshop, 2010

SimCheck: An Expressive Type System for Simulink.
Proceedings of the Second NASA Formal Methods Symposium, 2010

Unraveling a Card Trick.
Proceedings of the Time for Verification, 2010

2009
Automated deduction for verification.
ACM Comput. Surv., 2009

The verified software initiative: A manifesto.
ACM Comput. Surv., 2009

System Support for Forensic Inference.
Proceedings of the Advances in Digital Forensics V, 2009

2008
A Brief Overview of PVS.
Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

Fixpoints and Search in PVS.
Proceedings of the Advanced Lectures on Software Engineering, 2008

Trust and Automation in Verification Tools.
Proceedings of the Automated Technology for Verification and Analysis, 2008

2007
A Tutorial on Satisfiability Modulo Theories.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007

2005
Inference Systems for Logical Algorithms.
Proceedings of the FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 2005

2004
Justifying Equality.
Proceedings of the Selected Papers from the Workshops on Disproving, 2004

SAL 2.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004

The ICS Decision Procedures for Embedded Deduction.
Proceedings of the Automated Reasoning - Second International Joint Conference, 2004

2003
Invisible formal methods for embedded control systems.
Proc. IEEE, 2003

2002
Verification by Abstraction.
Proceedings of the Formal Methods at the Crossroads. From Panacea to Foundational Support, 2002

Combining Shostak Theories.
Proceedings of the Rewriting Techniques and Applications, 13th International Conference, 2002

Little Engines of Proof.
Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 2002

Formal Verification of a Combination Decision Procedure.
Proceedings of the Automated Deduction, 2002

2001
Using Decision Procedures with a Higher-Order Logic.
Proceedings of the Theorem Proving in Higher Order Logics, 14th International Conference, 2001

A Technique for Invariant Generation.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2001

Static Analysis for Safe Destructive Updates in a Functional Language.
Proceedings of the Logic Based Program Synthesis and Transformation, 2001

Deconstructing Shostak.
Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

ICS: Integrated Canonizer and Solver.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001

2000
Combining Theorem Proving and Model Checking through Symbolic Analysis.
Proceedings of the CONCUR 2000, 2000

Symbolic Analysis of Transition Systems.
Proceedings of the Abstract State Machines, 2000

1999
Modular Verification of SRT Division.
Formal Methods Syst. Des., 1999

A case-study in component-based mechanical verification of fault-tolerant programs.
Proceedings of the 1999 ICDCS Workshop on Self-stabilizing Systems, 1999

Principles and Pragmatics of Subtyping in PVS.
Proceedings of the Recent Trends in Algebraic Development Techniques, 1999

Abstract and Model Check While You Prove.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999

1998
Subtypes for Specifications: Predicate Subtyping in PVS.
IEEE Trans. Software Eng., 1998

Verifying a self-stabilizing mutual exclusion algorithm.
Proceedings of the Programming Concepts and Methods, 1998

Fair Synchronous Transition Systems and Their Liveness Proofs.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 1998

PVS: An Experience Report.
Proceedings of the Applied Formal Methods, 1998

1997
Industrial Strength Formal Verification Techniques for Hardware Designs.
Proceedings of the 10th International Conference on VLSI Design (VLSI Design 1997), 1997

Integration in PVS: Tables, Types, and Model Checking.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1997

Lazy Compositional Verification.
Proceedings of the Compositionality: The Significant Difference, International Symposium, 1997

1996
Steps Toward Mechanizing Program Transformations Using PVS.
Sci. Comput. Program., 1996

Unifying Verification Paradigms.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 1996

PVS: Combining Specification, Proof Checking, and Model Checking.
Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996

Experiments in Theorem Proving and Model Checking for Protocol Verification.
Proceedings of the FME '96: Industrial Benefit and Advances in Formal Methods, 1996

PVS: Combining Specification, Proof Checking, and Model Checking.
Proceedings of the Computer Aided Verification, 8th International Conference, 1996

On Shostak's Decision Procedure for Combinations of Theories.
Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

1995
Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS.
IEEE Trans. Software Eng., 1995

Computer-Aided Computing.
Proceedings of the Mathematics of Program Construction, 1995

Decision Problems for Second-Order Linear Logic
Proceedings of the Proceedings, 1995

An Integration of Model Checking with Automated Proof Checking.
Proceedings of the Computer Aided Verification, 1995

1994
A Tutorial on Using PVS for Hardware Verification.
Proceedings of the Theorem Provers in Circuit Design, 1994

Effective Theorem Proving for Hardware Verification.
Proceedings of the Theorem Provers in Circuit Design, 1994

Proof Search in First-Order Linear Logic and Other Cut-Free Sequent Calculi
Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994

Using Proof Theory to Optimize Proof Search.
Proceedings of the ICLP 1994, 1994

Proof Search (Tutorial).
Proceedings of the ICLP 1994, 1994

Towards a Duration Calculus Proof Assistant in PVS.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems, 1994

Metamathematics, machines, and Gödels's proof.
Cambridge tracts in theoretical computer science 38, Cambridge University Press, ISBN: 978-0-521-42027-3, 1994

1993
Linearizing Intuitionistic Implication.
Ann. Pure Appl. Log., 1993

David A. McAllester, Ontic: A Knowledge Representation System for Mathematics.
Artif. Intell., 1993

Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned.
Proceedings of the FME '93: Industrial-Strength Formal Methods, 1993

Verification of Real-Time Systems Using PVS.
Proceedings of the Computer Aided Verification, 5th International Conference, 1993

1992
Decision Problems for Propositional Linear Logic.
Ann. Pure Appl. Log., 1992

Mechanical Verification of a Generalized Protocol for Byzantine Fault Tolerant Clock Synchronization.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 1992

Proof Search in the Intuitionistic Sequent Calculus.
Proceedings of the Automated Deduction, 1992

PVS: A Prototype Verification System.
Proceedings of the Automated Deduction, 1992

1991
From formal verification to silicon compilation.
Proceedings of the Compcon Spring '91, San Francisco, 1991

1988
A mechanical proof of the Church-Rosser theorem.
J. ACM, 1988

Efficient Parallel Circuits and Algorithms for Division.
Inf. Process. Lett., 1988

1985
Towards Mechanical Metamathematics.
J. Autom. Reason., 1985


  Loading...