Natarajan Shankar | Academic Influence

Natarajan Shankar's AcademicInfluence.com Rankings

Natarajan Shankar

Computer Science

#1717

World Rank

#1778

Historical Rank

Software Engineering

#288

World Rank

#294

Historical Rank

Database

#7256

World Rank

#7507

Historical Rank

computer-science Degrees

Download Badge

Computer Science

Natarajan Shankar's Degrees

PhD Computer Science Stanford University
Masters Computer Science Stanford University

Similar Degrees You Can Earn

Why Is Natarajan Shankar Influential?

(Suggest an Edit or Addition)

According to Wikipedia, Natarajan Shankar is a computer scientist working at SRI International in Menlo Park, California, where he leads the Symbolic Analysis Laboratory. Education Shankar received his Ph.D. degree in computer science, under advisors Robert S. Boyer and J Strother Moore, from the University of Texas at Austin in 1986.

(See a Problem?)

Natarajan Shankar's Published Works

Number of citations in a given year to any of this author's works

Total number of citations to an author for the works they published in a given year. This highlights publication of the most important work(s) by the author

Published Works

PVS: A Prototype Verification System (1992) (1784)
Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS (1995) (673)
PVS: Combining Specification, Proof Checking, and Model Checking (1996) (575)
Decision problems for propositional linear logic (1990) (317)
A Tutorial Introduction to PVS (1998) (294)
An Integration of Model Checking with Automated Proof Checking (1995) (250)
An Overview of SAL (2000) (219)
Abstract and Model Check While You Prove (1999) (218)
Experiments in Theorem Proving and Model Checking for Protocol Verification (1996) (193)
Subtypes for Specifications: Predicate Subtyping in PVS (1998) (175)
ICS: Integrated Canonizer and Solver (2001) (159)
The SAL Language Manual (2003) (133)
Reverse Engineering Digital Circuits Using Structural and Functional Analyses (2014) (109)
Towards a Duration Calculus Proof Assistant in PVS (1994) (96)
Deconstructing Shostak (2001) (95)
Effective Theorem Proving for Hardware Verification (1994) (92)
The 1st Verified Software Competition: Experience Report (2011) (92)
A Technique for Invariant Generation (2001) (87)
Verification of Real-Time Systems Using PVS (1993) (87)
PVS: An Experience Report (1998) (86)
A mechanical proof of the Church-Rosser theorem (1988) (86)
On Shostak's Decision Procedure for Combinations of Theories (1996) (84)
A Tutorial on Satisfiability Modulo Theories (2007) (83)
The PVS Specification Language (1993) (83)
Combining Theorem Proving and Model Checking through Symbolic Analysis (2000) (83)
The verified software initiative: A manifesto (2009) (83)
User guide for the pvs specification and verification system (beta release) (1991) (81)
WordRev: Finding word-level structures in a sea of bit-level gates (2013) (80)
Proof Search in the Intuitionistic Sequent Calculus (1992) (75)
Metamathematics, machines, and Gödels's proof (1994) (73)
ARSENAL: Automatic Requirements Specification Extraction from Natural Language (2014) (68)
Pvs: Combining Speciication, Proof Checking, and Model Checking ? 1 Combining Theorem Proving and Typechecking (1996) (66)
Combining Shostak Theories (2002) (65)
Mechanical Verification of a Generalized Protocol for Byzantine Fault Tolerant Clock Synchronization (1992) (63)
Proof search in first-order linear logic and other cut-free sequent calculi (1994) (59)
The ICS Decision Procedures for Embedded Deduction (2004) (59)
Modular Verification of SRT Division (1996) (58)
Tool Integration with the Evidential Tool Bus (2013) (54)
Invisible formal methods for embedded control systems (2003) (54)
A Tutorial on Using PVS for Hardware Verification (1994) (53)
Integration in PVS: Tables, Types, and Model Checking (1997) (47)
Evaluating, Testing, and Animating PVS Specications (2001) (46)
Sal 2 (2004) (45)
SOTER: A Runtime Assurance Framework for Programming Safe Robotics Systems (2018) (44)
Symbolic Analysis of Transition Systems (2000) (44)
Little engines of proof (2002) (38)
Using Decision Procedures with a Higher-Order Logic (2001) (37)
A Brief Overview of PVS (2008) (37)
Linearizing intuitionistic implication (1991) (37)
Principles and Pragmatics of Subtyping in PVS (1999) (36)
A case-study in component-based mechanical verification of fault-tolerant programs (1999) (35)
Automated deduction for verification (2009) (34)
Justifying Equality (2005) (33)
Lazy Compositional Verification (1997) (33)
Automated software winnowing (2015) (32)
Verifying a self-stabilizing mutual exclusion algorithm (1998) (31)
The Mechanical Verification of a DPLL-Based Satisfiability Solver (2011) (30)
EFSMT: A Logical Framework for Cyber-Physical Systems (2013) (30)
Static Analysis for Safe Destructive Updates in a Functional Language (2001) (29)
SimCheck: a contract type system for Simulink (2011) (29)
Automatically Extracting Requirements Specifications from Natural Language (2014) (29)
TeLEx: learning signal temporal logic from positive examples using tightness metric (2019) (27)
TeLEx: Passive STL Learning Using Only Positive Examples (2017) (27)
Design and verification for transportation system security (2015) (26)
A Tutorial on Specification and Verification Using PVS (1993) (26)
Fair Synchronous Transition Systems and Their Liveness Proofs (1998) (24)
Trust and Automation in Verification Tools (2008) (24)
Mechanical Verification of a Schematic Byzantine Clock Synchronization Algorithm (1991) (22)
Towards mechanical metamathematics (1985) (22)
Formal Verification of a Combination Decision Procedure (2002) (21)
SimCheck: An Expressive Type System for Simulink (2010) (21)
Efficient Parallel Circuits and Algorithms for Division (1988) (21)
The PVS Prelude Library (2003) (20)
Steps Toward Mechanizing Program Transformations Using PVS (1996) (19)
Satisfiability Modulo Theories and Assignments (2017) (19)
Double Helix and RAVEN: A System for Cyber Fault Tolerance and Recovery (2016) (19)
Machine-assisted verification using theorem proving and model checking (1997) (17)
The Gradual Verifier (2014) (17)
Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned (1993) (16)
Decision problems for second-order linear logic (1995) (15)
Counterexample-Driven Model Checking ? (2003) (13)
Unifying Verification Paradigms (1996) (13)
Combining Model Checking and Deduction (2018) (13)
A Mechanized Refinement Proof for a Garbage Collector (1997) (13)
Metamathematics, Machines, and Gödels's Proof: The Undecidable Sentence (1994) (12)
SOTER: Programming Safe Robotics System using Runtime Assurance (2018) (11)
Proofs in conflict-driven theory combination (2018) (11)
A framework for high-assurance quasi-synchronous systems (2014) (11)
Automatic Dimensional Analysis of Cyber-Physical Systems (2012) (11)
Model-Centered Assurance for Autonomous Systems (2020) (11)
Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness (2019) (11)
Design and verification of multi-rate distributed systems (2015) (11)
Inference Systems for Logical Algorithms (2005) (11)
Proceedings of the Third international joint conference on Automated Reasoning (2006) (10)
Automated Reasoning: Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings (2006) (10)
Automatic Requirements Specification Extraction from Natural Language (ARSENAL) (2014) (10)
A Semantic Embedding of theA g Dynamic Logic in PVS (2003) (10)
Proof-checking metamathematics (theorem-proving) (1986) (9)
Computer-Aided Computing (1995) (9)
Machine Reading Using Markov Logic Networks for Collective Probabilistic Inference (2011) (9)
Integrating Verification Components ⋆ (2005) (8)
JBernstein: A Validity Checker for Generalized Polynomial Constraints (2013) (8)
Research Report: The Parsley Data Format Definition Language (2020) (7)
Automated verification using deduction, exploration, and abstraction (2003) (7)
Automated Reasoning: Thrid International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings (Lecture Notes in Computer Science) (2007) (7)
Accountable clouds (2013) (7)
Code Generation Using a Formal Model of Reference Counting (2016) (7)
A verified packrat parser interpreter for parsing expression grammars (2020) (7)
Software engineering and automated deduction (2014) (7)
Verification by Abstraction (2002) (6)
The Semantics of Datalog for the Evidential Tool Bus - (Extended Abstract) (2014) (6)
A Brief Introduction to the PVS2C Code Generator (2018) (5)
A Tutorial on Using Pvs for Hardware Veriication ? Pvs Stands for \prototype Veriication System." It Consists of a Speciication Language Integrated with Support Tools and a Theorem Prover. Pvs Tries to Pro- ? (1995) (5)
Duality-Based Nested Controller Synthesis from STL Specifications for Stochastic Linear Systems (2018) (4)
Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs (2021) (4)
A Tool Bus for Anytime Verification ? (2010) (4)
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (2016) (3)
Integration of formal verification with real-time design (1996) (3)
Embedded Deduction With ICS (2003) (3)
A model-constructing framework for theory combination (2016) (3)
A Logical Basis for Functional Programming (extended Abstract) (3)
Metamathematics, Machines, and Gödels's Proof: Preface (1994) (3)
System Support for Forensic Inference (2009) (3)
From formal verification to silicon compilation (1991) (3)
The 1st Verified Software Competition, Extended Experience Report (2011) (3)
Sherlock : A Tool for Verification of Deep Neural Networks (2019) (2)
The First Fifteen Years of the Verified Software Project (2021) (2)
Contract-Based Verification of Complex Time-Dependent Behaviors in Avionic Systems (2016) (2)
Rewriting, Inference, and Proof (2010) (2)
Integrating Verification Components : The Interface is the Message ? (2004) (2)
Industrial strength formal verification techniques for hardware designs (1997) (2)
Prin iples and Pragmati s of Subtyping in PVS ? (1999) (2)
AFM ’ 08 : Third Workshop on Automated Formal Methods 14 July 2008 Princeton , New Jersey (2008) (1)
Are formal methods useful for software development? (1992) (1)
Requirements-Driven Model Checking and Test Generation for Comprehensive Verification (2022) (1)
Unraveling a Card Trick (2010) (1)
Unifying Verification Paradigms (Extended Abstract)* (1996) (1)
Automated Reasoning, Fast and Slow (2013) (1)
DesCert: Design for Certification (2022) (1)
EFSMT: A Logical Framework for the Design of Cyber-Physical Systems (2014) (1)
Fixpoints and Search in PVS (2008) (1)
Recent Trends in Algebraic Development Techniques (1999) (1)
Chapter 23 SYSTEM SUPPORT FOR FORENSIC INFERENCE (2009) (0)
The Correctness of a Code Generator for a Functional Language (2020) (0)
Beyond Satisfiability: Extensions and Applications (2007) (0)
PVS Theorem Proving Enhancements. (1997) (0)
Using Proof Theory to Optimize Proof Search (1994) (0)
Theorem Proving for HardwareVeri cation ? ? ? (1994) (0)
Machine-Assisted Veri cationUsing Theorem Provingand Model (1997) (0)
Little Engines of Proof : Lecture 1 (0)
A Brief Introduction to the PVS 2 C Code Generator ∗ (2018) (0)
Metamathematics, Machines, and Gödels's Proof: A Mechanical Proof of the Church–Rosser Theorem (1994) (0)
Mechanical proofs of fault-tolerant clock synchronization (1990) (0)
Derived Inference Rules (1994) (0)
Enhan ing PVS to Support Evaluating , Testing , and Animating PVS Spe i (2007) (0)
Decision Problems for Propositional Linear (2009) (0)
Integrating LTL Model Checking with Automated Theorem Proving ( Category A ) (0)
Revisiting Variable Ordering for Real Quantifier Elimination using Machine Learning (2023) (0)
Can we rely on Formal Methods (1995) (0)
Metamathematics, Machines, and Gödels's Proof: The Statement of the Incompleteness Theorem (1994) (0)
Proceedings of the 2nd international conference on Verified Software: Theories, Tools, Experiments (2008) (0)
2018 CAV award (2021) (0)
A Tutorial on Satisfiability Modulo Theories (Invited Tutorial) (2007) (0)
Identifying Negative Cost Cycles in Strongly Polynomial Space (2015) (0)
Figure 3: Microprocessor Speciication Bolic Model Checking for Sequential Circuit Veriication. Ieee Transactions on 5 Conclusions and Future Work 4.2 Abstracting the Microprocessor Design 4.1 Proving the Lemmas Using Model-checking (0)
Model Checking and Deduction ( DRAFT ) ? (2014) (0)
TeLEx: learning signal temporal logic from positive examples using tightness metric (2019) (0)
David A. McAllester, Ontic: A Knowledge Representation System for Mathematics (1993) (0)
BERGER, U., Total sets and objects in domain theory DOWNEY, R., Every recursive boolean algebra is isomorphic to one with incomplete atoms GONCHAREV, S., YAKHNIS, A. and YAKHNIS, V., Some effectively infinite classes of enumerations (1993) (0)
Solving the First Verified Software Competition Problems Using PVS (2011) (0)
A mechanical verification of the stressing algorithm for negative cost cycle detection in networks (2011) (0)
[12] Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Some lessons learned. In J. C. P. Woodcock and P. G. Larsen, editors, (1993) (0)
Metamathematics, Machines, and Gödels's Proof: Conclusions (1994) (0)
CDSAT for Nondisjoint Theories with Shared Predicates: Arrays With Abstract Length (2022) (0)
Performance verification of audio converter integrated circuits (1998) (0)
The Verified Software Initiative: A Manifesto (2021) (0)
Conflict-Driven Satisfiability for Theory Combination: Transition System and Completeness (2019) (0)
A Refinement Proof for a Garbage Collector (2019) (0)
Formalizing Hoare Logic in PVS (2017) (0)
Capturing the iccMAX calculatorElement: A Case Study on Format Design (2022) (0)
Deconstructing S hostak (2001) (0)
Using Model Checking and Simula- Tion to Detect a Safety Violation in a Control System Speciication. Submitted for Publication (1998) (0)
Conflict-Driven Satisfiability for Theory Combination: Lemmas, Modules, and Proofs (2021) (0)
Proceedings of the second workshop on Automated formal methods (2007) (0)
The situation has provided a cue; this cue has given the expert access to information stored in memory, and the information provides the answer. Intuition is nothing more and nothing less than recognition. (2013) (0)
CoProver: A Recommender System for Proof Construction (2023) (0)
Acknowledgments: Pvs Was Constructed by Our Colleagues Sam Owre and 3.1 Informal Proof: Sketch Omh(0) (2007) (0)
Evidential Transactions with Cyberlogic (2023) (0)
The Architecture of Inference from SMT to ETB (2013) (0)
Proof Search (Tutorial) (1994) (0)
Review: Larry Wos, Ross Overbeek, Ewing Lusk, Jim Boyle, Automated Reasoning. Introduction and Applications (1994) (0)
2018 CAV award (2021) (0)
Metamathematics, Machines, and Gödels's Proof: The Representability of the Metatheory (1994) (0)
Automated Formal Methods (AFM09) (2009) (0)

This paper list is powered by the following services:

Other Resources About Natarajan Shankar

en.wikipedia.org

What Schools Are Affiliated With Natarajan Shankar?

Natarajan Shankar is affiliated with the following schools: