Bounded Model Checking of Temporal Formulas with Alloy

Abstract

Alloy is a formal modeling language based on first-order relational logic, with no native support for specifying reactive systems. We propose an extension of Alloy to allow the specification of temporal formulas using LTL, and show how they can be verified by bounded model checking with the Alloy Analyzer.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{Cunha14,
  author       = {Alcino Cunha},
  editor       = {Yamine A{\"{\i}}t Ameur and
                  Klaus{-}Dieter Schewe},
  title        = {Bounded Model Checking of Temporal Formulas with Alloy},
  booktitle    = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 4th International
                  Conference, {ABZ} 2014, Toulouse, France, June 2-6, 2014. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {8477},
  pages        = {303--308},
  publisher    = {Springer},
  year         = {2014},
  url          = {https://doi.org/10.1007/978-3-662-43652-3\_29},
  doi          = {10.1007/978-3-662-43652-3\_29},
  timestamp    = {Tue, 14 May 2019 10:00:50 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/Cunha14.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}