I have a BSc in Computer Science and Mathematics and a BSc (Hons) in Logic and Computation, both from Victoria University of Wellington, New Zealand. In 2009, I received a PhD on formal derivations of concurrent algorithms at the University of Queensland, Australia. After this, I held postdoctorate positions at the University of Queensland and then at the University of Sheffield. I was a lecturer at Brunel University London (2014-18).
My research is on formal techniques and verification methods for concurrent and real-time systems. This includes concurrent objects, transactional memory and associated correctness conditions; weak memory models; algebraic techniques; and hybrid systems.
University roles and responsibilities
- Level 3 coordinator
- Alumni and advancement coordinator
I am actively seeking good PhD students. Please contact me for further details.
COM1026 Foundations of Computing
COM2022 Computer Networking
COM3028 Systems Verification
COM3001 Professional Project
COMM002 MSc Dissertation
Professional Training (Computer Science)
totally ordered, linearizability is compositional: the composition of two
linearizable objects is guaranteed to be linearizable. However, linearizability
is not compositional when events are only partially ordered, as
in the weak-memory models that describe multicore memory systems.
In this paper, we present a generalisation of linearizability for concurrent
objects implemented in weak-memory models. We abstract from the
details of specific memory models by defining our condition using Lamport's
execution structures. We apply our condition to the C11 memory
model, providing a correctness condition for C11 objects. We develop a
proof method for verifying objects implemented in C11 and related models.
Our method is an adaptation of simulation-based methods, but in
contrast to other such methods, it does not require that the implementation
totally orders its events. We apply our proof technique and show
correctness of the Treiber stack that blocks on empty, annotated with
C11 release-acquire synchronisation.
fragment of the C11 memory model with relaxed
accesses. We show that the semantics is both sound and
complete with respect to the axiomatic model of Batty et
al. The semantics relies on a per-thread notion of observability,
which allows one to reason about a weak memory
C11 program in program order. On top of this, we develop a
proof calculus for invariant-based reasoning, which we use
to verify the release-acquire version of Peterson?s mutual
a programmer model for software transactional memory.
LTRF programs satisfy the SC-LTRF property, thus allowing
the programmer to focus on sequential executions in which
transactions execute atomically. Unlike previous results, SCLTRF
does not require global race freedom.We also provide a
lower-level implementation model to reason about quiescence
fences and validate numerous compiler optimizations.
Correctness to Weak Memory, 32nd International Symposium on Distributed Computing (DISC 2018) Proceedings Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik
on concurrent objects. In this paper, we propose a correctness condition (called causal atomicity)
for concurrent objects executing in a weak memory model, where the histories of the objects in
question are partially ordered. We establish compositionality and abstraction results for causal
atomicity and develop an associated refinement-based proof technique.
weak memory C11 programs in the Event-B framework.
We build on a recently developed operational semantics for
the RAR fragment of C11, which we use as a top-level abstraction.
In our technique, a concrete C11 program can be
modelled by refining this abstract model of the semantics.
Program structures and individual operations are then introduced
in the refined machine and can be checked and
verified using available Event-B provers and model checkers.
The paper also discusses how ProB model checker can be
used to validate the Event-B model of C11 programs. We applied
our technique to the C11 implementation of Peterson?s
algorithm, where we discovered that the standard invariant
used to characterise mutual exclusion is inadaquate. We
therefore propose and verify new invariants necessary for
characterising mutual exclusion in a weak memory setting.
new paradigm for memory preserving its contents even after power loss.
The expected ubiquity of NVM has stimulated interest in the design of
persistent concurrent data structures, together with associated notions of
correctness. In this paper, we present the first formal proof technique for
durable linearizability, which is a correctness criterion that extends linearizability
to handle crashes and recovery in the context of NVM. Our
proofs are based on refinement of IO-automata representations of concurrent
data structures. To this end, we develop a generic procedure for
transforming any standard sequential data structure into a durable specification.
Since the durable specification only exhibits durably linearizable
behaviours, it serves as the abstract specification in our refinement proof.
We exemplify our technique on a recently proposed persistent memory
queue that builds on Michael and Scott?s lock-free queue.
of equational first order logic. We adapt them to cylindric Kleene lattices
and their variants and present relational and relational fault models for
these. This allows us to encode frames and local variable blocks, and to
derive Morgan's refinement calculus as well as an algebraic Hoare logic
for while programs with assignment laws. Our approach thus opens the
door for algebraic calculations with program and logical variables instead
of domain-specific reasoning over concrete models of the program store.
A refinement proof for a small program is presented as an example.
 J. Derrick, G. Smith, L. Groves, and B. Dongol. A proof method for linearizability on TSO architectures. In Provably Correct Systems, NASA Monographs in Systems and Software Engineering, pages 61--91. Springer, 2017.
 B. Dongol, R. Jagadeesan, and J. Riely. Transactions in relaxed memory architectures. PACMPL, 2(POPL):18:1--18:29, 2018.
 B. Dongol and R. M. Hierons. Decidability and complexity for quiescent consistency and its variations. Information and Computation, 2017. In press.
 J. Derrick, S. Doherty, B. Dongol, G. Schellhorn, O. Travkin, and H. Wehrheim. Mechanized proofs of opacity: A comparison of two techniques. Formal Aspects of Computing, 2017. Accepted 21 July, 2017 (Mechanisations available here: https://swt.informatik.uni-augsburg.de/swt/projects/Opacity-TML.html).
 B. Dongol, V. B. F. Gomes, I. J. Hayes, and G. Struth. Partial semigroups and convolution algebras. Archive of Formal Proofs, 2017, 2017.
 B. Dongol, I. J. Hayes, and G. Struth. Convolution as a unifying concept: Applications in separation logic, interval calculi, and concurrency. ACM Trans. Comput. Log., 17(3):15:1--15:25, 2016.
 B. Dongol and J. Derrick. Verifying linearisability: A comparative survey. ACM Comput. Surv., 48(2):19, 2015.
 B. Dongol and J. Derrick. Interval-based data refinement: A uniform approach to true concurrency in discrete and real-time systems. Sci. Comput. Program., 111:214--247, 2015.
 B. Dongol, I. J. Hayes, and P. J. Robinson. Reasoning about goal-directed real-time teleo-reactive programs. Formal Asp. Comput., 26(3):563--589, 2014.
 B. Dongol, I. J. Hayes, and J. Derrick. Deriving real-time action systems with multiple time bands using algebraic reasoning. Sci. Comput. Program., 85:137--165, 2014.
 I. J. Hayes, A. Burns, B. Dongol, and C. B. Jones. Comparing degrees of non-determinism in expression evaluation. Comput. J., 56(6):741--755, 2013.
 B. Dongol and I. J. Hayes. Deriving real-time action systems in a sampling logic. Sci. Comput. Program., 78(11):2047--2063, 2013.
 R. Colvin and B. Dongol. A general technique for proving lock-freedom. Sci. Comput. Program., 74(3):143--165, 2009.
B. Dongol and A. J. Mooij. Streamlining progress-based derivations of concurrent programs. Formal Asp. Comput., 20(2):141--160, 2008.
B. Dongol and D. Goldson. Extending the theory of Owicki and Gries with a logic of progress. Logical Methods in Computer Science, 2(1), 2006.
Refereed Conference Publications
 S. Doherty, B. Dongol, H. Wehrheim, and J. Derrick. Brief announcement: Generalising concurrent correctness to weak memory. In DISC, 2018. To appear.
 S. Doherty, B. Dongol, H. Wehrheim, and J. Derrick. Making linearizability compositional for partially ordered executions. In iFM, Lecture Notes in Computer Science. Springer, 2018. To appear.
 B. Dongol, R. Jagadeesan, J. Riely, and A. Armstrong. On abstraction and compositionality for weak-memory linearisability. In VMCAI, volume 10747 of Lecture Notes in Computer Science, pages 183--204. Springer, 2018.
 A. Armstrong and B. Dongol. Modularising opacity verification for hybrid transactional memory. In FORTE, volume 10321 of Lecture Notes in Computer Science, pages 33--49. Springer, 2017.
 A. Armstrong, B. Dongol, and S. Doherty. Proving opacity via linearizability: A sound and complete method. In FORTE, volume 10321 of Lecture Notes in Computer Science, pages 50--66. Springer, 2017. (Previous version: https://arxiv.org/abs/1610.01004).
 S. Doherty, B. Dongol, J. Derrick, G. Schellhorn, and H. Wehrheim. Proving opacity of a pessimistic STM. In OPODIS, volume 70 of LIPIcs, pages 35:1--35:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.
 B. Dongol. An interval logic for stream-processing functions: A convolution-based construction. In FTSCS, volume 694 of Communications in Computer and Information Science, pages 20--35, 2016.
 B. Dongol and L. Groves. Contextual trace refinement for concurrent objects: Safety and progress. In ICFEM, volume 10009 of Lecture Notes in Computer Science, pages 261--278, 2016.
 B. Dongol and R. M. Hierons. Decidability and complexity for quiescent consistency. In LICS, pages 116--125. ACM, 2016.
 B. Dongol and L. Groves. Towards linking correctness conditions for concurrent objects and contextual trace refinement. In Refine@FM, volume 209 of EPTCS, pages 107--111, 2015.
 J. Derrick, B. Dongol, G. Schellhorn, O. Travkin, and H. Wehrheim. Verifying opacity of a transactional mutex lock. In N. Bjørner and F. D. de Boer, editors, FM, volume 9109 of LNCS, pages 161--177. Springer, 2015.
 B. Dongol, V. B. F. Gomes, and G. Struth. A program construction and verification tool for separation logic. In R. Hinze and J. Voigtländer, editors, MPC, volume 9129 of LNCS, pages 137--158. Springer, 2015.
 B. Dongol, J. Derrick, L. Groves, and G. Smith. Defining correctness conditions for concurrent objects in multicore architectures. In J. T. Boyland, editor, ECOOP, volume 37 of LIPIcs, pages 470--494. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.
 J. Derrick, G. Smith, L. Groves, and B. Dongol. Using coarse-grained abstractions to verify linearizability on TSO architectures. In E. Yahav, editor, HVC, volume 8855 of LNCS, pages 1--16. Springer, 2014.
 G. Smith, J. Derrick, and B. Dongol. Admit your weakness: Verifying correctness on TSO architectures. In I. Lanese and E. Madelaine, editors, FACS, volume 8997 of LNCS, pages 364--383. Springer, 2014.
 J. Derrick, G. Smith, and B. Dongol. Verifying linearizability on TSO architectures. In E. Albert and E. Sekerinski, editors, iFM, volume 8739 of LNCS, pages 341--356. Springer, 2014.
 B. Dongol, J. Derrick, and G. Smith. Reasoning algebraically about refinement on TSO architectures. In G. Ciobanu and D. Méry, editors, ICTAC, volume 8687 of LNCS, pages 151--168. Springer, 2014.
 J. Derrick, B. Dongol, G. Schellhorn, B. Tofan, O. Travkin, and H. Wehrheim. Quiescent consistency: Defining and verifying relaxed linearizability. In C. B. Jones, P. Pihlajasaari, and J. Sun, editors, FM, volume 8442 of LNCS, pages 200--214. Springer, 2014.
 B. Dongol and J. Derrick. Simplifying proofs of linearisability using layers of abstraction. ECEASST, 66, 2013.
 B. Dongol, O. Travkin, J. Derrick, and H. Wehrheim. A high-level semantics for program execution under total store order memory. In Z. Liu, J. Woodcock, and H. Zhu, editors, ICTAC, volume 8049 of LNCS, pages 177--194. Springer, 2013.
 B. Dongol and J. Derrick. Data refinement for true concurrency. In J. Derrick, E. A. Boiten, and S. Reeves, editors, Refine, volume 115 of EPTCS, pages 15--35, 2013.
 B. Dongol, J. Derrick, and I. J. Hayes. Fractional permissions and non-deterministic evaluators in interval temporal logic. ECEASST, 53, 2012.
 B. Dongol, I. J. Hayes, L. Meinicke, and K. Solin. Towards an algebra for real-time programs. In W. Kahl and T. G. Griffin, editors, RAMICS, volume 7560 of LNCS, pages 50--65. Springer, 2012.
 B. Dongol and I. J. Hayes. Deriving real-time action systems controllers from multiscale system specifications. In J. Gibbons and P. Nogueira, editors, MPC, volume 7342 of LNCS, pages 102--131. Springer, 2012.
 B. Dongol and I. J. Hayes. Rely/guarantee reasoning for teleo-reactive programs over multiple time bands. In J. Derrick, S. Gnesi, D. Latella, and H. Treharne, editors, IFM, volume 7321 of LNCS, pages 39--53. Springer, 2012.
 B. Dongol and I. J. Hayes. Approximating idealised real-time specifications using time bands. ECEASST, 46:1--16, 2012. 11th International Workshop on Automated Verification of Critical Systems.
 B. Dongol and I. J. Hayes. Compositional action system derivation using enforced properties. In C. Bolduc, J. Desharnais, and B. Ktari, editors, MPC, volume 6120 of LNCS, pages 119--139. Springer, 2010.
 B. Dongol and I. J. Hayes. Enforcing safety and progress properties: An approach to concurrent program derivation. In ASWEC, pages 3--12. IEEE Computer Society, 2009.
 R. Colvin and B. Dongol. Verifying lock-freedom using well-founded orders. In C. B. Jones, Z. Liu, and J. Woodcock, editors, ICTAC, volume 4711 of LNCS, pages 124--138. Springer, 2007.
 B. Dongol. Formalising progress properties of non-blocking programs. In Z. Liu and J. He, editors, ICFEM, volume 4260 of LNCS, pages 284--303. Springer, 2006.
 B. Dongol. Towards simpler proofs of lock-freedom. In Preliminary Proceedings of the 1st Asian Working Conference on Verified Software, pages 136--146, 2006.
 B. Dongol. Derivation of Java monitors. In ASWEC, pages 211--220. IEEE Computer Society, 2006.
 B. Dongol and A. J. Mooij. Progress in deriving concurrent programs: Emphasizing the role of stable guards. In T. Uustalu, editor, MPC, volume 4014 of LNCS, pages 140--161. Springer, 2006.
 D. Goldson and B. Dongol. Concurrent program design in the extended theory of Owicki and Gries. In M. D. Atkinson and F. K. H. A. Dehne, editors, CATS, volume 41 of CRPIT, pages 41--50. Australian Computer Society, 2005.
 B. Dongol. Progress-based verification and derivation of concurrent programs. PhD thesis, School of Information Technology and Electrical Engineering, The University of Queensland, Qld, Australia, October 2009.
Technical reports (not elsewhere published)
B. Dongol, I. J. Hayes, and G. Struth. Relational Convolution, Generalised Modalities and Incidence Algebras. ArXiv e-prints, February 2017.
B. Dongol and J. Derrick. Proving linearisability via coarse-grained abstraction. CoRR, abs/1212.5116, 2012.
B. Dongol and I. J. Hayes. Reasoning about teleo-reactive programs under parallel composition. Technical Report SSE-2011-01, Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland, QLD 4072, Australia, April 2011.
B. Dongol and I. J. Hayes. Trace semantics for the Owicki-Gries theory integrated with the progress logic from UNITY. Technical Report SSE-2007-02, Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland, QLD 4072, Australia, April 2007.