Marieke Huisman

Assertion Monitoring in Concurrent Software

Checking whether a program respects the assertions can be done in different ways. In the research community, much attention is given to static checking. However, it is also possible to check adherence to the specifications during program execution. This is usually known as run-time assertion checking or monitoring. For sequential programs, several tools exist that have been succesfully used for run-time assertion checking. However, building a run-time assertion checker for concurrent programs is more challenging.

In this presentation we will first describe the challenges and potential problems for developing run-time assertion checking techniques for concurrent software, and then we will outline our solution. This solution is based on an extension of the STROBE framework, which is used to create snapshots of the states in which assertions should be checked. These checks are then executed by the OpenJML framework, one of the standard run-time assertion checking tools for sequential Java programs. In the future we plan to extend this work with additional control of the scheduler, which will allow one to investigate different executions of the program.

Dr. Marieke Huisman is an Associate Professor working in the Formal Methods and Tools group at the University of Twente. Huisman is a well-established researcher in the area of program verification. She obtained her PhD in 2001 from the University of Nijmegen, Netherlands. Her thesis was about the semantics and verification of sequential Java programs. In 2010 she received a personal ERC Starting Grant for the VerCors project on Verification of Concurrent Data Structures. In 2013 she received the Dutch ICT Research award, a unique prize for a scientist, aged 40 years or younger, who carries out innovative research or is responsible for a scientific breakthrough in ICT.