MAP/i - Foundations of Computing

Option I: Program Semantics, Verification, and Construction

Final Grades

Nome Part I Part II Part III Final
Andreia Sofia da Costa Teixeira 16 16 16 16
Arif Rahman 10 14 14 13
Daniela Carneiro da Cruz 14 14 16 15
David Miguel Ramalho Pereira 15 16 17 16
Hugo Daniel dos Santos Macedo 16 18 17 17
Hugo Sereno Ferreira 15 17 18 17
Jorge Leonel Gonçalves Matos F 15 12 11
José Carlos de Queirós Pinto 15 18 16 16
Paulo César Oliveira Jesus 15 15 16 15
Rui Jorge Pereira Gonçalves 15 14 F 12
Miguel Pereira   17   R

Part I

Each student must complete and write the solutions of this assignment alone. The deadline is : *20/02/2008 *The answers must be send by e-mail to the following emails: \{nam,amf,sbb,luis\} at

Part II

Students are expected to work in groups of two; each group will be assessed based on the following three components.

COQ Exercises

Should be sent by e-mail to this address. The deadline is the date of the presentations session.

Caduceus Mini-project

A list of examples of programs verified with Caduceus can be found here.

Select a program with a similar level of difficulty (not listed in the examples). Write an adequate specification and verify the program using Caduceus and the Coq proof assistant.

Groups should write a short report on their work (with proof scripts attached) and prepare a short talk (5 minutes) to be given in the final presentations session (see date below).

Paper Reading

Each group should select one paper from the following list. Please send a mail to this address with your choice. Papers will be allocated on a first come, first served basis. Groups will give a talk (20 minutes) on the paper in the presentations session (see date below).

  • Efficient Weakest Preconditions. K. Rustan M. Leino. link

  • Boogie: A Modular Reusable Verifier for Object-Oriented Programs. Mike Barnett, Bor-Yuh Evan Chang, Robert deLine, Bart Jacobs, and K. Rustan M. Leino. link

  • Foundational Proof-Carrying Code. Andrew W. Appel. link

  • Proof Obligations Preserving Compilation (Extended abstract). Gilles Barthe, Tamara Rezk and Ando Saabas. link

  • Beyond Assertions: Advanced Specification and Verification with JML and ESC / Java2. Patrice Chalin, Joseph Kiniry, Gary T. Leavens and Erki Poll. link

  • A Certifying Compiler for Java. Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Mark Plesko, Kenneth Cline. link

  • A Tutorial on Recursive Types in Coq. Eduardo Gimenez and Pierre Casteran. link

  • Universes: Lightweight Ownership for JML. Werner Dietl and Peter Mueller. link


  • Deadline for delivery of Caduceus mini-project report: February 4
  • Presentations session and deadline for delivery of Coq Exercises: February 11

Part III

  • Reading and presenting a paper in the field (one paper per student)
  • Papers will become available here very soon
  • Date of presentations: February 4th

r18 - 27 Sep 2008 - 11:44:49 - JoseBacelarAlmeida
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM