5 citations · 6 across the 2 of their papers we have counts for
4 papers
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit
Tobias Reinhard, Amin Timany, Bart Jacobs
Programs for multiprocessor machines commonly perform busy-waiting for synchronisation. In this paper, we make a first step towards proving termination of such programs. We approxi…
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report
Tobias Reinhard, Amin Timany, Bart Jacobs
Programs for multiprocessor machines commonly perform busy-waiting for synchronisation. In this paper, we make a first step towards proving termination of such programs. We approxi…
Abstract I/O Specification
Willem Penninckx, Amin Timany, Bart Jacobs
We recently proposed an approach for the specification and modular formal verification of the interactive (I/O) behavior of programs, based on an embedding of Petri nets into separ…
Category Theory in Coq 8.5
Amin Timany, Bart Jacobs
We report on our experience implementing category theory in Coq 8.5. The repository of this development can be found at https://bitbucket.org/amintimany/categories/. This implement…