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 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)