K Semantics for Abstractions

This dissertation shows how abstract interpretation’s view of program analysis and verification can be instilled in the K framework in a generic fashion as reflective semantics.

The program analysis and verification approaches tackled in K are either model checking, achieved via Maude’s LTL model checker, or deductive verification, achieved via matching logic. However, the third major verification technique, namely abstract interpretation, was not systematically approached in K. Our thesis addresses this omission and covers it. As such, we design a generic method for defining in K abstract specifications of pushdown systems and fixpoint iterators over these specifications. We demonstrate the efficiency of this design by instantiating it with three case studies of abstractions for data analysis, alias analysis, and shape analysis.