Razor swMATH ID: 39520 Software Authors: Salman Saghafi; Daniel J. Dougherty Description: Razor: Provenance and Exploration in Model-Finding. Razor is a model-finder for first-order theories presented geometric form; geometric logic is a variant of first-order logic that focuses on “observable” properties. An important guiding principle of Razor is that it be accessible to users who are not necessarily expert in formal methods; application areas include software design, analysis of security protocols and policies, and configuration management. A core functionality of the tool is that it supports exploration of the space of models of a given input theory, as well as presentation of provenance information about the elements and facts of a model. The crucial mathematical tool is the ordering relation on models determined by homomorphism, and Razor prefers models that are minimal with respect to this homomorphism- ordering. Homepage: https://web.cs.wpi.edu/~dd/publications/paar14.pdf Source Code: https://github.com/salmans/RazorExamples Related Software: MiniSat; iProver; iProver-Eq; Kodkod; Mace4; E-Darvin; z3; Darwin; TPTP Cited in: 1 Publication Cited by 3 Authors 1 Danas, Ryan 1 Dougherty, Daniel J. 1 Saghafi, Salman Cited in 0 Serials Cited in 1 Field 1 Computer science (68-XX) Citations by Year