Natarajan Shankar's Recent Talks
Transparencies for recent talks by
Natarajan Shankar.
 An Architecture for Inference, Logosphere/Little Engines of
Proof Workshop, CMU, Pittsburgh, January 28/29, 2006.
(
.pdf )
 Inference Systems for Logical Algorithms, Invited talk at
FSTTCS'05, Hyderabad, India, December 16, 2005.
(
.pdf )
 Explaining Decision Procedures, Invited talk at the Calculemus'05, Newcastle,
England on July 18, 2005
(
.pdf )
 Modularity in Inference Systems, Invited talk at the PDPAR'05, Edinburgh,
Scotland on July 12, 2005
(
.ps.gz )
 The Challenge of Software Verification, Invited talk at the HCSS'05
(
.pdf )
 The Interface is the Message at the Monterey Workshop, Baden,
Vienna on Oct 6, 2004 (
.ps.gz )
( .ps
)(
.pdf
)
 Little Engines of Proof at University of Utah, Salt Lake City
on Mar 1, 2004 (
.ps
)(
.pdf
)
 Introducing Cyberlogic High Confidence Software and Systems,
Baltimore, Maryland, April 2003
(
.pdf
)
 Computer Aided Verification (Lectures
at
EEF School on Specification, Verification, and Refinement, Turku,
Finland, Aug 19  30, 2002)
(
4up gzipped postscript
)(
gzipped postscript
)(
4up postscript
) (
postscript
)(
PDF
)(
4up PDF
)
 Little Engines of Proof: Invited Talk at FLoC 2002, Copenhagen.
(
.ps.gz)
(
.ps)
(
4up.ps)
(
4up.ps.gz)
(
.pdf)
(
4up.pdf)
 Little Engines of Proof: Invited Talk at ASL 2002, Las Vegas.
(
.ps.gz)
(
.ps)
(
.pdf)
 Verification by Abstraction: UNU/IIST 10th Anniversary
Colloquium, Lisbon, Portugal, Mar 1821, 2002.
( 4up
ps.gz)
(
4up ps)
(
ps.gz)
(
ps)
(
4up pdf)
(
pdf)
 Deconstructing Shostak: CMU seminar January 2002.
( 4up .ps)
( .ps)
( 4up
.pdf)
( .pdf)
 Mechanized Verification Methodologies Using PVS (Lectures
at WG2.3 School, TRDDC Pune, India, Jan. 310, 2002)
Revised from the CISM notes below.
(
4up gzipped postscript
)(
gzipped postscript
)(
4up postscript
) (
postscript
)(
PDF
)(
4up PDF
)
 Generating Efficient Code from Logic (Invited talk at LOPSTR 2001,
Cyprus)
( 4up PS
)
( 4up PDF
)
 What is a Garbage Collector? (WG2.3 Meeting 39 at Hanover)
( 4up PS
)
( 4up PDF
)
 Mechanized Verification Methodologies Using PVS (Tutorial to be given
at CISM, Udine, Sept. 2428, 2001)
(
4up gzipped postscript
)(
gzipped postscript
)(
4up postscript
) (
postscript
)(
PDF
)(
4up PDF
)
 Using Decision Procedures With a Higher Order Logic (TPHOLS 2001)
(
4up gzipped postscript
)(
gzipped postscript
)(
4up postscript
) (
postscript
)

Deconstructing Shostak (LICS 2001)

Combining Theorem Proving and Model Checking Through Symbolic
Analysis (Invited talk at CONCUR 2000)

Goedel's First Incompleteness Theorem: A Mechanical Verification
(Compressed 4up; Talks given at the Stanford Logic Seminar, November
1999)

Principles and Pragmatics of Subtyping in PVS
(Compressed 4up; Talks given at the WADT'99, September,
1999)

Efficient Code Generation and Evaluation from PVS
(Compressed 4up)

Verifying a SelfStabilizing Mutual Exclusion Algorithm (PROCOMET '98)
(Compressed 4up)

Lazy Compositional Verification (Compressed 4up)

An Overview of Deductive Verification Technology .
(
Compressed 4up)

The Use of Decision Procedures in Deductive Verification .
(
Compressed 2up)

Modular Verification of SRT Division

The Mechanics of Proof Search in Linear Logic

The Integration of Model Checking with Theorem Proving in PVS
 An
Integration of Model Checking and Proof Checking

Language and Induction

Byzantine Agreement

PVS Overview