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.


Better QoS for distributed software with stochastic and formal methods

Better QoS for distributed software with stochastic and formal methods

Reusability of software is a hot topic nowadays. It is easier, cheaper and more efficient to reuse parts of existing software in order to adjust or incorporate new functionalities, than to design completely new programs. However, due to the different sources and constraints of software components, it is not easy to define the Quality of Service (QoS) for newly composed software, especially when it consists of components or services provided by various geographically distributed organizations. Young-Joo Moon, PhD student at the Centrum Wiskunde & Informatica (CWI) in Amsterdam, developed a stochastic formal model to derive the end-to-end QoS of such software systems.

Better QoS for distributed software with stochastic and formal methods - 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

PhD defence Julian Salamance (FM)

  • 2018-04-24T16:30:00+02:00
  • 2018-04-24T18:00:00+02:00
April 24 Tuesday

Start: 2018-04-24 16:30:00+02:00 End: 2018-04-24 18:00:00+02:00

Radboud Universiteit, Academiezaal, Aula, Comeniuslaan 2, Nijmegen

Everyone is welcome to attend the public defence of Julian Salamanca, of his thesis 'Coequations and Eilenberg-type Correspondences'

Promotor: Prof.dr. J.J.M.M. (Jan) Rutten

Co-promotor: Dr. M.M. (Marcello) Bonsangue


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