Solo testo/Text only

Formal verification of computer systems by theorem proving

Dr. Holger Pfeifer
Faculty of Engineering and Computer Sciences, Institute of Artificial Intelligence, University of Ulm, Germany

16 hours, 4 credits (final test)

March 27 - March 30, 2007
Dipartimento di Ingegneria dell'Informazione: Elettronica, Informatica, Telecomunicazioni, via Diotisalvi 2, meeting room

Contacts: Prof. Cinzia Bernardeschi

Aims

Introduction to Theorem Proving

Theorem proving is a technique to verify properties of systems by deriving them as theorems from a system model by means of logical deduction. Given a sufficiently expressive logic, theorem proving can in principle be applied to any type of verification problem. An important application area of theorem proving is the analysis of critical aspects of fault-tolerant real-time systems.

This series of lectures provides an introduction to the area of theorem proving by presenting basic logical formalisms and their respective proof methods. The selection of course topics is tailored towards what is needed to understand the principle aspects of PVS, a state-of-the-art automated theorem proving system.

Upon completion, course participants will have a basic understanding of propositional, first-order, and higher-order logics and selected proof methods, and will be able to perform automated deductions of simple theorems in the PVS system.

Syllabus

• Introduction:
  History, facets of theorem proving, application areas.
• Fundamental concepts and notions of logic:
  Syntax, semantics, model, consequence, proof calculus, etc.
• Propositional logic:
  Syntax and semantics, axiomatization, proof methods.
• First-order logic:
  Syntax and semantics, many-sorted FOL, proof methods.
• Sequent calculus:
  Inference rules for propositional logic and FOL, derivations.
• Lambda calculus and higher-order logic:
  Syntax, reduction rules, simply-typed lambda calculus, higher-order logics: motivation, semantics, properties.
• Inductive structures and induction:
  Peano arithmetic and mathematical induction, inductive datatypes and structural induction, recursive functions.
• Automated theorem proving using PVS:
  Introduction to PVS, simple proofs of propositional and FOL theorems, abstract datatypes and proofs by induction.