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.




PhD Student on the subject of Verification of Mainstream Java Libraries

The overall objective of this PhD position is the development and application of formal methods to actual software. Of particular interest are the mainstream libraries of the popular programming language Java. These libraries are widely used and therefore their correctness is of the utmost importance. This research builds on and extends the successful verification by means of the interactive theorem prover KeY of executable Java versions of Counting sort and Radix sort. A recent attempt to verify the Java implementation of the TimSort hybrid sorting algorithm as provided by the Java Collections Framework (and which is designed to perform well on real world data) revealed a fundamental error which for certain inputs crashed the software. In close collaboration with the Software Engineering group of TU Darmstadt, we succeeded in the verification of the corrected software. Motivated by this success our overall goal is the systematic verification of the Java Collections Framework.


Commit2Data grant for better, faster and real-time adaptable big data analysis

Commit2Data grant for better, faster and real-time adaptable big data analysis

To improve parallel processing of big data, NWO granted the project ‘Evolutionary changes in Distributed Analysis’ (ECiDA) within their Commit2Data programme. The research partners in this project – CWI being one of them – will develop a platform to support 'evolving data-intensive application pipelines’, making big data analysis safer, better, faster and adaptable in real-time.

Commit2Data grant for better, faster and real-time adaptable big data analysis - Read More…

Best Paper Award for Training DevOps engineers

Best Paper Award for Training DevOps engineers

Researchers from CWI's Formal Methods group won the Best Paper Award in the 6th European Conference on Service-Oriented and Cloud Computing (ESSOC) in September 2017. They were awarded the prize for their work on 'Human-in-the-Loop Simulation of Cloud Services'. The researchers are one of the first to carry out live, interactive simulation of DevOps engineers inside simulated cloud environments.

Best Paper Award for Training DevOps engineers - Read More…

Current events

CWI symposium 'It's All About Coordination' in honour of Prof.dr. Farhad Arbab

  • 2018-05-25T13:00:00+02:00
  • 2018-05-25T18:30:00+02:00
May 25 Friday

Start: 2018-05-25 13:00:00+02:00 End: 2018-05-25 18:30:00+02:00

WCW Congress Center, Turing room, Science Park 123, Amsterdam

Dear colleagues,

On Friday afternoon 25 May CWI will organize a farewell symposium on the occasion of   
the retirement of prof.dr. Farhad Arbab.
You are cordially invited to attend this special event.

The program, entitled 'It's All About Coordination' is as follows:

13.00 - 13.30  Welcome with coffee/thee
13.30 - 13.45  Musical interlude by Rouzbeh Motia
13.45 - 15.15  Scientific presentations:
                         Carolyn Talcott: From Soft Agents to Soft Component Automata and Back
                         Marjan Sirjani  : Reo and Tagged Signal Models, Challenge of Constraints
                         Krzysztof Apt    : Self-Stabilization Through the Lens of Game Theory
15.15 - 15.45  Koffie/thee break
15.45 - 16.00  Musical interlude by Rouzbeh Motia
16.00 - 17.00  Personal communications by
                         Kasper Dokter          : The Art of Storytelling
                         Sun Meng                  : Tons of Fun in a Zodiac Cycle
                         Sungshik Jongmans : The (Dis)likes of Farhad
17.00 - 17.30  Closing

Afterwards there will be a reception.

Location: Turing room, CWI, Science Park 123, Amsterdam.

There is no fee for attending this event, but registration is highly recommended
for planning purposes.
Please confirm your participation, by registering here.

We hope to welcome you on this very special afternoon at CWI.

On behalf of the organizing committee,
Frank de Boer


Associated Members



Current projects with external funding

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

Related partners

  • SRI International, Menlo Park, California, USA