Tutorial: Automated Formal Methods with PVS, SAL, and Yices

摘要

This full-day tutorial provides an introduction to automated formal methods using modern tools and methods. PVS is a comprehensive system for formal specification and analysis. It provides an attractive specification language based on higher order logic extended with dependent types and structural and predicate subtypes, and includes constructs for recursively defined abstract data types, recursive functions, inductive relations, and tabular specifications, as well as traditional logical formulas. Analysis capabilities include very strong typechecking (which can involve theorem proving), direct execution (at speeds within a factor of five of hand-crafted C), random testing, theorem proving, and symbolic model checking (with predicate abstraction). The PVS theorem prover provides powerful automation including rewriting and decision procedures for real and integer arithmetic, and is scriptable. Properties to be verified can be expressed as individual logical formulas, as CTL properties (for model checking), or as theory interpretations. The system is supported by massive built-in and user-provided libraries of specifications for mathematics and computer science.