Modular Transformation of Java Exceptions Modulo Errors

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

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 languageEnglish
Title of host publicationFormal Methods for Industrial Critical Systems
Subtitle of host publication26th International Conference, FMICS 2021, Paris, France, August 24–26, 2021, Proceedings
EditorsAlberto Lluch Lafuente, Anastasia Mavridou
PublisherSpringer
Pages67-84
Number of pages18
ISBN (Electronic)978-3-030-85248-1
ISBN (Print)978-3-030-85247-4
DOIs
Publication statusPublished - 2021
Event26th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2021 - Virtual Conference
Duration: 24 Aug 202126 Aug 2021
Conference number: 26

Publication series

NameLecture notes in computer science
Volume12863

Conference

Conference26th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2021
Abbreviated titleFMICS 2021
CityVirtual Conference
Period24/08/2126/08/21

Fingerprint

Dive into the research topics of 'Modular Transformation of Java Exceptions Modulo Errors'. Together they form a unique fingerprint.

Cite this