Avestan: a declarative modeling language based on SMT-LIB

Avestan is a declarative modelling language compatible with SMT-LIB. SMT-LIB is an standard input language that is supported by the state-of-the-art satisfiability modulo theory solvers (SMT solvers). The recent advances in SMT solvers have introduced them as efficient analysis tools; as a result, they are becoming more popular in the verification and certification of digital products. SMT-LIB was designed to be machine readable rather than human readable. In this paper, we present Avestan, a declarative modelling language that is intended to be analyzed by SMT solvers and readable by humans. An Avestan model is translated to an SMT-LIB model so that it can be analyzed by different SMT solvers. Avestan has relational constructs that are heavily inspired by Alloy; we added these constructs to increase the readability of an Avestan model.