Specifying languages and verifying programs with K

Grigore Roşu

doi:10.1109/SYNASC.2013.81

Specifying languages and verifying programs with K

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Proceedings - 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013
Publisher	IEEE Computer Society
Pages	28-31
Number of pages	4
ISBN (Print)	9781479930357
DOIs	https://doi.org/10.1109/SYNASC.2013.81
State	Published - 2013
Event	15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013 - Timisoara, Romania Duration: Sep 23 2013 → Sep 26 2013

Publication series

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

Conference

Conference	15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013
Country/Territory	Romania
City	Timisoara
Period	9/23/13 → 9/26/13

Keywords

Semantics; verification; formal methods; logic

ASJC Scopus subject areas

Software
Modeling and Simulation

Online availability

10.1109/SYNASC.2013.81

Library availability

Discover UIUC Full Text

Cite this

Roşu, G. (2013). Specifying languages and verifying programs with K. In Proceedings - 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013 (pp. 28-31). [6821127] (Proceedings - 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013). IEEE Computer Society. https://doi.org/10.1109/SYNASC.2013.81

Specifying languages and verifying programs with K. / Roşu, Grigore.
Proceedings - 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013. IEEE Computer Society, 2013. p. 28-31 6821127 (Proceedings - 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Roşu, G 2013, Specifying languages and verifying programs with K. in Proceedings - 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013., 6821127, Proceedings - 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013, IEEE Computer Society, pp. 28-31, 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013, Timisoara, Romania, 9/23/13. https://doi.org/10.1109/SYNASC.2013.81

Roşu G. Specifying languages and verifying programs with K. In Proceedings - 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013. IEEE Computer Society. 2013. p. 28-31. 6821127. (Proceedings - 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013). doi: 10.1109/SYNASC.2013.81

@inproceedings{a201ff8d620c4ec594662421834612aa,

title = "Specifying languages and verifying programs with K",

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.",

keywords = "Semantics; verification; formal methods; logic",

author = "Grigore Ro{\c s}u",

year = "2013",

doi = "10.1109/SYNASC.2013.81",

language = "English (US)",

isbn = "9781479930357",

series = "Proceedings - 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013",

publisher = "IEEE Computer Society",

pages = "28--31",

booktitle = "Proceedings - 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013",

note = "15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2013 ; Conference date: 23-09-2013 Through 26-09-2013",

}

TY - GEN

T1 - Specifying languages and verifying programs with K

AU - Roşu, Grigore

PY - 2013

Y1 - 2013

N2 - 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.

AB - 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.

KW - Semantics; verification; formal methods; logic

UR - http://www.scopus.com/inward/record.url?scp=84904551010&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84904551010&partnerID=8YFLogxK

U2 - 10.1109/SYNASC.2013.81

DO - 10.1109/SYNASC.2013.81

M3 - Conference contribution

AN - SCOPUS:84904551010

SN - 9781479930357

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

SP - 28

EP - 31

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

PB - IEEE Computer Society

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

Y2 - 23 September 2013 through 26 September 2013

ER -

Specifying languages and verifying programs with K

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this