Formal Methods

Course given by DCC-UFMG

---

• Plano de ensino
• Instructor:
  • Haniel Barbosa, Office 4323, DCC, hbarbosa@dcc.ufmg.br

---

Outline

1. Formal Methods
2. Topic 1: Alloy
   1. Introduction
   2. Modeling
   3. Dynamic Systems
3. Topic 2: Constraint Solving for Formal Verification
   1. Alloy encodings
   2. SAT solving
   3. SAT and SMT encodings
4. Topic 3: Dafny
   1. Introduction
   2. Arrays, Invariants and Frame Conditions
   3. OO programming and verification

---

An overview of formal methods in three parts.

Topic 1: Alloy

Introduction

Modeling

Dynamic Systems

Topic 2: Constraint Solving for Formal Verification

Alloy encodings

SAT solving

SAT and SMT encodings

Topic 3: Dafny

Introduction

Arrays, Invariants and Frame Conditions

OO programming and verification