How Formal Engines Think
Boolean models, reachability, cones of influence, BDDs, SAT, bounded model checking and induction — the ideas inside every formal tool.
What you will learn
- Turn a small circuit into Boolean equations and check two implementations for equivalence with a miter.
- Explain reachability, initial states and why some states are unreachable.
- Use the cone of influence to predict how hard a property will be.
- Describe how BDD- and SAT-based engines work, at a whiteboard level.
- Explain bounded model checking and k-induction, and why induction sometimes needs helper assertions.
Lessons
- 2.1Circuits as Boolean functionsTruth tables, Boolean laws and checking two implementations with a miter.
- 2.2State, transitions and reachabilityWhy formal thinks in states, and what "reachable" means.
- 2.3The cone of influenceOnly logic that can affect a property matters to its proof.
- 2.4Binary decision diagramsA canonical, shared representation of Boolean functions.
- 2.5SAT solving in a nutshellCNF, unit propagation, backtracking and clause learning.
- 2.6Bounded model checking and inductionHow SAT finds deep bugs, and how proofs become unbounded.
- ✎Chapter quiz (5 questions)