Natarajan Shankar

Staff Scientist, Computer Science Laboratory

Natarajan Shankar, Ph.D., is a staff scientist in the Computer Science Laboratory at SRI International. He performs research and is published across a wide spectrum ranging from fundamental mathematics to system software building. He is responsible for the creation of the highly influential Prototype Verification System (PVS), a benchmark system for the development of proofs and the verification of algorithms against which other systems are compared. Shankar’s current research ranges from foundational aspects of logic and programming to practical applications in software development, as well as system certification.

He is also very active in the software technology community and has hosted dozens of students, professors, and technology leaders from around the world. Shankar is considered one of the leading scientists in his field, and has played a central role in several international research initiatives. 

Shankar was named an SRI Fellow in 2009.

Recent publications

read More

  • Design and Verification for Transportation System Security

    In this work, we propose an integrated framework that combines hybrid modeling, formal verification, and automated synthesis techniques for analyzing the security and safety of transportation systems and carrying out…

  • A Framework for High-Assurance Quasi-Synchronous Systems

    In this paper, we examine the foundations of a quasi-synchronous model of computation Our version of the quasi-synchronous model is inspired by the Robot Operating System (ROS).

  • The Semantics of Datalog for the Evidential Tool Bus

    The Evidential Tool Bus (ETB) is a distributed framework for tool integration for the purpose of building and maintaining assurance cases. We outline the semantic characteristics of the variant of…

  • The Gradual Verifier

    We propose a gradual verification approach, GraVy. For a given piece of Java code, GraVy partitions the statements into those that are unreachable, or from which exceptional termination is impossible, inevitable, or…

  • Reverse Engineering Digital Circuits Using Structural and Functional Analyses

    In this paper, we present a set of algorithms for the reverse engineering of digital circuits starting from an unstructured netlist and resulting in a high-level netlist with components such…

  • Accountable Clouds

    To address current limitations, we propose a suite of mechanisms that enhances cloud computing technologies with more assurance capabilities. Assurance becomes a measurable property, quantified by the volume of evidence…