Natarajan Shankar's Recent Papers
The following is a partial list of papers (co)authored by
Natarajan Shankar.
 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 HigherOrder 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 CaseStudy in ComponentBased Mechanical Verification of FaultTolerant
Programs (with S. Kulkarni, J.M. Rushby)

FMSD99: Modular Verification of SRT Division (with H. Ruess, M. Srivas)

FMTrends'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 SelfStabilizing Mutual Exclusion Algorithm

TACAS'97: Integration in PVS: Tables, Types, and Model Checking

MachineAssisted 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): ComputerAided Computing
 CAV95: An
Integration of Model Checking and Automated Proof Checking
 TSE95: Formal Verification for FaultTolerant Architectures: Prolegomena to the
Design of PVS

LICS95: Decision Problems for SecondOrder Linear Logic

TPCD94: Effective Theorem Proving for Hardware Verification
 LICS94: Proof Search in Cutfree Sequent Calculi ( .ps.gz )( .ps )( .pdf )
 CAV93: Mechanical Verification of Realtime Systems Using PVS
 CADE92: PVS: Prototype Verification System
 FME93: Formal Verification for FaultTolerant Architectures: Some Lessons Learned
 FTRTFT92: Mechanical Verification of a Generalized Protocol for Byzantine Fault Tolerant Clock Synchronization
 CADE92: Proof Search in Intuitionistic Sequent Calculus ( .ps.gz)( .ps)( .pdf)
 Decision
Problems in Linear Logic
 LICS91: Linearizing
Intuitionistic Implication
 FOCS90: Decision Problems in Linear Logic (short form)