University of Twente Student Theses
Improving Support for Java Exceptions and Inheritance in VerCors
Rubbens, R.B. (2020) Improving Support for Java Exceptions and Inheritance in VerCors.
|
PDF
506kB |
| Abstract: | In the age where one software bug can cost millions, software correctness is paramount. Static verifiers are used more and more in both academia and industry to prevent these costly bugs. They can formally prove that an implementation adheres to a specification. With the recent increased use of concurrency, proving correctness of software has become more challenging. However, progress is being made in this area: several static verifiers can now also verify languages in concurrent environments. Unfortunately their features are lagging behind: most checkers do not proceed beyond the prototyping phase and do not tackle the more practical language features. To improve the situation, this work presents an approach for implementing verification support for exceptions and inheritance as presented in Java. We also present, in great detail, the transformation of a language with exceptions and inheritance into a language without, and discuss the theory underlying the practical support for exceptions and inheritance. Finally, we briefly evaluate the approaches for both exceptions and inheritance, and discuss what can be further improved in static verification. |
| Item Type: | Essay (Master) |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 54 computer science |
| Programme: | Computer Science MSc (60300) |
| Link to this item: | https://purl.utwente.nl/essays/81338 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page