Research of Wim H. Hesselink

• 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.