Author: Natarajan Shankar

  • 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 design space exploration of both in-vehicle electronic control systems and vehicle-to-vehicle communications.

  • 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 Datalog used in ETB and describe an abstract machine for evaluating Datalog queries.

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

  • 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 as register files, counters, adders, and subtractors.

  • 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 to audit and retain in a privacy-preserving and nonrepudiable fashion.

  • JBernstein: A Validity Checker for Generalized Polynomial Constraints

    Despite substantial advances in verification technology, complexity issues with classical decision procedures for nonlinear real arithmetic are still a major obstacle for formal verification of real-world applications.

  • WordRev: Finding Word-Level Structures in a Sea of Bit-Level Gates

    In this paper, we present a systemic way of automatically deriving word-level structures from the gate-level netlist of a digital circuit. We demonstrate the effectiveness of our approach on a system-on-a-chip (SoC) design consisting of approximately 400,000 IBM 12SOI cells and several open-source designs.

  • Declaratively Processing Provenance Metadata

    We propose a simple declarative language for processing provenance metadata and evaluate it by translating filters implemented in SPADE [9], an open-source provenance collection platform.