32 citations · 82 across the 9 of their papers we have counts for
9 papers
Teaching Design by Contract using Snap!
Marieke Huisman, Raúl E. Monti
With the progress in deductive program verification research, new tools and techniques have become available to support design-by-contract reasoning about non-trivial programs writ…
VerifyThis 2019: A Program Verification Competition (Extended Report)
Claire Dross, Carlo A. Furia, Marieke Huisman +2
VerifyThis is a series of program verification competitions that emphasize the human aspect: participants tackle the verification of detailed behavioral properties -- something tha…
Formal Methods: From Academia to Industrial Practice. A Travel Guide
Marieke Huisman, Dilian Gurov, Alexander Malkis
For many decades, formal methods are considered to be the way forward to help the software industry to make more reliable and trustworthy software. However, despite this strong bel…
Verification of Shared-Reading Synchronisers
Afshin Amighi, Marieke Huisman, Stefan Blom
Synchronisation classes are an important building block for shared memory concurrent programs. Thus to reason about such programs, it is important to be able to verify the implemen…
Future-based Static Analysis of Message Passing Programs
Wytse Oortwijn, Stefan Blom, Marieke Huisman
Message passing is widely used in industry to develop programs consisting of several distributed communicating components. Developing functionally correct message passing software…
Permission-Based Separation Logic for Multithreaded Java Programs
Christian Haack, Marieke Huisman, Clément Hurlin +1
This paper presents a program logic for reasoning about multithreaded Java-like programs with dynamic thread creation, thread joining and reentrant object monitors. The logic is ba…
Verifying Parallel Loops with Separation Logic
Stefan Blom, Saeed Darabi, Marieke Huisman
This paper proposes a technique to specify and verify whether a loop can be parallelised. Our approach can be used as an additional step in a parallelising compiler to verify user…
Quantitative Security Analysis for Multi-threaded Programs
Tri Minh Ngo, Marieke Huisman
Quantitative theories of information flow give us an approach to relax the absolute confidentiality properties that are difficult to satisfy for many practical programs. The classi…
A History of BlockingQueues
Marina Zaharieva-Stojanovski, Marieke Huisman, Stefan Blom
This paper describes a way to formally specify the behaviour of concurrent data structures. When specifying concurrent data structures, the main challenge is to make specifications…