Project Overview

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.

Contributors

Sorawee Porncharoenwase, Tim Nelson, and Shriram Krishnamurthi

Relevant Links

CompoSAT: Specification-Guided Coverage for Model Finding Paper