Welcome to the home page of Frank S. de Boer

Senior researcher and leader of the research group Formal Methods, CWI
Professor Program Correctness at the Leiden Institute of Advanced Computer Science.



Contact information

Centrum voor Wiskunde en Informatica (CWI)
Department of Software Engineering
Kruislaan 413
P.O. Box 94079
1090 GB Amsterdam
The Netherlands
Phone (direct): 020 592 4139 (international: +31 20 592 4139)
Phone (secretary Susanne van Dam): 020 592 4189 (international: +31 20 592 4189)
Fax: 020 592 4199 (international: +31 20 592 4199)
Email: F.S.de.Boer at cwi.nl

Research profile

As a logician I have worked on the development and formal justification of programming logics. In my thesis (1991) reasoning about dynamically evolving process structures (A proof theory of the parallel object-oriented language POOL) I developed a first sound and complete proof method for a (parallel) object-oriented language, designed and implemented at Philips Research Laboratories. Further development has resulted in a comprehensive proof-theory of a variety of object-oriented features and mechanisms like object creation, aliasing, method calls, multi-threading, inheritance and subtyping.
In general I have worked on formal methods. I am a coauthor of the books

                           
My other publications can be found at DBLP Bibliography Server and my Google Scholar profile. For my research on programming languages for multi-agent systems I also refer to my publications stored by the Intelligent Systems group at the department of Information and Computing Sciences of Utrecht University).
Here you can find some selected publications.

Object-Orientation

  1. Verification of object-oriented programs: A transformational approach
  2. A WP-calculus for OO
  3. Abstract Object Creation in Dynamic Logic: To Be or Not to Be Created
  4. Automated Verification of Recursive Programs with Pointers
  5. Reasoning about dynamically evolving process structures
  6. Verification for Java's Rentrant Multithreading Concept
  7. Automated Deadlock Detection in Synchronized Reentrant Multithreaded Call-Graph
  8. A Syntax-Directed Hoare Logic for Object-Oriented Programming Concepts
  9. Formalizing UML Models and OCL Constraints in PVS
  10. Schedulability of asynchronous real-time concurrent objects
  11. User-defined schedulers for real-time concurrent objects
  12. Programming and Deployment of Active Objects with Application-Level Scheduling
  13. Object Connectivity and Full Abstraction for a Concurrent Calculus of Classes
  14. A Complete Guide to the Future

Autonomous Agents and Multiagent Systems

  1. Agent Programming in 3APL
  2. Agent Programming with Declarative Goals
  3. Programming Agent Deliberation: an approach illustrated using the 3APL language
  4. Control Structures of Rule-Based Agent Languages
  5. A verification framework for agent programming with declarative goals
  6. Semantics of communicating agents based on deduction and abduction
  7. Goal-Oriented Modularity in Agent Programming
  8. Coordination and composition in multi-agent systems
  9. On dynamically generated ontology translators in agent communication
  10. A formal embedding of agentspeak(L) in 3APL
  11. Information-Passing and Belief Revisionin Multi-agent Systems
  12. A verification framework for agent communication
  13. Prototyping 3APL in the Maude Term Rewriting Language
  14. Strategic Executions of Choreographed Timed Normative Multi-Agent Systems
  15. On Coordination, Autonomy and Time
  16. The Refinement of Choreographed Multi-Agent Systems
  17. On the Semantics and Verification of Normative Multi-Agent Systems
  18. A weakest precondition calculus for BUnity
  19. Model-Checking Agent Refinement

Coordination Languages

  1. Models and temporal logical specifications for timed component connectors>
  2. A Logical Interface Description Language for Components
  3. Synthesis of Reo Circuits for Implementation of Component-Connector Automata Specifications
  4. A Channel-based Coordination Model for Components
  5. MoChapi, an Exogenous Coordination Calculus based on Mobile Channels
  6. Reo Connectors as Coordination Artifacts in 2APL Systems
  7. Fault-Based Test Case Generation for Component Connectors
  8. Connectors as designs: Modeling, refinement and test case generation

Concurrent Logic and Constraint Languages

  1. A fully abstract model for concurrent constraint programming
  2. A timed concurrent constraint language
  3. Proving concurrent constraint programs correct
  4. Nondeterminism and infinite computations in constraint programming
  5. Partial order and SOS semantics for linear constraint programs
  6. A temporal logic for reasoning about timed concurrent constraint programs
  7. On the asynchronous nature of communication in concurrent logic languages: A fully abstract model based on sequences
  8. From concurrent logic programming to concurrent constraint programming

Actor Based Languages

  1. Decidability Problems for Actor Systems
  2. Model Checking, Automated Abstraction, and Compositional Verification of Rebeca Models
  3. Modular Verification of a Component-Based Actor Language
  4. Extended Rebeca: a component-based actor language with synchronous message passing

Enterprise Architectues

  1. Towards a language for coherent enterprise architecture descriptions
  2. Change impact analysis of enterprise architectures
  3. Enterprise Architecture Analysis with XML
  4. Integrating Architectural Models
  5. A logical viewpoint on architectures

Supervision PhD Theses

  1. Compositional Verification of Parallel Programs by M. van Hulst (Utrecht University, June 21, 1995).
  2. Semantics of Agent Communication Languages, by R. van Eijk (Utrecht University, October 18, 2000).
  3. The Agent Programming Language 3APL by K. Hindriks (Utrecht University, 2000).
  4. Semantical Analysis of Compositional Proof Rules for Concurrency by U. Hannemann (UU, October 30, 2000).
  5. Agent Interaction: Abstract Approaches to Modelling, Programming and Verifying Multi-Agent Systems by W. de Vries (Utrecht University, November 11, 2002).
  6. An Assertional Proof System for Multithreaded Java - Theory and Tool-Support by E. Abraham (LIACS, Januari 20, 2004).
  7. Verifying OCL Specifications of UML Models: Tool Support and Compositionality by M. Kyas (LIACS, April 4, 2006).
  8. Validation Techniques for Object-Oriented Proof Outlines by C. Pierik (Utrecht University, May, 2006).
  9. Cognitive Agent Programming: A Semantic Approach by B. van Riemsdijk (Utrecht Uuniversity, 2006).
  10. Mobile Channels for Exogenous Coordination of Distributed Systems : Semantics, Implementation and Composition by J. Scholten (LIACS, Januari 10, 2007).
  11. Domain Specific Modeling and Analysis by J. Jacob (LIACS, November 13, 2008).
  12. Testing Object Interaction by Andreas Gruener (LIACS, December 15, 2010).
  13. Time At your Service: Schedulability Analysis of Real-Time and Distributed Services by Mohammad Mahdi Jaghoori (LIACS, December 20, 2010).
  14. An Executable Theory of Multi-Agent Systems Refinement by Lacramioara Astefanoaei (Utrecht University, Januari 19, 2011).
  15. Organizing Agent Organizations: Syntax and Semantics of an Organization-Oriented Programming Language by N. Tinnemeier (Utrecht University, February 7, 2011).
  16. Modelling and Analysis of Real-Time Coordination Patterns by S. Kemper (LIACS, December 20, 2011).
  17. Static Analysis of Unbounded Structures in Object-Oriented Programs by I. Grabe (LIACS, December 19, 2012).
  18. Combining monitoring with run-time assertion checking by Stijn de Gouw (LIACS, December 18, 2013).
  19. Abstract delta modeling : software product lines and beyond by Michiel Helvensteijn (LIACS, December 11, 2014).
  20. Enhanced Coinduction by Jurriaan Rot (LIACS, October 15, 2015).
  21. Actors at Work by Behrooz Nobakht (LIACS, December 15, 2016).
  22. Abstract Behavioral Specification: unifying modeling and programming by Nikolaos Bezirgiannis (LIACS, April 17, 2018).

Projects

Recently I have been involved in the following EU FP7 projects:

Envisage: Engineering Virtualized Services
Upscale: From Inherent Concurrency to Massive Parallelism through Type-based Optimizations

Courses

Currently, I am giving (at LIACS) a course on Programmeren & Correctheid.

Professional History

And, finally, here you may find out more about my professional me.

CWI DISCLAIMER