An Institutional Foundation for the K Semantic Framework

Claudia-Elena Chirita, Traian Florin Serbanuta

Research output: Contribution to journalArticlepeer-review

72 Downloads (Pure)


We advance an institutional formalisation of the logical systems that underlie the K semantic framework and are used to capture both structural properties of program configurations through pattern matching, and changes of configurations through reachability rules. By defining encodings of matching and reachability logic into the institution of first-order logic, we set the foundation for integrating K into logic graphs of heterogeneous institution-based specification languages such as HETCASL. This will further enable the use of the K tool with other existing formal specification and verification tools associated with Hets.
Original languageEnglish
Pages (from-to)9-29
Number of pages21
JournalLecture Notes in Computer Science
Early online date30 Dec 2015
Publication statusE-pub ahead of print - 30 Dec 2015

Cite this