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.
News
EATCS Presburger Award 2017 for Alexandra Silva
The 2017 Presburger Committee has unanimously selected Alexandra Silva, a Senior Lecturer at University College London as recipient of the prestigious 2017 EATCS Presburger Award for young scientists. She received the award for a large part of her PhD research, which she carried out in the Formal Methods research group at Centrum Wiskunde & Informatica (CWI) in Amsterdam.
Farhad Arbab honoured by Sharif University of Technology
CWI researcher Farhad Arbab was honoured by Sharif University of Technology in Iran as one of its fifty most outstanding alumni over the past fifty years. The alumni were selected for both their technical achievements and service to the society.
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.
FACS Best Paper Award for Formal Methods researchers
During the FACS2015 conference three researchers associated with the CWI Formal Methods research group were awarded the Best Paper Award for their article ‘Composing Constraint Automata, State-by-State’. The conference was held in Niterói, Brazil, from 14-16 October 2015.
Members
Associated Members
Publications
-
Hiep, H.A, Maathuis, O, Bian, J, de Boer, F.S, van Eekelen, M, & de Gouw, C.P.T. (2020). Verifying OpenJDK's LinkedList using KeY. Lecture Notes in Computer Science.
-
Azadbakht, K. (2019, December 11). Asynchronous programming in the abstract behavioural specification language.
-
de Boer, F.S, & Hiep, H.A. (2019). Axiomatic characterization of trace reachability for concurrent objects. In Proceedings of the 15th International Conference on integrated Formal Methods (pp. 157–174). doi:10.1007/978-3-030-34968-4_9
-
Esterhuyse, C.A, & Hiep, H.A. (2019). Reowolf: Synchronous multi-party communication over the Internet?. In Proceedings of the 16th International Conference on Formal Aspects of Component Software. doi:10.1007/978-3-030-40914-2_12
-
Kappé, T.W.J, Lion, B, Arbab, F, & Talcott, C. (2019). Soft component automata: Composition, compilation, logic, and verification. Science of Computer Programming, 183. doi:10.1016/j.scico.2019.08.001
-
Bezirgiannis, N, de Boer, F.S, Johnsen, E.B, Pun, K.I, & Tapia Tarifa, S.L. (2019). Implementing SOS with active objects: A case study of a multicore memory system. In FASE 2019: Fundamental Approaches to Software Engineering (pp. 332–350). doi:10.1007/978-3-030-16722-6_20
-
Rutten, J.J.M.M. (2019). The Method of Coalgebra: exercises in coinduction. CWI, Amsterdam, The Netherlands.
-
Serbanescu, V.N, de Boer, F.S, & Jaghouri, M.M. (2018). ASCOOP: Actors in scala with cooperative scheduling. In 21st IEEE International Conference on Computational Science and Engineering, CSE 2018 (pp. 19–28). doi:10.1109/CSE.2018.00010
-
Lion, B, Chouali, S, & Arbab, F. (2018). Compiling protocols to Promela and verifying their LTL properties. In Proceedings of 21st MODELS Workshops 2018: Copenhagen, Denmark (pp. 31–39).
-
Serbanescu, V.N, de Boer, F.S, & Jaghouri, M.M. (2018). Actors with coroutine support in Java. In Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence (pp. 237–255). doi:10.1007/978-3-030-02146-7_12
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)
-
Reowolf
Related partners
-
Anchormen
-
Vitens
-
Stichting NLnethttps://nlnet.nl/contact/address.html