MAP/i - Foundations of Computing

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 ncc.up.pt.

Part II

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

COQ Exercises

• Coq Exercises (collected from the slides).

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

Dates

• 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