Specifying Languages and Verifying Programs with K

From FSL
Jump to: navigation, search

Specifying Languages and Verifying Programs with K
Grigore Rosu
SYNASC'13, IEEE/CPS, pp 28-31. 2013
Abstract. K is a rewrite-based executable semantic framework for defining languages. The K framework is designed to allow implementing a variety of generic tools that can be used with any language defined in K, such as parsers, interpreters, symbolic execution engines, semantic debuggers, test-case generators, state-space explorers, model checkers, and even deductive program verifiers. The latter are based on matching logic for expressing static properties, and on reachability logic for expressing dynamic properties. Several large languages have been already defined or are being defined in K, including C, Java, Python, Javascript, and LLVM.
PDF, Slides(PPTX), K, DOI, SYNASC'13, BIB

Personal tools
Namespaces

Variants
Actions
Navigation