CompoSAT: Specification-Guided Coverage for Model Finding
Model-finding tools like the Alloy Analyzer produce concrete examples of how a declarative specification can be satisfied. These formal tools are useful in a wide range of domains: software design, security, networking, and more. By producing concrete examples, they assist in exploring system behavior and can help find surprising faults.
Sorawee Porncharoenwase, Tim Nelson, and Shriram Krishnamurthi
CompoSAT: Specification-Guided Coverage for Model Finding Paper