Program Semantics, Verification, and Construction
(Previous instance: 2008/2009)
2010/2011
Course leader: Jorge Sousa Pinto (jsp(AT)di(DOT)uminho(DOT)pt )
Lecture 1
Introduction to the mathematics of program construction
Date: 27/09/10 (Monday, 10h13h). Room: DI A.1, Lecturer: J.N. Oliveira
Topics:
Overview of the scientific method applied to software design. Correct by verification versus correct by construction. Calculate versus invent & verify. The e=m+c equation: description versus calculation. Pointfree (PF) and pointwise (PW) notations. PFtransform for (algebraic) reasoning.
Analogy with the Laplace transform (historical perspective).
Binary relations as a building block for logic in computer science.
Introduction to the binary relation calculus.
Notes:
 Theory and applications of the PFtransform Lectures 12 (0156) (slides of the LerNET doctoral school at Piriapolis, Uruguay, 2008)
 Full tutorial paper: (LNCS)
Papers:
Lecture 2
PFtransform: when everything becomes a relation
Date:
04/10/10 (Monday, 10h13h). Room: DI A.1, Lecturer: J.N. Oliveira
Topics:
Taxonomy of binary relations. Functions.
Conditions and coreflexives. PFtransform of nary relations. Union and meet. Universal
constructions and properties. Galois connections underpinning relation algebra.
Extended static checking(ESC) in the PFstyle.
Notes:
Lecture 3
PFtransform: extended static checking by calculation
Date:
11/10/10 (Monday, 10h13h). Room: DI A.1, Lecturer: J.N. Oliveira
Topics:
Verification conditions in the PFstyle. Arrow notation. Relation to Hoare triples and Hoare logic. Handling nondeterminism. Calculus of proof obligations (proof rules). Case study: verifying a model of a journaled file system. Manual proofs in conjunction with model checking in Alloy. Open issues and research topics.
Notes:
 Hands on a Grand Challenge in Computing: Proving a Journaled File System Correct (PDF)
Lecture 4
Module assessment: paper recitation
Date:
18/10/10 (Monday, 10h13h). Room: DI A.1, Lecturer: J.N. Oliveira
Topics: Provisional schedule as follows:
 10h00  Carlos Eduardo Bastos e Marques da Silva: Variations on a AlloyCentric Toolchain in Verifying a Journaled File System Model
 10h18  Constantin Taivan: Reverse Program Calculation Supported by Code Slicing
 10h36  Frederico Miguel Goulão Valente: Generic Pointfree Lenses
 10h54  Henrique Manuel Fernandes de Castro: A Relational Model for Confined Separation Logic
 11h12 Coffee break
 11h30  Nuno Filipe Moreira Macedo: First steps in Pointfree Functional Dependency Theory
 11h48  Nuno Miguel Almeida Luz: Strategic Term Rewriting and its Application to a VDM to SQL Convertion
 12h06  Paulo José Correia Bernardes: On the design of a Periodic Table of VDM specifications
 12h24  Eduardo Augusto Peixoto da Silva Brito: Tupling Calculation Eliminates Multiple Data Traversals
 12h42  Pedro Miguel Ribeiro Martins: Proving correctness using Free Theorems
 13h00 Closing
Material:
Zip file containing all papers and presentations (11MB)
Lecture 5
A revision of propositional and ﬁrstorder logics
Date:
25/10/10 (Monday, 10h13h). Room: DI A.1, Lecturer: Luís Pinto
Topics:
 Propositional Logic (PL): Syntax; Semantics; Proof system; Adequacy of the proof system
 FirstOrder Logic (FOL): Syntax; Semantics; Proof system; Theory for equality
 Intuitionistic Logic: Natural deduction systems (propositional and firstorder)
Notes:
 A revision of propositional and ﬁrstorder logics (PDF)
Lecture 6
Validity Checking in Propositional and ForstOrder Logic
Date:
08/11/10 (Monday, 10h13h). Room: DI A.1, Lecturer: José Bacelar Almeida
Topics:
 Propositional Logic: general remarks; normal forms (NNF, CNF, DNF); validity/satisfiability in CNFs.
 FirstOrder Logic: general remarks; normal forms (NNF, prenex, Herbrand/Skolem); Herbrand's theorem; semidecidability; decidable fragments.
 FirstOrder Theories: basic concepts; some theories of interest; SMT provers.
Notes:
 Validity Checking in Propositional and FirstOrder Logic (PDF)
Bibliography:
Any standard textbook on Mathematical Logic addresses most of the topics mentioned in the Lecture (e.g. [11] from the list of recommended books).
A nice survey on the subject is
 Natarajan Shankar. Automated deduction for verification. ACM Computer Surveys, 41(4):1–56, 2009.
A more specialised list on the topic of decision procedures for specific theories:
 Daniel Kroening and Ofer Strichman. Decision Procedures: An Algorithmic Point of View. Springer Verlag, 2008.
 Aaron R. Bradley and Zohar Manna. Calculus of Computation: Decision Procedures with Applications to Verification. Springer Verlag, 2007.
Lecture 7
The λcalculus and the CurryHoward correspondence
Date:
15/11/10 (Monday, 10h13h). Room: DI A.1, Lecturer: José Espírito Santo
Topics:
 Proof Theory: Natural Deduction; Normalisation; Other proof systems
 The λcalculus: the untyped λcalculus; the simplytyped λcalculus
 The CurryHoward correspondence, variants, and uses
Notes:
 The λcalculus and the CurryHoward correspondence (PDF)
Bibliography:
 See references on the notes
Lecture 8
Type Systems and Logics
Date:
22/11/10 (Monday, 10h13h). Room: DI A.1, Lecturer: Maria João Frade
Topics:
 Proof assistants based on type theory
 Pure Type Systems
 The Lambda Cube
 The Logic Cube
Notes:
Bibliography:
 Henk Barendregt. Lambda calculi with types. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 117–309. Oxford Science Publications, 1992.
 Henk Barendregt and Herman Geuvers. Proofassistants using dependent type systems. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, pages 1149–1238. Elsevier and MIT Press, 2001.
 Gilles Barthe and Thierry Coquand. An introduction to dependent type theory. In Gilles Barthe, Peter Dybjer, Luís Pinto, and João Saraiva, editors, APPSEM, volume 2395 of Lecture Notes in Computer Science, pages 1–41. Springer, 2000.
Lecture 9
A Practical Approach to the Coq ProofAssistant
Date:
29/11/10 (Monday, 10h13h). Room: DI A.1, Lecturer: José Bacelar Almeida
Topics:
 Gallina language (Coq specification language)
 Interactive proof development environment
 Case study: correctness of sorting algorithms
Notes:
 The Coq ProofAssistant (PDF)
Bibliography:
Lecture 10
An Introduction to the FramaC tool for the Analysis of C code
Date:
6/12/10 (Monday, 10h13h). Room: DI A.1, Lecturer: Jorge Sousa Pinto
Topics:
 Overview of formal code analysis and verification techniques: static analysis; abstract interpretation; software model checking; deductive verification
 Introduction to FramaC and its plugins
 The Jessie tool: verification of safety properties of C code. The GWhy GUI and the multiprover facilities
 The ACSL specification language. Verification of functional properties with Jessie.
Notes:
 Safety veriication with FramaC (PDF)
 Functional Verification with FramaC (PDF)
Bibliography:
 Loc Correnson, Pascal Cuoq, Armand Puccetti, and Julien Signoles. FramaC user manual. from the FramaC website, http://framac.com, 2010.
 Patrick Baudin, JeanChristophe Fillitre, Claude March, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Speciﬁcation Language. Preliminary Design (version 1.4). from the FramaC website, http://framac.com, 2010.
 Yannick Moy and Claude March´e. Jessie Plugin Tutorial. LRI, February 2010. Beryllium Version.
 Created by : JoseNunoOliveira  24 Sep 2010


Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.

