<?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%">Victor Cacciari Miraldo</style></author><author><style face="normal" font="default" size="100%">Maria João Frade</style></author><author><style face="normal" font="default" size="100%">Cláudio Belo Lourenço</style></author><author><style face="normal" font="default" size="100%">Jorge Sousa Pinto</style></author></authors><secondary-authors><author><style face="normal" font="default" size="100%">Beatriz Sousa Santos</style></author><author><style face="normal" font="default" size="100%">João Cachopo</style></author></secondary-authors></contributors><titles><title><style face="normal" font="default" size="100%">Experimenting with Predicate Abstraction</style></title><secondary-title><style face="normal" font="default" size="100%">Proceedings of Simpósio de Informática - Inforum</style></secondary-title></titles><dates><year><style  face="normal" font="default" size="100%">2013</style></year><pub-dates><date><style  face="normal" font="default" size="100%">September</style></date></pub-dates></dates><urls><related-urls><url><style face="normal" font="default" size="100%">https://haslab.uminho.pt/sites/default/files/jsp/files/predabs-final.pdf</style></url></related-urls></urls><publisher><style face="normal" font="default" size="100%">Universidade de Évora</style></publisher><pub-location><style face="normal" font="default" size="100%">Évora, Portugal</style></pub-location><language><style face="normal" font="default" size="100%">eng</style></language><abstract><style face="normal" font="default" size="100%">&lt;p&gt;Predicate abstraction is a technique employed in software model checking to produce abstract models that can be conservatively checked for property violations in reasonable time. The precision degree of different abstractions of the same program may differ based on (i) the set of predicates used; or (ii) the algorithmic technique employed to generate the model. In this paper we explain how we have implemented and optimized one such technique, that produces the most precise existential abstraction of a program, and give the first steps towards establishing a common framework for both this direct technique and a second one, based on cartesian abstraction by weakest precondition calculations.&lt;/p&gt;
</style></abstract></record></records></xml>