Extending the SMT-Lib Standard with Theory of Nominative Data
Liudmyla Omelchuk, Olena Shyshatska · 2019
We describe the theory of nominative data, formulate the basic prin- ciples of the composition-nominative approach, and define the class of nomina- tive data and functions. By using nominative data, we can increase the level of adequacy of representation data structures, functions, and compositions that are used in programming languages. Thus, in terms of composition-nominative ap- proach, we can build systems of verification of programs based on a unified conceptual basis. Computer-aided verification of computer programs often uses SMT (satisfiability modulo theories) solvers. A common technique is to trans- late preconditions, postconditions, and assertions into SMT formulas in order to determine if required properties can hold. The SMT-LIB Standard was created for forming a common standard and library for solving SMT problems. Now, it is one of the most used libraries for SMT systems. Formulas in SMT-LIB for- mat are accepted by the great majority of current SMT solvers. The theory of nominative data is of interest for software modelling and verification, but cur- rently lacks support in the SMT-LIB format. In the article, we propose the dec- laration for the theory of nominative data for the SMT-LIB Standard 2.6. The goal is the development of SMT solvers with nominative data support.