IdentityHashMap

De paper is gebaseerd op de masterscriptie van Martin de Boer, die inmiddels is afgestudeerd aan de Open Universiteit. De Gouw, de Boer en de Duitse onderzoekers onderzochten de correctheid van een stukje software, de zogenaamde IdentityHashMap. De software maakt onderdeel uit van het veelgebruikte Java Collection Framework uit de programmeertaal Java - Java en dit framework wordt bijvoorbeeld op alle Android telefoons gebruikt.

Software toetsen

De Gouw en de Boer schreven formele specificaties die het gewenste gedrag van de IdentityHashMap omschrijven. Vervolgens hebben ze de onderliggende code van de sotfware getoetst aan een wiskundig bewijsprogramma. Ze vonden daadwerkelijk enkele problemen in de code. Voor het schrijven van de specificaties maakten ze gebruik van zogenaamde testing en model checking technieken, waardoor ze het schrijfproces op een slimme en innovatieve manier konden versnellen.

Stijn de Gouw

Stijn de Gouw is als universitair docent verbonden aan de vakgroep informatica van de faculteit Bètawetenschappen van de Open Universiteit. Martin de Boer, Stijn de Gouw, Jonas Klamroth, Christian Jung, Mattias Ulbrich & Alexander Weigl (2022). Formal Specification and Verification of JDK’s Identity Hash Map Implementation. iFM 2022: Integrated Formal Methods, pp 45–62.