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.
|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|
|Number of pages||18|
|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
|Name||Lecture notes in computer science|
|Conference||26th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2021|
|Abbreviated title||FMICS 2021|
|Period||24/08/21 → 26/08/21|
FingerprintDive into the research topics of 'Modular Transformation of Java Exceptions Modulo Errors'. Together they form a unique fingerprint.