Formal Methods for Everyone: Practical Tools for Computer-Aided Reasoning
summary
Concrete outcomes: Z3 SMT solver is used (Python, C/C++, Java bindings) to decide satisfiability over integers, strings, bitvectors and floating point and to produce counterexample models (example: left shift by 3 equals multiply by 8 is valid, right shift vs divide by 8 yields a concrete counterexample). A modified LLVM bitcode pipeline runs KLEE symbolic execution to generate replayable testcases, discover crashes and out‑of‑bounds accesses, and the demos and tooling are open source and runnable today.
AI-written summary · about
chapters (20)
- 0:00Intro
- 0:29Outline
- 1:05What are Formal Methods?
- 2:06Formal Methods At Work
- 3:07Formal Methods in Practice
- 3:45A Brief Tour of Formal Logic
- 4:30Boolean Satisfiability
- 5:31SMT Solvers
- 8:06The Z3 Theorem Prover
- 9:56What can Z3 Do?
- 10:39Proving an Invariant with Z3
- 11:38Finding a Counterexample with Z3
- 12:41Symbolic Execution
- 13:50Concrete vs. Symbolic
- 15:13KLEE Virtual Machine
- 15:58Using KLEE
- 17:29Testing a Simple Function
- 18:10Testing with KLEE
- 18:35What's Next for Formal Methods?
- 19:39Conclusion
related talks
21mEnhancing Symbolic Execution with Machine-Checked Safety Proofs
31mSound Symbolic Execution via Abstract Interpretation and its Application to Sec...
58mAutomating Relational Verification of Infinite-State Programs
30mLet's Build a Symbolic Analyser And Automatically Find Bugs
19mAutomated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs
46mVerifying code using automated reasoning
55mCode Analysis with Zero False Positives in Java
01h 00mAI Safety through Programming?