Automated Reasoning for Software Engineering (F24AI1)
:
Theorem Proving
Aims and objectives:
The aim of this part of the module is to explore topics within automated
reasoning as applied to
software engineering and to promote understanding of the issues involved
in interactive theorem proving.
We discuss methods and tools for formally proving correctness of mathematical proofs and hardware or software
systems. Verifying a complex system must include verification of the mathematical background theory, therefore it requires the
development of formal mathematical models. We express the relevant properties that we want to prove using higher-order
logic.
We will explain the principles of higher-order logic, its relation to typed lambda calculus, and how an
interactive theorem prover for higher-order logic can be implemented. We will develop modeling and verification
skills by verifying many examples with state-of-the-art theorem provers.
Practical exercises will be done with PVS. PVS incorporates powerful automatic decision procedures.
Download slides
Lecture material:
-
Lecture 1: Model checking versus theorem proving [ ps
pdf ]
Lecture 2: Theorem proving: Basics [ ps
pdf ]
Lecture 3: Theorem proving: Bound and Free Variables, Substitution, Higher-Order Logic [ ps
pdf ]
Lecture 3: Sequent calculus and PVS commands
[ ps
pdf ]
Downolad a reference paper on sequent calculus by D. Miller
[ ps
pdf ]
For PVS commands follow the recommended link: PVS prover guide, Chapter 4!
Commands: FLATTEN, SPLIT, BDDSIMP
Lab: Thursday, Room EM 2.50.
Download overview lecture given at NASA for basic features of the language
of PVS!
PVS:
Basic Language (PostScript)
Lecture 3: Higher order types and lambda expressions
[ ps
pdf ]
Laboratory material: (follow the links for)
- handouts
- handout for Lectures 1,2,3 Week 1:
- handout for Lecture 1 Week 2:
- exercises
- PVS files: Now contains: simple theorems involving natural numbers and lists.
- solutions
Tool support:
- PVS is available under
Linux within the School, simply type cd (to change to your home
directory) and then pvs at
the prompt. Note: Add the following line to your ~/.pvs.lisp
file:
(setq *decision-procedures* (remove 'ics *decision-procedures*))
Create the file ~/.pvs.lisp if necessary.
- PVS
SURVIVAL GUIDE
Start by reading chapter 2
of the system guide and work your way through the proof as shown: the
files are available from the exercise subdirectory. A summary of common
problem is given in the PVSSurvival.html