A Framework for Exploring Finite Models
ÖffentlichHerunterladbarer Inhalt
open in viewerThis thesis presents a framework for understanding first-order theories by investigating their models. A common application is to help users, who are not necessarily experts in formal methods, analyze software artifacts, such as access-control policies, system configurations, protocol specifications, and software designs. The framework suggests a strategy for exploring the space of finite models of a theory via augmentation. Also, it introduces a notion of provenance information for understanding the elements and facts in models with respect to the statements of the theory. The primary mathematical tool is an information-preserving preorder, induced by the homomorphism on models, defining paths along which models are explored. The central algorithmic ideas consists of a controlled construction of the Herbrand base of the input theory followed by utilizing SMT-solving for generating models that are minimal under the homomorphism preorder. Our framework for model-exploration is realized in Razor, a model-finding assistant that provides the user with a read-eval-print loop for investigating models.
- Creator
- Mitwirkende
- Degree
- Unit
- Publisher
- Language
- English
- Identifier
- etd-043015-110044
- Stichwort
- Advisor
- Committee
- Defense date
- Year
- 2015
- Date created
- 2015-04-30
- Resource type
- Rights statement
Beziehungen
- In Collection:
Objekte
Artikel
Miniaturansicht | Titel | Sichtbarkeit | Embargo Release Date | Aktionen |
---|---|---|---|---|
saghafi1.pdf | Öffentlich | Herunterladen | ||
saghafi2.pdf | Öffentlich | Herunterladen |
Permanent link to this page: https://digital.wpi.edu/show/5q47rn87k