Alloy is a tool for writing specifications and constructing instances of these specifications, based on relational logic. Satisfiability Modulo Theories (SMT) solvers embody another popular approach to specification and instance-generation; most solvers implement a language based on the SMT-LIB standard. The Alloy language and the core of SMT-LIB are each formally equivalent, over finite structures, to first-order mathematical logic; however, they support quite different modeling idioms. To help bridge this gap we have initiated a project to construct a translation from Alloy to SMT-LIB.

• This report represents the work of one or more WPI undergraduate students submitted to the faculty as evidence of completion of a degree requirement. WPI routinely publishes these reports on its website without editorial or peer review.

Creator

• McCormick, Kyle D
• Cinelli, Forrest C

Contributors

• Lecce, John

Publisher

• Worcester Polytechnic Institute

Identifier

• E-project-032318-155219

Advisor

• Dougherty, Daniel J.

Year

• 2018

Date created

• 2018-03-23

Resource type

• Major Qualifying Project

Major

• Computer Science
• Interdisciplinary

Rights statement

• In Copyright

License

• All rights reserved