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 development of dynamic data analysis pipelines on distributed data clusters
The Formal Methods group at CWI has an open positions for a PhD student to work in the project Evolutionary changes in Distributed Analysis (ECiDA). This project involves development of dynamic data analysis pipelines on distributed data clusters.
News
Java Bug Fixed with Formal Methods CWI
Researchers from CWI fixed a bug in the widely used object-oriented programming language Java in February 2015. They found an error in a broadly applied sorting algorithm, TimSort, which could crash programs.
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.
Members
Associated Members
Publications
-
Azadbakht, K, de Boer, F.S, & de Vink, E.P. (2018). Deadlock detection for actor-based coroutines. In Proceedings of the International symposium on Formal Methods (pp. 39–54). doi:10.1007/978-3-319-95582-7_3
-
Groenewegen, L.P.J, Verschuren, J.H.S, de Vink, E.P, & Rutten, J.J.M.M. (2018). Extending paradigm with data. In F.S de Boer & M.M Bonsangue (Eds.), It's All About Coordination. Essays to Celebrate the Lifelong Scientific Achievements of Farhad Arbab (pp. 224–244). doi:10.1007/978-3-319-90089-6_15
-
Bonsangue, M.M, & Rutten, J.J.M.M. (2018). It's All About Coordination. Essays to Celebrate the Lifelong Scientific Achievements of Farhad Arbab. (F.S de Boer, Ed.)Lecture Notes in Computer Science. doi:10.1007/978-3-319-90089-6
-
Blom, C.L. (2018). Personal note: Working with Farhad Arbab 1990–2005. In F.S de Boer, M.M Bonsangue, & J.J.M.M Rutten (Eds.), It's All About Coordination. Essays to Celebrate the Lifelong Scientific Achievements of Farhad Arbab (pp. 68–69). doi:10.1007/978-3-319-90089-6_5
-
Dokter, K.P.C, & Arbab, F. (2018). Rule-based form for stream constraints. In Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence. doi:10.1007/978-3-319-92408-3_6
-
Kappé, T.W.J, Arbab, F, & Talcott, C. (2017). A component-oriented framework for autonomous agents. In Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence (pp. 20–38). doi:10.1007/978-3-319-68034-7_2
-
Bezirgiannis, N, de Boer, F.S, & de Gouw, C.P.T. (2017). Human-in-the-loop simulation of Cloud services. In Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence (pp. 143–158). doi:10.1007/978-3-319-67262-5_11
-
Azadbakht, K, Bezirgiannis, N, & de Boer, F.S. (2017). On futures for streaming data in abs. In Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence (pp. 67–73). doi:10.1007/978-3-319-60225-7_5
-
Hansen, H.H, Kupke, C.A, & Rutten, J.J.M.M. (2017). Stream differential equations: Specification formats and solution methods. Logical Methods in Computer Science, 13(1), 1–51. doi:10.23638/LMCS-13(1:3)2017
-
Rutten, J.J.M.M. (2017, January). A new proof by coinduction of Moessner's theorem.
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
-
Evolutionary changes in Distributed Analysis (ECiDA)
-
Enhancing efficiency and expressiveness of the coinduction proof method (EcoPro)
Related partners
-
Anchormen
-
Vitens