@techreport{jackson2013open-world,
author = {Jackson, Ethan and Schulte, Wolfram and Bjørner, Nikolaj},
title = {Open-World Logic Programs: A New Foundation for Formal Specifications},
year = {2013},
month = {May},
abstract = {Recent advances in decision procedures and constraint solvers can enable a new generation of formal specification languages. In this paper we present a new semantic foundation for formal specifications, called open-world logic programming, which integrates with state-of-the-art solvers. Analysis, verification, and synthesis problems on open-world logic programs can be converted to constraints by a quantifier-elimination scheme using symbolic execution. This paper presents the features, semantics, and algorithms of open-world logic programs. We have implemented this approach in the FORMULA specification language, which has been used for production-quality specifications and models.},
publisher = {Microsoft Technical Report},
url = {http://approjects.co.za/?big=en-us/research/publication/open-world-logic-programs-a-new-foundation-for-formal-specifications/},
number = {MSR-TR-2013-55},
}