Collection

Tag: sat-solving

Bounded Model Checking and the Decision to Turn Verification into SAT

Bounded model checking recast finite-depth verification as Boolean satisfiability, using rapidly improving SAT solvers to find deep counterexamples without constructing a global symbolic state representation.

↗

Daniel Jackson and Alloy: Lightweight Formal Methods Through Automated Model Finding

Daniel Jackson’s Alloy paired a compact relational modeling language with automatic bounded analysis, making counterexample-driven formal modeling fast enough to fit exploratory software design.

↗