Welcome to the home page of Frank S. de Boer
Centrum voor Wiskunde en Informatica (CWI)
of Software Engineering
P.O. Box 94079
1090 GB Amsterdam
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
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,
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
my Google Scholar profile.
programming languages for multi-agent systems I also refer to my
stored by the
group at the department
of Information and Computing Sciences of Utrecht University).
Here you can find some selected publications.
Verification of object-oriented programs: A transformational approach
A WP-calculus for OO
Abstract Object Creation in Dynamic Logic: To Be or Not to Be Created
Automated Verification of Recursive
Programs with Pointers
Reasoning about dynamically evolving process structures
for Java's Rentrant Multithreading Concept
Automated Deadlock Detection in Synchronized
Reentrant Multithreaded Call-Graph
A Syntax-Directed Hoare Logic
for Object-Oriented Programming Concepts
Formalizing UML Models and OCL Constraints in PVS
Schedulability of asynchronous real-time concurrent objects
User-defined schedulers for real-time concurrent objects
Programming and Deployment of Active Objects with
Object Connectivity and Full Abstraction
for a Concurrent Calculus of Classes
A Complete Guide to the Future
Autonomous Agents and Multiagent Systems
Agent Programming in 3APL
Agent Programming with Declarative Goals
Programming Agent Deliberation: an approach illustrated using the 3APL language
of Rule-Based Agent Languages
A verification framework for agent programming with declarative goals
Semantics of communicating agents based on deduction and abduction
Modularity in Agent Programming
Coordination and composition in multi-agent systems
On dynamically generated ontology translators in agent communication
A formal embedding of agentspeak(L) in 3APL
Information-Passing and Belief Revisionin Multi-agent Systems
A verification framework for agent communication
Prototyping 3APL in the Maude Term
Strategic Executions of Choreographed
Timed Normative Multi-Agent Systems
On Coordination, Autonomy and Time
The Refinement of Choreographed Multi-Agent Systems
On the Semantics and Verification of Normative
A weakest precondition calculus for BUnity
Model-Checking Agent Refinement
Models and temporal logical specifications for timed
A Logical Interface Description Language
Synthesis of Reo Circuits for Implementation of
Component-Connector Automata Specifications
A Channel-based Coordination Model for
an Exogenous Coordination Calculus based on
Reo Connectors as Coordination Artifacts in
Fault-Based Test Case Generation for Component Connectors
Connectors as designs: Modeling, refinement and test case generation
Concurrent Logic and Constraint Languages
A fully abstract model for concurrent constraint programming
A timed concurrent constraint language
Proving concurrent constraint programs correct
Nondeterminism and infinite computations in constraint programming
Partial order and SOS semantics for linear constraint programs
A temporal logic for reasoning about timed concurrent constraint programs
On the asynchronous nature of communication in concurrent logic languages: A fully abstract model based on sequences
From concurrent logic programming to concurrent constraint programming
Actor Based Languages
Decidability Problems for Actor Systems
Model Checking, Automated Abstraction, and
Compositional Verification of Rebeca Models
Modular Verification of a Component-Based Actor Language
Extended Rebeca: a component-based actor language with synchronous message passing
Towards a language for coherent enterprise architecture descriptions
Change impact analysis of enterprise architectures
Enterprise Architecture Analysis with XML
Integrating Architectural Models
A logical viewpoint on architectures
Supervision PhD Theses
Compositional Verification of Parallel Programs by M. van Hulst (Utrecht University, June
Semantics of Agent Communication Languages, by R. van Eijk
(Utrecht University, October 18, 2000).
The Agent Programming Language 3APL
by K. Hindriks (Utrecht University, 2000).
Semantical Analysis of Compositional Proof Rules for
Concurrency by U. Hannemann
(UU, October 30, 2000).
Agent Interaction: Abstract Approaches to Modelling, Programming and Verifying Multi-Agent Systems by W. de Vries (Utrecht University, November 11, 2002).
An Assertional Proof System for Multithreaded Java - Theory and Tool-Support by E. Abraham
(LIACS, Januari 20, 2004).
Verifying OCL Specifications of UML Models: Tool Support and
Compositionality by M. Kyas
(LIACS, April 4, 2006).
Validation Techniques for Object-Oriented Proof Outlines by C. Pierik
(Utrecht University, May, 2006).
Cognitive Agent Programming: A Semantic Approach by B. van Riemsdijk
(Utrecht Uuniversity, 2006).
Mobile Channels for Exogenous Coordination of Distributed
Systems : Semantics, Implementation and Composition by J. Scholten (LIACS, Januari
Domain Specific Modeling and Analysis by J. Jacob
(LIACS, November 13, 2008).
Testing Object Interaction by Andreas Gruener
(LIACS, December 15, 2010).
Time At your Service: Schedulability Analysis of Real-Time and Distributed Services by
Mohammad Mahdi Jaghoori
(LIACS, December 20, 2010).
An Executable Theory of Multi-Agent Systems Refinement
by Lacramioara Astefanoaei
(Utrecht University, Januari 19, 2011).
Organizing Agent Organizations: Syntax and Semantics of an Organization-Oriented Programming Language by N. Tinnemeier
(Utrecht University, Februari, 2011).
Modelling and Analysis of Real-Time Coordination Patterns
by S. Kemper (LIACS, December 20, 2011).
Static Analysis of Unbounded Structures in Object-Oriented Programs by I. Grabe
(LIACS, December 19, 2012).
Combining monitoring with run-time assertion checking by Stijn de Gouw
(LIACS, December 18, 2013).
Abstract delta modeling : software product lines and beyond by Michiel Helvensteijn (LIACS, December 11, 2014).
Recently I have been involved in
project which is an Integrated Project supported by the 7th Framework Programme of the EC within the FET (Future and Emerging Technologies) scheme.
The HATS project develops a formal method for the design, analysis, and implementation of software product families.
Currently I am involved in the following two EU FP7 projects:
Envisage: Engineering Virtualized Services
Upscale: From Inherent Concurrency to Massive Parallelism through Type-based Optimizations
Currently, I am giving (at LIACS) a course on
Programmeren & Correctheid.
And, finally, here you may find out more about my professional me.