Description
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.
Vacancies
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.
News

Fewer errors in software features by using delta modelling
When new features are being written into software code, errors can easily be made. This is due to the fact that feature code often interacts in many different places in the software.

CWI and SDL join forces to improve cloud-based marketing
Centrum Wiskunde & Informatica (CWI) and SDL recently started a public-private partnership project to improve cloud-based software for marketing purposes. In this joint project both CWI and SDL contribute to the research budget.

New technique detects bugs in object-oriented languages
CWI researcher Stijn de Gouw has developed a new technique for the detection of bugs in software written in object-oriented languages like Java. In a first test case, the technique was able to determine the correctness of complex software of marketing software company SDL Fredhopper.
CWI joins Sino-European research network LIAMA
Centrum Wiskunde & Informatica (CWI) has officially joined research network LIAMA. The Sino-European Laboratory in Computer Science, Automation and Applied Mathematics (LIAMA) is a research lab consisting of European and Chinese research institutes in the field of mathematics and computer science. LIAMA conducts research, training and transfer projects in these fields. CWI will join the lab as one of the founding members.
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
CWI symposium 'It's All About Coordination' in honour of Prof.dr. Farhad Arbab
Start: 2018-05-25 13:00:00+02:00 End: 2018-05-25 18:30:00+02:00
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
Members
Associated Members
Publications
-
Salamanca Tellez, J.R. (2018, April 24). Coequations and Eilenberg-type Correspondences (No. 2018-3). Institute for Programming research and Algorithmics Dissertation Series.
-
Bezirgiannis, N. (2018, April 17). Abstract behavioral specification: unifying modeling and programming. Institute for Programming research and Algorithmics Dissertation Series.
-
de Boer, F.S, Bravetti, M, Lee, M.D, & Zavattaro, G. (2018). A Petri net based modeling of active objects and futures. Fundamenta Informaticae, 159(3), 197–256. doi:10.3233/FI-2018-1663
-
de Boer, F.S, Serbanescu, V.N, Hähnle, R, Henrio, L, Rochas, J, Din, C.C, … Yang, A.M. (2017). A survey of active object languages. ACM Computing Surveys, 50(5). doi:10.1145/3122848
-
Jongmans, S.-S.T.Q, Kappé, T.W.J, & Arbab, F. (2017). Constraint automata with memory cells and their composition. Science of Computer Programming, 146, 50–86. doi:10.1016/j.scico.2017.03.006
-
Dokter, K.P.C, & Arbab, F. (2017). Exposing latent mutual exclusion by work automata. In Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence (pp. 59–73). doi:10.1007/978-3-319-68953-1_6
-
Basold, H, Hansen, H.H, Pin, J.-É, & Rutten, J.J.M.M. (2017). Newton series, coinductively: a comparative study of composition. Mathematical Structures in Computer Science. doi:10.1017/S0960129517000159
-
Azadbakht, K, Bezirgiannis, N, & de Boer, F.S. (2017). Distributed network generation based on preferential attachment in ABS. In Proceedings of 43rd International Conference on Current Trends in Theory and Practice of Computer Science (pp. 103–115). doi:10.1007/978-3-319-51963-0_9
-
Rutten, J.J.M.M. (2017, January). Newton series coinductively, a comparative study of composition.
-
Kappé, T.W.J, Arbab, F, & Talcott, C. (2016). A compositional framework for preference-aware agents. In Electronic Proceedings in Theoretical Computer Science (pp. 21–36). doi:10.4204/EPTCS.232.6
Software
Extensible Coordination Tools: plug-ins for the Eclipse platform
ECT: The Extensible Coordination Tools consist of a set of plug-ins for the Eclipse platform to facilitate development of concurrency protocols and distributed applications based on the coordination language Reo.
SAGA: A run-time verifier for Java programs
SAGA is a run-time verifier for single-threaded as well as multi-threaded Java programs.
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