Bounded Model Checking of Temporal Formulas with Alloy
Bounded Model Checking of Temporal Formulas with Alloy
| dc.contributor.author | Alcino Cunha | en |
| dc.date.accessioned | 2017-12-17T09:26:46Z | |
| dc.date.available | 2017-12-17T09:26:46Z | |
| dc.date.issued | 2014 | en |
| dc.description.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. © 2014 Springer-Verlag. | en |
| dc.identifier.uri | http://repositorio.inesctec.pt/handle/123456789/4182 | |
| dc.identifier.uri | http://dx.doi.org/10.1007/978-3-662-43652-3_29 | en |
| dc.language | eng | en |
| dc.relation | 5612 | en |
| dc.rights | info:eu-repo/semantics/openAccess | en |
| dc.title | Bounded Model Checking of Temporal Formulas with Alloy | en |
| dc.type | conferenceObject | en |
| dc.type | Publication | en |
Files
Original bundle
1 - 1 of 1