Student Work

 

Translating Alloy to SMT-LIB Public

Downloadable Content

open in viewer

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.

Creator
Contributors
Publisher
Identifier
  • E-project-032318-155219
Advisor
Year
  • 2018
Date created
  • 2018-03-23
Resource type
Major
Rights statement
License

Relationships

In Collection:

Items

Permanent link to this page: https://digital.wpi.edu/show/xw42n929h