Collecting Semantics under Predicate Abstraction in the K Framework

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.