MAP/i - Foundations of Computing

Option I: Program Semantics, Verification, and Construction

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, 10h-13h). 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. Point-free (PF) and point-wise (PW) notations. PF-transform 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 PF-transform Lectures 1-2 (01-56) (slides of the Ler-NET doctoral school at Piriapolis, Uruguay, 2008)
  • Full tutorial paper: (LNCS)

Papers:

Lecture 2

PF-transform: when everything becomes a relation

Date:

04/10/10 (Monday, 10h-13h). Room: DI A.1, Lecturer: J.N. Oliveira

Topics:

Taxonomy of binary relations. Functions. Conditions and coreflexives. PF-transform of n-ary relations. Union and meet. Universal constructions and properties. Galois connections underpinning relation algebra. Extended static checking(ESC) in the PF-style.

Notes:

Lecture 3

PF-transform: extended static checking by calculation

Date:

11/10/10 (Monday, 10h-13h). Room: DI A.1, Lecturer: J.N. Oliveira

Topics:

Verification conditions in the PF-style. 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, 10h-13h). Room: DI A.1, Lecturer: J.N. Oliveira

Topics: Provisional schedule as follows:

  • 10h00 - Carlos Eduardo Bastos e Marques da Silva: Variations on a Alloy-Centric Tool-chain 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 first-order logics

Date:

25/10/10 (Monday, 10h-13h). Room: DI A.1, Lecturer: Luís Pinto

Topics:

  1. Propositional Logic (PL): Syntax; Semantics; Proof system; Adequacy of the proof system
  2. First-Order Logic (FOL): Syntax; Semantics; Proof system; Theory for equality
  3. Intuitionistic Logic: Natural deduction systems (propositional and first-order)

Notes:

  • A revision of propositional and first-order logics (PDF)

Lecture 6

Validity Checking in Propositional and Forst-Order Logic

Date:

08/11/10 (Monday, 10h-13h). Room: DI A.1, Lecturer: José Bacelar Almeida

Topics:

  1. Propositional Logic: general remarks; normal forms (NNF, CNF, DNF); validity/satisfiability in CNFs.
  2. First-Order Logic: general remarks; normal forms (NNF, prenex, Herbrand/Skolem); Herbrand's theorem; semi-decidability; decidable fragments.
  3. First-Order Theories: basic concepts; some theories of interest; SMT provers.

Notes:

  • Validity Checking in Propositional and First-Order 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 Curry-Howard correspondence

Date:

15/11/10 (Monday, 10h-13h). Room: DI A.1, Lecturer: José Espírito Santo

Topics:

  1. Proof Theory: Natural Deduction; Normalisation; Other proof systems
  2. The λ-calculus: the untyped λ-calculus; the simply-typed λ-calculus
  3. The Curry-Howard correspondence, variants, and uses

Notes:

  • The λ-calculus and the Curry-Howard correspondence (PDF)

Bibliography:

  • See references on the notes

Lecture 8

Type Systems and Logics

Date:

22/11/10 (Monday, 10h-13h). Room: DI A.1, Lecturer: Maria João Frade

Topics:

  1. Proof assistants based on type theory
  2. Pure Type Systems
  3. The Lambda Cube
  4. 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. Proof-assistants 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 Proof-Assistant

Date:

29/11/10 (Monday, 10h-13h). Room: DI A.1, Lecturer: José Bacelar Almeida

Topics:

  1. Gallina language (Coq specification language)
  2. Interactive proof development environment
  3. Case study: correctness of sorting algorithms

Notes:

  • The Coq Proof-Assistant (PDF)

Bibliography:

Lecture 10

An Introduction to the Frama-C tool for the Analysis of C code

Date:

6/12/10 (Monday, 10h-13h). Room: DI A.1, Lecturer: Jorge Sousa Pinto

Topics:

  1. Overview of formal code analysis and verification techniques: static analysis; abstract interpretation; software model checking; deductive verification
  2. Introduction to Frama-C and its plugins
  3. The Jessie tool: verification of safety properties of C code. The GWhy GUI and the multiprover facilities
  4. The ACSL specification language. Verification of functional properties with Jessie.

Notes:

  • Safety veriication with Frama-C (PDF)
  • Functional Verification with Frama-C (PDF)

Bibliography:

  • Loc Correnson, Pascal Cuoq, Armand Puccetti, and Julien Signoles. Frama-C user manual. from the Frama-C website, http://frama-c.com, 2010.
  • Patrick Baudin, Jean-Christophe Fillitre, Claude March, Benjamin Monate, Yannick Moy, and Virgile Prevosto. ACSL: ANSI/ISO C Specification Language. Preliminary Design (version 1.4). from the Frama-C website, http://frama-c.com, 2010.
  • Yannick Moy and Claude March´e. Jessie Plugin Tutorial. LRI, February 2010. Beryllium Version.

-- Created by : JoseNunoOliveira - 24 Sep 2010

r13 - 07 Dec 2010 - 16:58:04 - JorgeSousaPinto
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM