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.

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

The PVS web page.

There are three documents that you need: the system guide, the prover guide and language reference. There are also Postscript versions of these documents for convenient printing.

PVS stores specifications in .pvs files, which it locates in its working context. The context defaults to the directory in which pvs was executed. In Emacs, M- refers to the "meta" key, which is usually Esc, but sometimes Alt. So M-x may mean press "Esc" then "x". If your context isn't the work directory your created earlier, type M-x change-context to change it. (Note that Emacs has tab completion.) Save files with extension .pvs in your work directory.

To cycle through the previous commands in the PVS buffer, type M-P. To display your current proof in a tree diagram, type M-x x-show-current-proof. PVS uses common Emacs commands for text editing, like C-x C-s to save, C-x C-c to exit the program, and C-g to exit a prompt. If you cannot remember a particular key binding, you can always use the toolbar.

If PVS takes a long time on a command, you can interrupt it with C-c C-c. This will dump you to a prompt for Lisp. Type (restore) to get back to your previous sequent. You can also reset PVS when your cursor is in the *pvs* buffer with M-x reset-pvs.

You can step through a proof using either the M-x step-proof or the M-x x-step-proof commands. The command TAB 1 executes one proof step. The command ESC n TAB 1 executes n proof steps. Repositioning the cursor in the Proofwindow affects which step will be executed next. Therefore, use C-x o to switch between bufferes rather than using mouse clicks.

From within the prover, you issue commands like (split), (flatten), and (grind). To quit the prover, issue the (quit) command. Remember that all prover commands are in parentheses.

Lecture material:

Lecture 1: Model checking versus theorem proving [ ps pdf ]

Lecture 2: Theorem proving: Basics [ ps pdf ]

Lecture 3: PVS: Basic Language [ ps pdf ]

Lecture 4: PVS and Sequent Calculi [ ps pdf ]

Lecture 5: PVS Commands [ PowerPoint ]

Lecture 6: Induction [ ps ]

Lecture 7: Induction in PVS: Examples [ ps ]

Laboratory material:

Follow the link for handouts for Lab Exercises, PVS files.

Assignment: Due by December, 7th, 2007

[ pvs]

Assignment grades