Runtime assertion checking and static verification: Collaborative partners

Fonenantsoa Maurica; David R. Cok; Julien Signoles

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

Runtime assertion checking and static verification: Collaborative partners

Fonenantsoa Maurica
, David R. Cok
, Julien Signoles

CEA/UVSQ/CNRS

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

Abstract

Runtime assertion checking aspires to a similar level of sound and complete checking of software as does static deductive verification. Furthermore, for the same source language and specification language, runtime and static checking should implement as closely as possible the same semantics. We describe here the architecture used by two different systems to achieve this goal. We accompany that with descriptions of novel designs and implementations that add new capabilities to runtime assertion checking, bringing it closer to the feature coverage of static verification.

Original language	English
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 Verlag
Pages	75-91
Number of pages	17
ISBN (Print)	9783030034207
DOIs	https://doi.org/10.1007/978-3-030-03421-4_6
Publication status	Published - 1 Jan 2018
Externally published	Yes
Event	8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018 - Limassol, Cyprus Duration: 5 Nov 2018 → 9 Nov 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

Conference

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

Access to Document

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

Cite this

Maurica, F., Cok, D. R., & Signoles, J. (2018). Runtime assertion checking and static verification: Collaborative partners. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, Proceedings (pp. 75-91). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11245 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-030-03421-4_6

Maurica, Fonenantsoa ; Cok, David R. ; Signoles, Julien. / Runtime assertion checking and static verification : Collaborative partners. Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, Proceedings. editor / Tiziana Margaria ; Bernhard Steffen. Springer Verlag, 2018. pp. 75-91 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{4b942a410bb146b0b36cd45d53b096e3,

title = "Runtime assertion checking and static verification: Collaborative partners",

abstract = "Runtime assertion checking aspires to a similar level of sound and complete checking of software as does static deductive verification. Furthermore, for the same source language and specification language, runtime and static checking should implement as closely as possible the same semantics. We describe here the architecture used by two different systems to achieve this goal. We accompany that with descriptions of novel designs and implementations that add new capabilities to runtime assertion checking, bringing it closer to the feature coverage of static verification.",

author = "Fonenantsoa Maurica and Cok, \{David R.\} and Julien Signoles",

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

month = jan,

day = "1",

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

language = "English",

isbn = "9783030034207",

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

publisher = "Springer Verlag",

pages = "75--91",

editor = "Tiziana Margaria and Bernhard Steffen",

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

}

Maurica, F, Cok, DR & Signoles, J 2018, Runtime assertion checking and static verification: Collaborative partners. 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 Verlag, pp. 75-91, 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2018, Limassol, Cyprus, 5/11/18. https://doi.org/10.1007/978-3-030-03421-4_6

Runtime assertion checking and static verification: Collaborative partners. / Maurica, Fonenantsoa; Cok, David R.; Signoles, Julien.
Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, Proceedings. ed. / Tiziana Margaria; Bernhard Steffen. Springer Verlag, 2018. p. 75-91 (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 › peer-review

TY - GEN

T1 - Runtime assertion checking and static verification

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

AU - Maurica, Fonenantsoa

AU - Cok, David R.

AU - Signoles, Julien

PY - 2018/1/1

Y1 - 2018/1/1

N2 - Runtime assertion checking aspires to a similar level of sound and complete checking of software as does static deductive verification. Furthermore, for the same source language and specification language, runtime and static checking should implement as closely as possible the same semantics. We describe here the architecture used by two different systems to achieve this goal. We accompany that with descriptions of novel designs and implementations that add new capabilities to runtime assertion checking, bringing it closer to the feature coverage of static verification.

AB - Runtime assertion checking aspires to a similar level of sound and complete checking of software as does static deductive verification. Furthermore, for the same source language and specification language, runtime and static checking should implement as closely as possible the same semantics. We describe here the architecture used by two different systems to achieve this goal. We accompany that with descriptions of novel designs and implementations that add new capabilities to runtime assertion checking, bringing it closer to the feature coverage of static verification.

UR - https://www.scopus.com/pages/publications/85056468221

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

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

M3 - Conference contribution

AN - SCOPUS:85056468221

SN - 9783030034207

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

SP - 75

EP - 91

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

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - Springer Verlag

Y2 - 5 November 2018 through 9 November 2018

ER -

Maurica F, Cok DR, Signoles J. Runtime assertion checking and static verification: Collaborative partners. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation. Verification - 8th International Symposium, ISoLA 2018, Proceedings. Springer Verlag. 2018. p. 75-91. (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_6

Runtime assertion checking and static verification: Collaborative partners

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this