FEUP-MFES

Repository of code developed for the course MFES @FEUP.

Info

• Date : 4th Year, 1st Semester, 2020/2021
• Course : Métodos Formais em Engenharia de Software | Formal Methods in Software Engineering (MFES)
• Contributors : Vítor Gonçalves

Table of Contents

• TEST01
• TEST02
• TP01
• TP02
• TP03
• TP04
• TP05
• TP06
• TP07
• TP08
• TP09
• TP10

TEST01

• Content: Some solved tests from previous years. Test includes content from tp01 to tp05 (Dafny).
• Resolution : TEST01

TEST02

• Content: Some solved tests from previous years. Test includes content from tp06 to tp10 (Alloy).
• Resolution : TEST02

TP01

• Content: Exercises on program verification with Hoare Logic
• Specification : English
• Resolution : TP01

TP02

• Content: Exercises on the verification of simple imperative programs with Hoare logic and Dafny
• Specification : English
• Source Code : TP02

TP03

• Content: Exercises on program verification with arrays and quantifiers in Dafny
• Specification : English
• Source Code : TP03

TP04

• Content: Exercises on design by contract and verification of object-oriented programs in Dafny (Part I)
• Specification : English
• Source Code : TP04

TP05

• Content: Exercises on design by contract and verification of object-oriented programs in Dafny (Part II)
• Specification : English
• Source Code : TP05

TP06

• Content: Exercises on First Order Logic (FOL) and Set Theory
• Source Code : TP06

TP07

• Content: Getting familiar with Alloy
• Source Code : TP07

TP08

• Content: Modulation of a file system in Alloy
• Source Code : TP08

TP09

• Content: Graphs in Alloy and Labeled Transition Systems
• Source Code : TP09

TP10

• Content: Use event idiom to module a Stack
• Source Code : TP10