<?xml version="1.0" encoding="UTF-8"?><xml><records><record><source-app name="Biblio" version="6.x">Drupal-Biblio</source-app><ref-type>47</ref-type><contributors><authors><author><style face="normal" font="default" size="100%">Alcino Cunha</style></author></authors></contributors><titles><title><style face="normal" font="default" size="100%">Bounded Model Checking of Temporal Formulas with Alloy</style></title><secondary-title><style face="normal" font="default" size="100%">Lecture Note in Computer Science</style></secondary-title></titles><dates><year><style  face="normal" font="default" size="100%">2014</style></year><pub-dates><date><style  face="normal" font="default" size="100%">June</style></date></pub-dates></dates><urls><related-urls><url><style face="normal" font="default" size="100%">https://haslab.uminho.pt/sites/default/files/alcino/files/1207.2746v2.pdf</style></url></related-urls></urls><publisher><style face="normal" font="default" size="100%">Springer</style></publisher><pub-location><style face="normal" font="default" size="100%">Toulouse, France</style></pub-location><volume><style face="normal" font="default" size="100%">8477</style></volume><abstract><style face="normal" font="default" size="100%">&lt;p&gt;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.&lt;/p&gt;
</style></abstract></record></records></xml>