Advanced Topics in Formal Methods


Aleksandar Zeljić
CS 357

Course details


Introduce yourselves:

  • Name

  • Level of studies

  • Interest/experience with formal methods

  • Mnemonic - give us a fun fact about yourself


  • Patriot Missile Failure

  • Pentium I FDIV bug

  • Ariane 5

  • The Millenium Bug

  • Java's Tim Sorting bug

Formal Methods

What are 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: $\forall x. x = x$
    • Symmetry: $\forall x,y. x=y \Rightarrow y=x$
    • Transitivity: $\forall x,y,z. x=y \land y=z \Rightarrow x=z$
  • Inference rules:

$A$       $A\Rightarrow B$


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,


  • 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



Answering yes/no questions

\[({\color{blue}a} \lor {\color{red}b}) \land (\lnot {\color{blue}a} \land {\color{green}c}) \land \lnot {\color{green}c} \]


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.

Performance of SAT solvers


A map of SAT solving


Classes of problems

Decision Problems Yes/No answers

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?

$ a^2 + b^2 = c^2$

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

  • SAT solver: smallest such $n is 7825
  • Only computational proofs exist ~ 200TB
    • Using the Cube and Conquer technique
    • Certificate is 68GB in DRAT format

B Method

  • Formal method for software developement

    • Specification, Design, Proof, Code generation

  • Used to synthesize code for the Paris line 14
    • 110k B loc $\rightarrow$ 86k ADA loc
    • Running since 1998
    • No bugs detected to date

Zelkowa by AWS

  • AWS tool for verifying policy security

  • Security policy -> SMT encoding -> SMT solver

  • Z3 and CVC4 for Strings/RegExps/BVs/Arithmethic

  • Checks for privacy and lifetime violations of user data

Opium - Optimal Package installer

  • Unlike most default package managers it is complete
  • Optimizes package size or number of packages it modifies
  • Uses SAT, pseudo boolean and LP solvers


  • Programming languages with verification constructs built-in
  • Based on Hoare's Calculus
  • Checks verification conditions at compile time
  • Uses Z3 as backend engine
  • https://​rise4fun.​com/​Dafny

Grasshopper based on an extension of HC called Separation Logic

Verification of Neural Networks


  • Show safety properties

  • DNN uses ReLUs: $\mathit{ReLU(x)}=\mathit{max(x,0)}$

  • SMT solvers: ~20 nodes.

  • Specialized tools:

Marabou, ReluVal, Planet, etc.