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 journalArticle

E-pub ahead of print

Documents

Links

Abstract

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
Volume9463
Early online date30 Dec 2015
DOIs
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