Avestan: A declarative modeling language based on SMT-LIB

Author

Vakili, Amirhossein ; Day, Nancy A.

Author_Institution

Cheriton Sch. of Comput. Sci., Univ. of Waterloo, Waterloo, ON, Canada

fYear

2012

fDate

2-3 June 2012

Firstpage

36

Lastpage

42

Abstract

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.

Keywords

computability; formal verification; simulation languages; Avestan model; LIB; SMT solver; declarative modeling language; digital product certification; digital product verification; readability; satisfiability modulo theory; Analytical models; Binary trees; Computational modeling; Educational institutions; Humans; Metals; Writing; Alloy; Declarative Model; First-Order Logic; Relational Construct; SMT solver; SMT-LIB;

fLanguage

English

Publisher

ieee

Conference_Titel

Modeling in Software Engineering (MISE), 2012 ICSE Workshop on

Conference_Location

Zurich

ISSN

2156-788

Print_ISBN

978-1-4673-1756-6

Type

conf

DOI

10.1109/MISE.2012.6226012

Filename

6226012