About me

Since January 2021 I joined ESI (TNO) in Eindhoven as a Research Fellow. There I work on methods and techniques for getting insight into the complex behaviours of industrial cyber-physical systems, and for understanding the impact of software changes on their system behaviour. We recently made a poster and corresponding video about part of our work.

Prior to that I worked at ETH Zurich as a postdoctoral researcher (2019—2020) at the Chair of Programming Methodology led by Peter Muller. At ETH I was involved in the VerifiedSCION project, in which we worked on the full-stack verification of the SCION routing protocol from the high-​​level design all the way down to the code implementation. In particular I was involved in developing the automated code verifier Gobra for the Go programming language—the implementation language of SCION—as well as techniques for proving properties of SCION and Go programs.

I did my PhD (2015—2019) at the University of Twente in the Formal Methods and Tools research group under supervision of Marieke Huisman. My PhD work investigates how (deductive) verification techniques for code implementations can be combined with (temporal) verification techniques for software designs, in such a way that they complement each other and benefit from each others results. During my PhD I visited the research group of Wolfgang Ahrendt at Chalmers University of Technology in Sweden, to investigate runtime verification of distributed (active) objects.

Research interests

I am interested in methods, techniques and tools for (formally) verifying and validating software-intensive systems, in a broad sense.

I like applying SAT and SMT solving, and automated and interactive theorem proving, for reasoning about algorithms, system/software designs and code implementations. For example I worked on and contributed to the code verifiers Gobra, VerCors and Viper, which translate the problem of establishing program correctness to proof obligations that are ultimately discharged to SMT solvers.

I am particularly interested in combining different specification formalisms and verification techniques (like program logics and model checking) in complementary ways, so that they benefit from each others results. Additionally I am looking into how verification can neatly be integrated in the complete development process of software-intensive systems, in order to increase their effectivity. The different design and engineering phases of system development should go hand-in-hand with their gradual verification, as should the evolution of the system.

Publications

Poster presentations

Theses

Supervised student projects

Academic service

  • Organisation: FTfJP 2020 (Chair), VerifyThis 2020/2021 (Co-​organiser).
  • Program committees: FMICS 2022, TACAS 2021 (AEC), WADT 2020, TACAS 2019 (AEC), OOPSLA 2019 (AEC).
  • External reviewer: VMCAI 2021, Mathematics 2020, SEFM 2020, VMCAI 2020, RV 2019, SEFM 2019, CONCUR 2019, FASE 2019, FoSSaCS 2019, FM 2018, TACAS 2018, CPP 2017, ESSoS 2016, FTSCS 2016, iFM 2016, FASE 2016.

Other accomplishments

  • Won the VerifyThis best student team award at ETAPS 2019, together with Sophie Lathouwers.
  • Won the VerifyThis student team—silver award at ETAPS 2018, together with Mohsen Safari.
  • Received my BSc degree Cum Laude in 2012 at Windesheim University of Applied Sciences, and managed to finish the four-​year computer science programme within three years.

Software

  • TectonicGenerator: Algorithms for generating Tectonic puzzles of various sizes and varying complexity, written as a small hobby project. The algorithms and their implementation are closed source for now, but some generated puzzles can be played here.
  • Gobra: A modular automated code verifier for programs written in Go.
  • VerCors: An automated and modular verifier that targets concurrent programs written in Java, C, OpenCL and OpenMP.
  • DistBDD: A distributed symbolic reachability analysis implementation for high-performance networks of multi-core machines.

Contact

Email: wytseoortwijn at gmail dot com.