Natarajan Shankar's Recent Papers

• NFM'10: SimCheck: An Expressive Type System for Simulink ( .pdf)
• WRLA'10: Rewriting, Inference, and Proof ( .pdf)
• HCSS03: Introducing Cyberlogic (with H. Ruess) ( .ps.gz) ( .ps) ( .pdf)
• FLoC'02/FME'02 (invited): Little Engines of Proof ( .ps.gz ) ( .ps) ( .pdf)
• FLoC'02/RTA'02 (invited): Combining Shostak Theories (with H. Ruess) ( .ps.gz ) ( .ps) ( .pdf)
  [Note: The paper that appears in the RTA'02 proceedings contains some minor errors that have been corrected here.]
• CADE'02: Formal Verification of a Combination Decision Procedure (with J. Ford) ( .ps.gz ) ( .ps) ( .pdf)
• LOPSTR'01 (invited): Static Analysis for Safe Destructive Updates in a Functional Language ( .ps.gz ) ( .ps) ( .pdf)
• TPHOLS01 (invited): Using Decision Procedures With a Higher-Order Logic
• LICS01: Deconstructing Shostak (with H. Ruess)
  
• TACAS'01: A Technique for Invariant Generation (with A. Tiwari, H. Ruess, and H. Saidi)
  
• CONCUR'00 (invited): Combining Theorem Proving and Model Checking through Symbolic Analysis
  
• ASM'00 (invited): Symbolic Analysis of Transition Systems
  
• WADT'99 (invited): Principles and Pragmatics of Subtyping in PVS
  
• LFM'00: An Overview of SAL
  
• CAV'99: Abstract and Model Check While you Prove (with H. Saidi)
  
• CDCS'99: A Case-Study in Component-Based Mechanical Verification of Fault-Tolerant Programs (with S. Kulkarni, J.M. Rushby)
  
• FMSD99: Modular Verification of SRT Division (with H. Ruess, M. Srivas)
  
• FM-Trends'98: PVS: An Experience Report
  
• TSE'98: Subtypes for Specifications: Predicate Subtypes in PVS
  
• FTRTFT'98: Fair Synchronous Transition Systems and their Liveness Proofs
  
• COMPOS'97: Lazy Compositional Verification
  
• PROCOMET'98: Verifying a Self-Stabilizing Mutual Exclusion Algorithm
  
• TACAS'97: Integration in PVS: Tables, Types, and Model Checking
  
• Machine-Assisted Verification Using Theorem Proving and Model Checking
  
• FTRTFT96 (invited): Unifying Verification Paradigms
  
• FMCAD96 (tutorial): PVS: Combining Specification, Proof Checking, and Model Checking
  
• CAV96 (system description): PVS: Combining Specification, Proof Checking, and Model Checking
  
• CAV96: Modular Verification of SRT Division
  
• CADE96: On Shostak's Decision Procedure for Combinations of Theories
  
• Mechanizing Program Transformation Using PVS
  
• FME96: Experiments in Theorem Proving and Model Checking for Protocol Verification
  
• MPC95 (invited): Computer-Aided Computing
  
• CAV95: An Integration of Model Checking and Automated Proof Checking
  
• TSE95: Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS
  
• LICS95: Decision Problems for Second-Order Linear Logic
  
• TPCD94: Effective Theorem Proving for Hardware Verification
  
• LICS94: Proof Search in Cut-free Sequent Calculi ( .ps )( .pdf )
  
• CAV93: Mechanical Verification of Real-time Systems Using PVS
  
• CADE92: PVS: Prototype Verification System
  
• FME93: Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned
  
• FTRTFT92: Mechanical Verification of a Generalized Protocol for Byzantine Fault Tolerant Clock Synchronization
  
• CADE92: Proof Search in Intuitionistic Sequent Calculus
  
• LICS91: Linearizing Intuitionistic Implication
  
• Decision Problems in Linear Logic
  
• FOCS90: Decision Problems in Linear Logic (short form)