An Institutional Foundation for the K Semantic Framework. / Chirita, Claudia-Elena; Serbanuta, Traian Florin.

In: Lecture Notes in Computer Science, Vol. 9463, 30.12.2015, p. 9-29.

Research output: Contribution to journalArticlepeer-review

E-pub ahead of print




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
This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 25043958