University of Illinois Urbana-Champaign

IsaK: A Complete Semantics of K

Li, Liyi; Gunter, Elsa L.

Content Files
K-semantics-tech-report.pdf

Permalink

https://hdl.handle.net/2142/100116

Description

Title
IsaK: A Complete Semantics of K
Author(s)
  • Li, Liyi
  • Gunter, Elsa L.
Issue Date
2018-06-25
Keyword(s)
K framework, formal semantics, Isabelle
Date of Ingest
2018-06-25T20:49:48Z
Abstract
K (Roşu and Şerbănuţă, 2010) is a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be de ned using con gurations, computations and rules. In this paper we de ne IsaK, a reference semantics for K, which was developed through discussion with the K team to meet their expectations of a semantics of K. IsaK is de ned in the interactive theorem prover Isabelle/HOL (Paulson, 1990), and, to the best of our knowledge, is the most complete of any existing K speci cation. IsaK de nes the full behavior of K, a useful sort system for K and suggests several undesirable behaviors in the current K implementations (K 3.6 and K 4.0). We also provide an OCaml based executable K interpreter generated automatically from the K speci cation in Isabelle. By using a prede ned K parser, the K interpreter is suitable to interpret major K de nitions for large languages such as the LLVM semantics in K, the Java semantics in K and the C semantics in K. We ran a test suite including 13 speci cations and 356 programs to test our K interpreter and we are able to compile all 13 speci cations and run the 338 programs not requiring keyboard input. As a utility of IsaK, we also formally prove a CTL application in IsaK correct.
Type of Resource
text
Genre of Resource
Technical Report
Language
en
Permalink
http://hdl.handle.net/2142/100116
Sponsor(s)/Grant Number(s)
NSF Grant No.0917218

Owning Collections

Research and Tech Reports - Computer Science PRIMARY