Formal Methods in Software Engineering

Collecting Semantics under Predicate Abstraction in the K Framework

Year2010
TypeConference
StatusPostproceedings
AuthorsIrina Asavoae, Mihail Asavoae

Links

Abstract

The K framework is a specialization of rewriting logic for defining programming language semantics.This paper introduces the model checking with predicate abstraction technique into the K framework. To express this technique in K, we go to the foundations of predicate abstraction, that is abstract interpretation, and use its collecting semantics.As such, we propose a suitable description in K for  collecting semantics under predicate abstraction of a simple imperative language. Next, we prove that our K specification for collecting semantics is a sound approximation of the K specification for concrete semantics. This work makes a further step towards the development of program verification methodologies in rewriting logic semantics project in general and  the K framework in particular.

BibTeX

@inproceedings{aa-wrla10, author = {Irina Mariuca Asavoae and Mihail Asavoae}, title = {Collecting Semantics under Predicate Abstraction in the K Framework}, booktitle = {Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Paphos, Cyprus, March 20-21, 2010, Revised Selected Papers}, year = {2010}, pages = {123-139}, editor = {Peter Csaba {"O}lveczky}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {6381}, year = {2010}, isbn = {978-3-642-16309-8}, url = {http://www.springerlink.com/content/g45n848267n34815/[aaWRLA10]} }