Exploring Theories with a Model-Finding Assistant

8 years 10 days ago

Download web.cs.wpi.edu

We present an approach to understanding ﬁrst-order theories by exploring their models. A typical use case is the analysis of artifacts such as policies, protocols, conﬁgurations, and software designs. For the analyses we oﬀer, users are not required to frame formal properties or construct derivations. Rather, they can explore examples of their designs, conﬁrming the expected instances and perhaps recognizing bugs inherent in surprising instances. Key foundational ideas include: the information preorder on models given by homomorphism, an inductively-deﬁned reﬁnement of the Herbrand base of a theory, and a notion of provenance for elements and facts in models. The implementation makes use of SMT-solving and an algorithm for minimization with respect to the information preorder on models. Our approach is embodied in a tool, Razor, that is complete for ﬁnite satisﬁability and provides a read-eval-print loop used to navigate the set of ﬁnite models of a theory and to disp...

Salman Saghafi, Ryan Danas, Daniel J. Dougherty

Real-time Traffic