# Advanced Topics in Formal Methods

## Introduction

 Aleksandar Zeljić CS 357 zeljic@stanford.edu

### Course details

• 10 weeks, Tue/Thu, 10:30-11:50

• 3 Assignments and a project

• Credit or letter of recommendation.

### Whiparound

Introduce yourselves:

• Name

• Level of studies

• Interest/experience with formal methods

• Mnemonic - give us a fun fact about yourself

## Motivation

• Patriot Missile Failure

• Pentium I FDIV bug

• Ariane 5

• The Millenium Bug

• Java's Tim Sorting bug

## Formal Methods

### So you want to use formal methods?

Mathematical model of the system:

• Computer easy
• Airplane complicated

Specification of the problem/property:

• Formal Language - Boolean logic, FOL, LTL/CTL, etc.
• Automatic vs. Manual vs. Impossible

Method to proove the property

• Proof calculus, decision procedures Enter Automated Reasoning

### What is Automated Reasoning

What is reasoning?

Deductive vs. Inductive vs. Abductive

All men are mortal.

Socrates is a man.

Socrates is mortal.

## Formal proof system:

• Axioms
• Reflexivity:
• Symmetry:
• Transitivity:
• Inference rules:

Search for a proof!

## What is a proof?

Proof - Sequence of steps from assumptions to conclusion convincing to a sceptic

What is the correct step size?

Small vs. Big vs. Gap

Computers can only perform small steps.

What is actually hard in a proof?

### What kind of systems are we looking at?

Finite and Infinite state systems:

• Unbounded data structures:
• stacks, queues, counters, clocks, etc.
• Unbounded control structures:
• parametrized systems, multi-threaded, concurrent programs,

Properties:

• Safety - system does not fail catastrophically

• Security - system is free from vulnerabilities

• Verification - system behaves as intended

### Formal Methods Tools

SATisfiability solvers

• MiniSAT, Lingeling, Glucose, CryptoMiniSAT,

Satisfiability Modulo Theory solvers

• Z3, CVC4, Yices, MathSAT, Boolector,

Automated Theorem Provers

• Vampire, E, Satallax, iProver,

Interactive Automated Theorem Provers

• Isabelle, Coq, Lean, Agda,

Model Checkers

• SPIN, UPPAAL, PRISM, NuSMV, CBMC, CoSA

### Satisfiability

SATisfiability

in presence of theories?

 ${\color{blue} a \equiv x + y = z }$ ${\color{red}b \equiv x \cdot y < z}$ ${\color{green} c \equiv z - y = x}$

Satisfiability Modulo Theories

### Propositional Satisfiability

• First NP-complete problem Cook/Levin theorem 1971

• Reducible to a landscape of other NP-complete problems
• text-book example of intractable
• DP/DPLL procedure in 1960s, CDCL in early 2000s

• Handles formulas with millions of variables and clauses.
• Swiss Army Knife of combinatorial problem solving:

• Scheduling, Packing, Coloring, Pathing, etc.

### Classes of problems

Function problems find one solution

Enumeration problems find all solutions

Optimization problems

## Success stories and Challenges

### Four Color Theorem

 Color a map with 4 colors … no adjacent areas share a color. 1976 - first computer proof Considers ~1400 states several errors 1996 - Simpler proof Considers 633 states 2005 - Coq proof Trust only the Coq kernel

### Pythagorean Triples Problem

Consider all partitions of {1,2,} into finitely many parts.

Does always at least one contain a Pythagorean Triple?

Proof: Show that to be true of a finite set {1,2,,n}: