Wytse Oortwijn

Since August 2015 I am a PhD candidate at the Formal Methods and Tools (FMT) research group at the University of Twente in Enschede, the Netherlands. My main research is focused on program logics, in particular separation logics, as well as program abstractions, process algebras, theorem proving, and high-performance, parallel and distributed (symbolic) model checking. I am currently working on verifying distributed software using both deductive and algorithmic reasoning. My Master's thesis, named Distributed Symbolic Reachability Analysis focuses more on high-performance model checking and can be found here. My curriculum vitae can be found here, last updated on September 2017.

Publications

• Stefan Blom, Saeed Darabi, Marieke Huisman, and Wytse Oortwijn. The VerCors Tool Set: Verification of Parallel and Concurrent Software, iFM, September 2017.
• Wytse Oortwijn, Stefan Blom, Dilian Gurov, Marieke Huisman, and Marina Zaharieva-Stojanovski. An Abstraction Technique for Describing Concurrent Program Behaviour, VSTTE, July 2017 (to appear).
• Wytse Oortwijn, Tom van Dijk, and Jaco van de Pol. Distributed Binary Decision Diagrams for Symbolic Reachability, SPIN, July 2017. Best paper award.
• Wytse Oortwijn and Marieke Huisman. Model-based Verification of Distributed Software, SEN symposium, February 2017.
• Wytse Oortwijn, Stefan Blom, and Marieke Huisman. Future-based Static Analysis of Message Passing Programs, PLACES 2016.
• Wytse Oortwijn, Stefan Blom, and Marieke Huisman. Static Verification of Message Passing Programs, ICTOpen 2016. Best IPA poster award. The poster is available here.
• Wytse Oortwijn, Tom van Dijk, and Jaco van de Pol. A Distributed Hash Table for Shared Memory, PPAM 2015. The GitHub page is available here.

Given talks

• The VerCors Tool Set - Verification of Parallel and Concurrent Software. Integrated Formal Methods (iFM) 2017, University of Torino, Turin, Italy, September 2017. (Slides)
• An Abstraction Technique for Describing Concurrent Program Behaviour. PhD Symposium - iFM 2017, University of Torino, Turin, Italy, September 2017. (Slides)
• The VerCors Tool Set - Verification of Parallel and Concurrent Software. Lunchmeeting FMT, University of Twente, Enschede, the Netherlands, September 2017. (Slides)
• An Abstraction Technique for Describing Concurrent Program Behaviour. VSTTE, Heidelberg, Germany, July 2017. (Slides)
• The VerCors Toolset: Verifying Parallel, Concurrent, and Distributed Software. Lunchmeeting, Delft University, the Netherlands, June 2017. (Slides)
• Verifying Concurrent and Distributed Software. SEN Symposium, CWI Amsterdam, the Netherlands, January 2017. (Slides)
• Verifying Concurrent Software. Lunchmeeting FMT, University of Twente, the Netherlands, December 2016. (Slides)
• Distributed Binary Decision Diagrams for Symbolic Reachability. Dutch Model Checking Day (DMCD), University of Twente, July 2016. (Slides)
• Static Analysis of Message Passing Programs. Dagstuhl seminar, Wadern, Germany, May 2016. (Slides)
• Future-based Static Analysis of Message Passing Programs. PLACES, Eindhoven University, the Netherlands, April 2016. (Slides)
• Static Verification of Message Passing Programs. ICT.Open, Amersfoort, the Netherlands, March 2016. (Slides)
• Distributed Binary Decision Diagrams for Symbolic Reachability. IPA Fall Days, Herten-Roermond, the Netherlands, November 2015. (Slides)
• A Distributed Hash Table for Shared Memory. PPAM, Krakow, Poland, September 2015.
• Distributed Symbolic Reachability Analysis. Lunchmeeting FMT, University of Twente, the Netherlands, July 2015. (Slides)

Theses

• Distributed Symbolic Reachability Analysis, Master's thesis, July 2015. The corresponding GitHub page is available here (SPIN2017 version).

Accomplishments

• I received my Master's degree with Honours, as result of attending the Master's Honours Research programme in addition to the regular Master's programme, named Methods and Tools for Verification (MTV). The topics of the MTV programme include: model checking, logic, static verification (model checking, deductive verification), dynamic (runtime) verification, and (model-based) testing.
• I received my Bachelor's degree Cum Laude in 2012, on Windesheim, University of applied sciences, and managed to finish the four-year programme within three years.

Supervised students

• Janina Torbecke, Symbolic Model Checking with Partitioned BDDs in Distributed Systems, Master's thesis, September 2017 (ongoing).
• Jelte Zeilstra, A logic to reason about distributed programs, Master's thesis, November 2016.
• Willem Siers, Correct and Efficient Concurrent Hash Tables in Java, Bachelor's thesis, July 2016.

Tools

• DistBDD - a distributed symbolic reachability analysis implementation for high-performance networks of multi-core machines.
• VerCors Verification Toolset - a toolset for verifying parallel and concurrent software (written in Java, C, OpenMP, or OpenCL). Some documentation can be found here. A detailed list of verified examples can be found here. Try VerCors online here.

Contact

University of Twente,
Drienerlolaan 5, 7522 NB, Enschede.

Room: Zi-3082 (Zilvering building, click here).
Email: w.h.m.oortwijn at utwente dot nl.