Show simple item record

dc.contributor.authorAbbassi, Ali
dc.contributor.authorDay, Nancy A.
dc.contributor.authorRayside, Derek 19:07:21 (GMT) 19:07:21 (GMT)
dc.description.abstractWe present a variety of translation options for converting Alloy to SMT-LIB via Alloy’s Kodkod interface. Our translations, which are implemented in a library that we call Astra, are based on converting the set and relational operations of Alloy into their equivalent in typed first-order logic (TFOL). We investigate and compare the performance of an SMT solver for many translation options. We compare using only one universal type to recovering Alloy type information from the Kod- kod representation and using multiple types in TFOL. We compare a direct translation of the relations to predicates in TFOL to one where we recover functions from their relational form in Kodkod and repre- sent these as functions in TFOL. We compare representations in TFOL with unbounded scopes to ones with bounded scopes, either pre or post quantifier expansion. Our results across all these dimensions provide di- rections for portfolio solvers, modelling improvements, and optimizing SMT solvers.en
dc.titleAstra Version 1.0: Evaluating Translations from Alloy to SMT-LIBen
dc.typeTechnical Reporten
uws.contributor.affiliation1Faculty of Engineeringen
uws.contributor.affiliation1Faculty of Mathematicsen
uws.contributor.affiliation2David R. Cheriton School of Computer Scienceen
uws.contributor.affiliation2Electrical and Computer Engineeringen

Files in this item


This item appears in the following Collection(s)

Show simple item record


University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages