A language-independent program verification framework

Xiaohong Chen; Grigore Roşu

doi:10.1007/978-3-030-03421-4_7

A language-independent program verification framework

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

Abstract

This invited paper describes an approach to language-independent deductive verification using the K semantics framework, in which an operational semantics of a language is defined and a program verifier together with other language tools are generated automatically, correct-by-construction.

Original language	English (US)
Title of host publication	Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, Proceedings
Editors	Tiziana Margaria, Bernhard Steffen
Publisher	Springer
Pages	92-102
Number of pages	11
ISBN (Print)	9783030034207
DOIs	https://doi.org/10.1007/978-3-030-03421-4_7
State	Published - 2018
Event	8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018 - Limassol, Cyprus Duration: Nov 5 2018 → Nov 9 2018

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	11245 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018
Country/Territory	Cyprus
City	Limassol
Period	11/5/18 → 11/9/18

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Online availability

10.1007/978-3-030-03421-4_7

Library availability

Discover UIUC Full Text

Cite this

Chen, X., & Roşu, G. (2018). A language-independent program verification framework. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, Proceedings (pp. 92-102). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11245 LNCS). Springer. https://doi.org/10.1007/978-3-030-03421-4_7

A language-independent program verification framework. / Chen, Xiaohong; Roşu, Grigore.
Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, Proceedings. ed. / Tiziana Margaria; Bernhard Steffen. Springer, 2018. p. 92-102 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11245 LNCS).

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

Chen, X & Roşu, G 2018, A language-independent program verification framework. in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11245 LNCS, Springer, pp. 92-102, 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018, Limassol, Cyprus, 11/5/18. https://doi.org/10.1007/978-3-030-03421-4_7

Chen X, Roşu G. A language-independent program verification framework. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, Proceedings. Springer. 2018. p. 92-102. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-03421-4_7

Chen, Xiaohong ; Roşu, Grigore. / A language-independent program verification framework. Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, Proceedings. editor / Tiziana Margaria ; Bernhard Steffen. Springer, 2018. pp. 92-102 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{4376e7704daf47e6afb1a535faa013d4,

title = "A language-independent program verification framework",

abstract = "This invited paper describes an approach to language-independent deductive verification using the K semantics framework, in which an operational semantics of a language is defined and a program verifier together with other language tools are generated automatically, correct-by-construction.",

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

note = "Publisher Copyright: {\textcopyright} Springer Nature Switzerland AG 2018.; 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018 ; Conference date: 05-11-2018 Through 09-11-2018",

year = "2018",

doi = "10.1007/978-3-030-03421-4_7",

language = "English (US)",

isbn = "9783030034207",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "92--102",

editor = "Tiziana Margaria and Bernhard Steffen",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, Proceedings",

address = "Germany",

}

TY - GEN

T1 - A language-independent program verification framework

AU - Chen, Xiaohong

AU - Roşu, Grigore

N1 - Publisher Copyright: © Springer Nature Switzerland AG 2018.

PY - 2018

Y1 - 2018

N2 - This invited paper describes an approach to language-independent deductive verification using the K semantics framework, in which an operational semantics of a language is defined and a program verifier together with other language tools are generated automatically, correct-by-construction.

AB - This invited paper describes an approach to language-independent deductive verification using the K semantics framework, in which an operational semantics of a language is defined and a program verifier together with other language tools are generated automatically, correct-by-construction.

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

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

U2 - 10.1007/978-3-030-03421-4_7

DO - 10.1007/978-3-030-03421-4_7

M3 - Conference contribution

AN - SCOPUS:85056450674

SN - 9783030034207

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 92

EP - 102

BT - Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, Proceedings

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - Springer

T2 - 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018

Y2 - 5 November 2018 through 9 November 2018

ER -

A language-independent program verification framework

Abstract

Publication series

Other

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this