Natarajan Shankar's Recent Talks

• 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 18-21, 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. 3-10, 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. 24-28, 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 Self-Stabilizing 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