Modular Transformation of Java Exceptions Modulo Errors

Robert Rubbens; Sophie Lathouwers; Marieke Huisman

doi:10.1007/978-3-030-85248-1_5

Modular Transformation of Java Exceptions Modulo Errors

Robert Rubbens^*, Sophie Lathouwers, Marieke Huisman

^*Corresponding author for this work

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

73 Downloads (Pure)

Abstract

Deductive verifiers are used more and more in both academia and industry to prevent costly bugs. Their capabilities of verifying concurrent programs are getting better, but they are still lagging behind with regard to many major programming language features such as exceptions. To improve the situation, this work presents a semantics of Java exceptions which reduces the annotation burden on the user, while still allowing verification of exceptions. This is accomplished by ignoring sources of errors which are irrelevant to functional verification. Additionally, to deal with the complex control flow introduced by finally, a transformation is proposed that simplifies verification of exceptional postconditions and finally into postconditions and goto. We implement the approach and evaluate it against several common exception patterns.

Original language	English
Title of host publication	Formal Methods for Industrial Critical Systems
Subtitle of host publication	26th International Conference, FMICS 2021, Paris, France, August 24–26, 2021, Proceedings
Editors	Alberto Lluch Lafuente, Anastasia Mavridou
Publisher	Springer
Pages	67-84
Number of pages	18
ISBN (Electronic)	978-3-030-85248-1
ISBN (Print)	978-3-030-85247-4
DOIs	https://doi.org/10.1007/978-3-030-85248-1_5
Publication status	Published - 19 Aug 2021
Event	26th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2021 - Virtual Conference Duration: 24 Aug 2021 → 26 Aug 2021 Conference number: 26

Publication series

Name	Lecture notes in computer science
Volume	12863

Conference

Conference	26th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2021
Abbreviated title	FMICS 2021
City	Virtual Conference
Period	24/08/21 → 26/08/21

Access to Document

10.1007/978-3-030-85248-1_5

10.1007_978-3-030-85248-1_5Final published version, 304 KBLicence: Taverne

Data accompanied to the paper: Modular Transformation of Java Exceptions Modulo Errors
Rubbens, B. (Creator), Huisman, M. (Creator) & Lathouwers, S. (Creator), 4TU.Centre for Research Data, 25 Aug 2021
DOI: 10.4121/14905251, https://data.4tu.nl/articles/_/14905251 and one more link, https://data.4tu.nl/articles/_/14905251/1 (show fewer)
Dataset

Cite this

Rubbens, R., Lathouwers, S., & Huisman, M. (2021). Modular Transformation of Java Exceptions Modulo Errors. In A. Lluch Lafuente, & A. Mavridou (Eds.), Formal Methods for Industrial Critical Systems: 26th International Conference, FMICS 2021, Paris, France, August 24–26, 2021, Proceedings (pp. 67-84). (Lecture notes in computer science; Vol. 12863). Springer. https://doi.org/10.1007/978-3-030-85248-1_5

Rubbens, Robert ; Lathouwers, Sophie ; Huisman, Marieke. / Modular Transformation of Java Exceptions Modulo Errors. Formal Methods for Industrial Critical Systems: 26th International Conference, FMICS 2021, Paris, France, August 24–26, 2021, Proceedings. editor / Alberto Lluch Lafuente ; Anastasia Mavridou. Springer, 2021. pp. 67-84 (Lecture notes in computer science).

@inbook{2eadd627fab3427e83f9a24b1f149a5f,

title = "Modular Transformation of Java Exceptions Modulo Errors",

abstract = "Deductive verifiers are used more and more in both academia and industry to prevent costly bugs. Their capabilities of verifying concurrent programs are getting better, but they are still lagging behind with regard to many major programming language features such as exceptions. To improve the situation, this work presents a semantics of Java exceptions which reduces the annotation burden on the user, while still allowing verification of exceptions. This is accomplished by ignoring sources of errors which are irrelevant to functional verification. Additionally, to deal with the complex control flow introduced by finally, a transformation is proposed that simplifies verification of exceptional postconditions and finally into postconditions and goto. We implement the approach and evaluate it against several common exception patterns.",

author = "Robert Rubbens and Sophie Lathouwers and Marieke Huisman",

note = "Publisher Copyright: {\textcopyright} 2021, Springer Nature Switzerland AG.; 26th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2021, FMICS 2021 ; Conference date: 24-08-2021 Through 26-08-2021",

year = "2021",

month = aug,

day = "19",

doi = "10.1007/978-3-030-85248-1_5",

language = "English",

isbn = "978-3-030-85247-4",

series = "Lecture notes in computer science",

publisher = "Springer",

pages = "67--84",

editor = "{Lluch Lafuente}, Alberto and Anastasia Mavridou",

booktitle = "Formal Methods for Industrial Critical Systems",

address = "Germany",

}

Rubbens, R, Lathouwers, S & Huisman, M 2021, Modular Transformation of Java Exceptions Modulo Errors. in A Lluch Lafuente & A Mavridou (eds), Formal Methods for Industrial Critical Systems: 26th International Conference, FMICS 2021, Paris, France, August 24–26, 2021, Proceedings. Lecture notes in computer science, vol. 12863, Springer, pp. 67-84, 26th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2021, Virtual Conference, 24/08/21. https://doi.org/10.1007/978-3-030-85248-1_5

Modular Transformation of Java Exceptions Modulo Errors. / Rubbens, Robert; Lathouwers, Sophie; Huisman, Marieke.
Formal Methods for Industrial Critical Systems: 26th International Conference, FMICS 2021, Paris, France, August 24–26, 2021, Proceedings. ed. / Alberto Lluch Lafuente; Anastasia Mavridou. Springer, 2021. p. 67-84 (Lecture notes in computer science; Vol. 12863).

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

TY - CHAP

T1 - Modular Transformation of Java Exceptions Modulo Errors

AU - Rubbens, Robert

AU - Lathouwers, Sophie

AU - Huisman, Marieke

N1 - Conference code: 26

PY - 2021/8/19

Y1 - 2021/8/19

N2 - Deductive verifiers are used more and more in both academia and industry to prevent costly bugs. Their capabilities of verifying concurrent programs are getting better, but they are still lagging behind with regard to many major programming language features such as exceptions. To improve the situation, this work presents a semantics of Java exceptions which reduces the annotation burden on the user, while still allowing verification of exceptions. This is accomplished by ignoring sources of errors which are irrelevant to functional verification. Additionally, to deal with the complex control flow introduced by finally, a transformation is proposed that simplifies verification of exceptional postconditions and finally into postconditions and goto. We implement the approach and evaluate it against several common exception patterns.

AB - Deductive verifiers are used more and more in both academia and industry to prevent costly bugs. Their capabilities of verifying concurrent programs are getting better, but they are still lagging behind with regard to many major programming language features such as exceptions. To improve the situation, this work presents a semantics of Java exceptions which reduces the annotation burden on the user, while still allowing verification of exceptions. This is accomplished by ignoring sources of errors which are irrelevant to functional verification. Additionally, to deal with the complex control flow introduced by finally, a transformation is proposed that simplifies verification of exceptional postconditions and finally into postconditions and goto. We implement the approach and evaluate it against several common exception patterns.

U2 - 10.1007/978-3-030-85248-1_5

DO - 10.1007/978-3-030-85248-1_5

M3 - Chapter

SN - 978-3-030-85247-4

T3 - Lecture notes in computer science

SP - 67

EP - 84

BT - Formal Methods for Industrial Critical Systems

A2 - Lluch Lafuente, Alberto

A2 - Mavridou, Anastasia

PB - Springer

T2 - 26th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2021

Y2 - 24 August 2021 through 26 August 2021

ER -

Rubbens R, Lathouwers S, Huisman M. Modular Transformation of Java Exceptions Modulo Errors. In Lluch Lafuente A, Mavridou A, editors, Formal Methods for Industrial Critical Systems: 26th International Conference, FMICS 2021, Paris, France, August 24–26, 2021, Proceedings. Springer. 2021. p. 67-84. (Lecture notes in computer science). doi: 10.1007/978-3-030-85248-1_5

Modular Transformation of Java Exceptions Modulo Errors

Abstract

Publication series

Conference

Access to Document

Fingerprint

Datasets

Data accompanied to the paper: Modular Transformation of Java Exceptions Modulo Errors

Cite this