Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Open-World Logic Programs: A New Foundation for Formal Specifications

Ethan Jackson, Nikolaj Bjorner, and Wolfram Schulte

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.

Details

Publication typeTechReport
NumberMSR-TR-2013-55
PublisherMicrosoft Technical Report
> Publications > Open-World Logic Programs: A New Foundation for Formal Specifications