Bounded Model Checking of Temporal Formulas with Alloy
classification
💻 cs.SE
cs.LO
keywords
alloyboundedcheckinglogicmodelsystemstemporalanalyzer
read the original abstract
Alloy is formal modeling language based on first-order relational logic, with no specific support for specifying reactive systems. We propose the usage of temporal logic to specify such systems, and show how bounded model checking can be performed with the Alloy Analyzer.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.