Specifying languages and verifying programs with K

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationProceedings - 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013
PublisherIEEE Computer Society
Pages28-31
Number of pages4
ISBN (Print)9781479930357
DOIs
StatePublished - 2013
Event15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013 - Timisoara, Romania
Duration: Sep 23 2013Sep 26 2013

Publication series

NameProceedings - 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013

Conference

Conference15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013
CountryRomania
CityTimisoara
Period9/23/139/26/13

Keywords

  • Semantics; verification; formal methods; logic

ASJC Scopus subject areas

  • Software
  • Modeling and Simulation

Fingerprint Dive into the research topics of 'Specifying languages and verifying programs with K'. Together they form a unique fingerprint.

Cite this