2024
First-Come-First-Served as a Separate Principle.
ACM Trans. Parallel Comput., December, 2024
2023
MCSH, a Lock with the Standard Interface.
ACM Trans. Parallel Comput., June, 2023
2022
Trylock, a case for temporal logic and eternity variables.
Sci. Comput. Program., 2022
2021
UNITY and Büchi automata.
Formal Aspects Comput., 2021
2019
Group Mutual Exclusion by Fetch-and-increment.
ACM Trans. Parallel Comput., 2019
2018
Fast mutual exclusion by the Triangle algorithm.
Concurr. Comput. Pract. Exp., 2018
High-contention mutual exclusion by elevator algorithms.
Concurr. Comput. Pract. Exp., 2018
2017
Tournaments for mutual exclusion: verification and concurrent complexity.
Formal Aspects Comput., 2017
2016
Correctness and concurrent complexity of the Black-White Bakery Algorithm.
Formal Aspects Comput., 2016
Dekker's mutual exclusion algorithm made RW-safe.
Concurr. Comput. Pract. Exp., 2016
2015
Mutual exclusion by four shared bits with not more than quadratic complexity.
Sci. Comput. Program., 2015
High-performance <i>N</i>-thread software solutions for mutual exclusion.
Concurr. Comput. Pract. Exp., 2015
2013
Mechanical verification of Lamport's Bakery algorithm.
Sci. Comput. Program., 2013
Complete assertional proof rules for progress under weak and strong fairness.
Sci. Comput. Program., 2013
Starvation-free mutual exclusion with semaphores.
Formal Aspects Comput., 2013
A distributed resource allocation algorithm for many processes.
Acta Informatica, 2013
Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos.
Acta Informatica, 2013
2012
Finite and infinite implementation of transition systems.
Theor. Comput. Sci., 2012
Formalizing a hierarchical file system.
Formal Aspects Comput., 2012
2011
Queue based mutual exclusion with linearly bounded overtaking.
Sci. Comput. Program., 2011
Simulation refinement for concurrency verification.
Sci. Comput. Program., 2011
Partial mutual exclusion for infinitely many processes
CoRR, 2011
Nonatomic dual bakery algorithm with bounded tokens.
Acta Informatica, 2011
2010
Alternating states for dual nondeterminism in imperative programming.
Theor. Comput. Sci., 2010
Simple concurrent garbage collection almost without synchronization.
Formal Methods Syst. Des., 2010
Solutions of equations in languages.
Formal Aspects Comput., 2010
2009
A queue based mutual exclusion algorithm.
Acta Informatica, 2009
Verification of a Lock-Free Implementation of Multiword LL/SC Object.
Proceedings of the Eighth IEEE International Conference on Dependable, 2009
2008
A challenge for atomicity verification.
Sci. Comput. Program., 2008
Concurrent Computation of Attribute Filters on Shared Memory Parallel Machines.
IEEE Trans. Pattern Anal. Mach. Intell., 2008
Euclidean Skeletons of Digital Image and Volume Data in Linear Time by the Integer Medial Axis Transform.
IEEE Trans. Pattern Anal. Mach. Intell., 2008
Universal extensions to simulate specifications.
Inf. Comput., 2008
2007
Lock-free parallel and concurrent garbage collection by mark&sweep.
Sci. Comput. Program., 2007
A linear-time algorithm for Euclidean feature transform sets.
Inf. Process. Lett., 2007
A general lock-free algorithm using compare-and-swap.
Inf. Comput., 2007
Kekulé Cells for Molecular Computation
CoRR, 2007
A criterion for atomicity revisited.
Acta Informatica, 2007
2006
Refinement verification of the lazy caching algorithm.
Acta Informatica, 2006
Splitting forward simulations to copewith liveness.
Acta Informatica, 2006
2005
Eternity variables to prove simulation of specifications.
ACM Trans. Comput. Log., 2005
Lock-free dynamic hash tables with open addressing.
Distributed Comput., 2005
Lock-Free Parallel Garbage Collection.
Proceedings of the Parallel and Distributed Processing and Applications, 2005
Euclidean Skeletons of 3D Data Sets in Linear Time by the Integer Medial Axis Transform.
Proceedings of the Mathematical Morphology: 40 Years On, 2005
Experiments with strategies for agents in the social interaction game Mafia.
Proceedings of the BNAIC 2005, 2005
2004
Using eternity variables to specify and prove a serializable database interface.
Sci. Comput. Program., 2004
Knowledge-Based Asynchronous Programming.
Fundam. Informaticae, 2004
An assertional proof for a construction of an atomic variable.
Formal Aspects Comput., 2004
Almost Wait-Free Resizable Hashtable.
Proceedings of the 18th International Parallel and Distributed Processing Symposium (IPDPS 2004), 2004
A Formal Reduction for Lock-Free Parallel Algorithms.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004
2003
Salembier's Min-tree algorithm turned into breadth first search.
Inf. Process. Lett., 2003
Efficient almost wait-free parallel accessible dynamic hashtables
CoRR, 2003
Preference rankings in the face of uncertainty.
Acta Informatica, 2003
2002
An assertional criterion for atomicity.
Acta Informatica, 2002
Eternity Variables to Simulate Specifications.
Proceedings of the Mathematics of Program Construction, 6th International Conference, 2002
2001
Concurrent determination of connected components.
Sci. Comput. Program., 2001
Wait-free concurrent memory management by Create and Read until Deletion (CaRuD).
Distributed Comput., 2001
An algorithm for the asynchronous Write-All problem based on process collision.
Distributed Comput., 2001
2000
Fixpoint semantics and simulation.
Theor. Comput. Sci., 2000
A generalization of Naundorf's fixpoint theorem.
Theor. Comput. Sci., 2000
A General Algorithm for Computing Distance Transforms in Linear Time.
Proceedings of the 5th International Symposium on Mathematical Morphology and its Applications to Image and Signal Processing, 2000
1999
Predicate Transformers for Recursive Procedures with Local Variables.
Formal Aspects Comput., 1999
The Verified Incremental Design of a Distributed Spanning Tree Algorithm: Extended Abstract.
Formal Aspects Comput., 1999
Progress Under Bounded Fairness.
Distributed Comput., 1999
1998
Invariants for the Construction of a Handshake Register.
Inf. Process. Lett., 1998
The design of a linearization of a concurrent data object.
Proceedings of the Programming Concepts and Methods, 1998
1997
Theories for Mechanical Proofs of Imperative Programs.
Formal Aspects Comput., 1997
A Mechanical Proof of Segall's PIF Algorithm.
Formal Aspects Comput., 1997
1996
Bounded Delay for a Free Address.
Acta Informatica, 1996
1995
Safety and Progress of Recursive Procedures.
Formal Aspects Comput., 1995
Wait-Free Linearization with a Mechanical Proof.
Distributed Comput., 1995
Angelic Termination in Dijkstra's Calculus.
Proceedings of the Mathematics of Program Construction, 1995
1994
Nondeterminacy and Recursion via Stacks and Games.
Theor. Comput. Sci., 1994
Wait-Free Linearization with an Assertional Proof.
Distributed Comput., 1994
Compact Image Representation using Gabor Wavelets.
Proceedings of the Massively Parallel Processing Applications and Develompent, 1994
1993
Proof Rules for Recursive Procedures.
Formal Aspects Comput., 1993
1992
Processes and Formalism for Unbounded Choice.
Theor. Comput. Sci., 1992
Sci. Comput. Program., 1992
Temporal Preconditions of Recursive Procedures.
Proceedings of the Sematics: Foundations and Applications, 1992
1991
Repetitions, Known or Unknown?
Inf. Process. Lett., 1991
Inf. Process. Lett., 1991
1990
Axioms and Models of Linear Logic.
Formal Aspects Comput., 1990
Command Algebras, Recursion and Program Transformation.
Formal Aspects Comput., 1990
1989
Predicate-Transformer Semantics of General Recursion.
Acta Informatica, 1989
Initialisation with a Final Value, an Exercise in Program Transformation.
Proceedings of the Mathematics of Program Construction, 1989
1988
A Mathematical Approach to Nondeterminism in Data Types.
ACM Trans. Program. Lang. Syst., 1988
Deadlock and Fairness in Morphisms of Transition Systems.
Theor. Comput. Sci., 1988
Interpretations of Recursion under Unbounded Nondeterminacy.
Theor. Comput. Sci., 1988
