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
TCS journal honours Jan Rutten
Jan Rutten from CWI’s Formal Methods research group was recently awarded by the journal Theoretical Computer Science (TCS) for his much cited article Universal Coalgebra – a theory of systems, on the occasion of the journal’s 40th anniversary.
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.
Current events
16th International Conference on Formal Aspects of Component Software (FACS 2019)
- 2019-10-23T09:00:00+02:00
- 2019-10-25T17:00:00+02:00
16th International Conference on Formal Aspects of Component Software (FACS 2019)
Start: 2019-10-23 09:00:00+02:00 End: 2019-10-25 17:00:00+02:00
Call for Papers: FACS 2019
FACS 2019 is concerned with how formal methods can be applied to component-based software and system development. Formal methods have provided foundations for component-based software through research on mathematical models for components, composition and adaptation, and rigorous approaches to verification, deployment, testing, and certification.
Component-based software development proposes sound engineering principles and techniques to cope with the complexity of present-day software systems. However, many challenging conceptual and technological issues remain in component-based software development theory and practice. Furthermore, the advent of service-oriented and cloud computing, cyber-physical systems, and the Internet of Things has brought to the fore new dimensions, such as quality of service and robustness to withstand faults, which require revisiting established concepts and developing new ones.
Invited speakers:
- Wan Fokkink (Professor of Theoretical Computer Science, Vrije Universiteit Amsterdam)
- Carlo Ghezzi (Professor of Software Engineering, Polytechnic University of Milan)
- Kim Larsen (Professor of Computer Science, Aalborg University)
- Web
- Email: Sung-Shik Jongmans
- Phone: see website
-
iCal
Members
Associated Members
Publications
-
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
-
de Boer, F.S, Giachino, E, de Gouw, C.P.T, Hähnle, R, Johnsen, E.B, Laneve, C, … Zavattaro, G. (2018). Analysis of SLA compliance in the cloud: An automated, model-based approach. In Electronic Proceedings in Theoretical Computer Science, EPTCS (pp. 1–15). doi:10.4204/EPTCS.302.1
-
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
-
Endrullis, J, Klop, J.W, & Overbeek, R. (2018). Decreasing diagrams with two labels are complete for confluence of countable systems. In Proceedings of the Third International Conference on Formal Structures for Computation and Deduction (pp. 14:1–14:15). doi:10.4230/LIPIcs.FSCD.2018.14
-
Dokter, K.P.C, & Arbab, F. (2018). Treo: Textual syntax for Reo connectors. In Electronic Proceedings in Theoretical Computer Science, EPTCS (pp. 121–135). doi:10.4204/EPTCS.272.10
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