Aleksandar Zeljić
CS 357
zeljic@stanford.edu 
10 weeks, Tue/Thu, 10:3011:50
Weekly readings
3 Assignments and a project
Credit or letter of recommendation.
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
Mathematical model of the system:
Specification of the problem/property:
Method to proove the property
What is reasoning?
Deductive vs. Inductive vs. Abductive
All men are mortal.
Socrates is a man.
Socrates is mortal.
Search for 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?
Finite and Infinite state systems:
Properties:
Safety  system does not fail catastrophically
Security  system is free from vulnerabilities
Verification  system behaves as intended
SATisfiability solvers
Satisfiability Modulo Theory solvers
Automated Theorem Provers
Interactive Automated Theorem Provers
Model Checkers
Answering yes/no questions …
SATisfiability
… in presence of theories?



Satisfiability Modulo Theories
First NPcomplete problem Cook/Levin theorem 1971
DP/DPLL procedure in 1960s, CDCL in early 2000s
Swiss Army Knife of combinatorial problem solving:
Decision Problems Yes/No answers
Function problems find one solution
Enumeration problems find all solutions
Optimization problems
Color a map with 4 colors … no adjacent areas share a color. 1976  first computer proof
1996  Simpler proof
2005  Coq proof


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}:
Formal method for software developement
Specification, Design, Proof, Code generation
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
Grasshopper based on an extension of HC called Separation Logic

Marabou, ReluVal, Planet, etc. 