×

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 in 0 Serials

Citations by Year