Leader of the group Formal Methods: Frank de Boer.

In the Formal Methods group, our research involves finding solutions to highly pragmatic real-world problems by reducing their complexity through the elegance and beauty of mathematics. We formulate problems to reveal their complexity and make them amenable to elegant solutions.

Our work yields technological foundations that underpin software engineering and service-oriented computing. With everything we do, we aim to add stability and reliability to those foundations and so to the third-party applications built on them. In this way, we cut the costs of technological failure for business and society and make life easier for programmers, developers and ultimately users.

Our no-nonsense approach relies on the smooth transfer of knowledge between senior and junior researchers, reaching back through our rich history as one of CWI’s original research groups. Our work is grounded in our collaborations with partners in business and industry.




Cum laude for new method making parallel programming easier

Cum laude for new method making parallel programming easier

Due to the increase of multicore processors used in smart phones, game consoles and other computers, parallel programming has become increasingly important. To prevent software errors, concurrent calculations must always exactly be executed in the correct order. This is not easy, because existing programming techniques for enforcing such orders - interaction protocols - are very hard to use. PhD student Sung-Shik Jongmans of Centrum Wiskunde & Informatica and Leiden University investigated a new programming method to simplify this.

Cum laude for new method making parallel programming easier - Read More…


CWI Lecture Professor Marta Kwiatkowska (University of Oxford)

  • 2017-06-09T11:00:00+02:00
  • 2017-06-09T12:00:00+02:00
June 9 Friday

Start: 2017-06-09 11:00:00+02:00 End: 2017-06-09 12:00:00+02:00

Room L120 at CWI, Science Park 123 in Amsterdam

Everyone is welcome to attend the CWI lecture given by Marta Kwiatkowska.

Prof.dr  Jos Baeten Prof.dr. Jan Rutten

Safety Verification of Deep Neural Networks
Marta Kwiatkowska
University of Oxford

Deep neural networks have achieved impressive experimental results in image classification, but can surprisingly be unstable with respect to adversarial perturbations, that is, minimal changes to the input image that cause the net-work to misclassify it. With potential applications including perception modules and end-to-end controllers for self-driving cars, this raises concerns about their safety. We develop a novel automated verification framework for feed-forward multi-layer neural networks based on Satisfiability Modulo Theory (SMT). We focus on image manipulations, such as scratches or changes to camera angle or lighting conditions, and define safety for an image classification decision in terms of invariance of the classification with respect to manipulations of the original image within a region of images that are close to it. We enable exhaustive search of the region by employing discretisation, and propagate the analysis layer by layer. Our method works directly with the network code and, in contrast to existing methods, can guarantee that adversarial examples, if they exist, are found for the given region and family of manipulations. If found, adversarial examples can be shown to human testers and/or used to fine-tune the network. We implement the techniques using Z3 and evaluate them on state-of-the-art networks, including regularised and deep learning networks. We also compare against existing techniques to search for adversarial examples and estimate network robustness.

Marta Kwiatkowska is Professor of Computing Systems and Fellow of Trinity College, University of Oxford. She led the development of the PRISM model checker (, the leading software tool in the area and winner of the HVC Award 2016. Applications of probabilistic model checking have spanned communication and security protocols, nanotechnology designs, power management, game theory, planning and systems biology, with genuine flaws found and corrected in real-world protocols. Kwiatkowska gave the Milner Lecture in 2012 in recognition of "excellent and original theoretical work which has a perceived significance for practical computing" and was awarded an honorary doctorate from KTH Royal Institute of Technology in Stockholm in 2014. Her research has been supported by the ERC Advanced Grant VERIWARE "From software verification to everyware verification" and the EPSRC Programme Grant on Mobile Autonomy. She is a Fellow of ACM, Member of Academia Europea and Fellow of EATCS.

PhD Defence Sung-Shik T.Q. Jongmans (FM)

  • 2016-03-03T14:00:00+01:00
  • 2016-03-03T16:00:00+01:00
March 3 Thursday

Start: 2016-03-03 14:00:00+01:00 End: 2016-03-03 16:00:00+01:00

Academiegebouw, Rapenburg 67-73 te Leiden

Everybody is welcome to attend the public defense of Sung-Shik Jongmans of his thesis 'Automata-Theoretic Protocol Programming'.

Promotor: Prof.dr. Farhad Arbab

Members of Formal Methods



Current Projects

  • Detection and Diagnosis of Deviations in Distributed Systems of Autonomous Agents
  • EcoPro
    Enhancing eciency and expressiveness of the coinduction proof method


  • SRI International, Menlo Park, California, USA