Abstraction Engineering with the Prototype Verification System (PVS) - Introduction to Interactive Theorem Proving

Learn about the Prototype Verification System (PVS) in this comprehensive colloquium talk that explores the intersection of logic and computing. Discover how PVS, released 30 years ago by SRI, aims to democratize interactive theorem proving through its combination of expressive formalism and automated reasoning tools. Explore key features including expressive-order logic, algebraic/coalgebraic datatypes, dependent predicate subtypes, and parametric theories. Gain insights into the system's interactive theorem prover, which utilizes automated proof strategies for simplification, rewriting, and case analysis, alongside built-in decision procedures for SAT and SMT solving. Understand how PVS functions as a functional programming language with code generation capabilities in Common Lisp and C. Examine extensive libraries covering various mathematical and computing topics through this informal overview of PVS's theoretical foundations, proof capabilities, and code generation features. Presented by Dr. Natarajan Shankar, a Distinguished Senior Scientist and SRI Fellow, who brings decades of expertise in computer science and is a co-developer of numerous technologies including PVS, SAL model checker, and Yices SMT solver.