- Development and verification of concurrent programs, usually for shared memory, e.g., refinement of atomicity, concurrent garbage collection, concurrent hash tables.
- Application of mechanical theorem provers like PVS and NQTHM, mainly to algorithms of the previous item, but possibly also to the verification of Wiles' proof of Fermat's Last Theorem.
- Basic algorithms for image processing, not necessarily concurrent: connected components, Euclidean distance transform, Euclidean feature transform, Maxtrees, skeletons.
- Weakest precondition semantics of sequential programs with recursion, unbounded nondeterminacy (both demonic and angelic), and local variables.
- Knowledge based programs.
- Molecular computing by polycyclic hydrocarbons.

Wim H. Hesselink Last modified: Fri Nov 9 10:47:43 CET 2007