Publications

Books and Edited Proceedings

[1] B. Dongol and E. Troubitsyna. Introduction to the special section on iFM 2020. Formal Aspects Comput., 34(1):1, 2022. [ bib | DOI | http ]
[2] A. Cavalcanti, B. Dongol, R. Heirons, J. Timmis, and J. Woodcock, editors. Software Engineering for Robotics. Springer, 2021. [ bib ]
[3] B. Dongol and E. Troubitsyna, editors. Integrated Formal Methods - 16th International Conference, IFM 2020, Lugano, Switzerland, November 16-20, 2020, Proceedings, volume 12546 of LNCS. Springer, 2020. [ bib ]
[4] E. Sekerinski, N. Moreira, J. N. Oliveira, D. Ratiu, R. Guidotti, M. Farrell, M. Luckcuck, D. Marmsoler, J. Campos, T. Astarte, L. Gonnord, A. Cerone, L. Couto, B. Dongol, M. Kutrib, P. Monteiro, and D. Delmas, editors. Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part I, volume 12232 of LNCS. Springer, 2020. [ bib | DOI | http ]
[5] J. Derrick, B. Dongol, and S. Reeves, editors. Proceedings 19th Refinement Workshop, Refine@FM 2019, Porto, UK, 2019. [ bib ]
[6] B. Dongol, L. Petre, and G. Smith, editors. Formal Methods Teaching - Third International Workshop and Tutorial, FMTea 2019, Held as Part of the Third World Congress on Formal Methods, FM 2019, Porto, Portugal, October 7, 2019, Proceedings, volume 11758 of LNCS. Springer, 2019. [ bib | DOI | http ]
[7] J. Derrick, B. Dongol, and S. Reeves, editors. Proceedings 18th Refinement Workshop, Refine@FM 2018, Oxford, UK, 18th July 2018, volume 282 of EPTCS, 2018. [ bib | DOI | http ]

Book Chapters

[8] B. Dongol, R. Bell, I. Habli, M. Lawford, P. Moore, and Z. Saigol. Panel Discussion: Regulation and Ethics of Robotics and Autonomous Systems, pages 467--483. Springer International Publishing, Cham, 2021. [ bib | DOI | http ]
[9] 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. [ bib ]

Journal Publications

[10] D. Wright, S. Dalvandi, M. Batty, and B. Dongol. Mechanised operational reasoning for C11 programs with relaxed dependencies. ACM Formal Aspects of Computing, 2023. (To appear). [ bib ]
[11] S. Dalvandi and B. Dongol. Implementing and verifying release-acquire transactional memory in C11. Proc. ACM Program. Lang., 6(OOPSLA2):1817--1844, 2022. [ bib ]
[12] E. Bila, J. Derrick, S. Doherty, B. Dongol, G. Schellhorn, and H. Wehrheim. Modularising verification of durable opacity. Log. Methods Comput. Sci., 18(3), 2022. [ bib | DOI | http ]
[13] S. Doherty, S. Dalvandi, B. Dongol, and H. Wehrheim. Unifying operational weak memory verification: An axiomatic approach. ACM Trans. Comput. Log., 23(4):27:1--27:39, 2022. [ bib | DOI | http ]
[14] T. Kulik, B. Dongol, P. Gorm Larsen, H. Daniel Macedo, S. Schneider, P. D. W. V. Tran-Jørgensen, and J. Woodcock. A survey of practical formal methods for security. 34(1):1--39, 2022. [ bib | DOI | http ]
[15] S. Dalvandi, B. Dongol, S. Doherty, and H. Wehrheim. Integrating Owicki-Gries for C11-Style memory models into Isabelle/HOL. J. Autom. Reason., 66(1):141--171, 2022. [ bib | DOI | http ]
[16] J. Derrick, S. Doherty, B. Dongol, G. Schellhorn, and H. Wehrheim. Verifying correctness of persistent concurrent data structures: a sound and complete method. Formal Aspects Comput., 33(4-5):547--573, 2021. [ bib | DOI | http ]
[17] B. Dongol, I. J. Hayes, and G. Struth. Convolution algebras: Relational convolution, generalised modalities and incidence algebras. Log. Methods Comput. Sci., 17(1), 2021. [ bib | http ]
[18] T. Y. Lam and B. Dongol. A blockchain-enabled e-learning platform. Interactive Learning Environments, 0(0):1--23, 2020. [ bib | DOI | http ]
[19] B. Dongol, R. Jagadeesan, and J. Riely. Transactions in relaxed memory architectures. PACMPL, 2(POPL):18:1--18:29, 2018. [ bib ]
[20] B. Dongol and R. M. Hierons. Decidability and complexity for quiescent consistency and its variations. Inf. Comput., 257:1--21, 2017. [ bib ]
[21] J. Derrick, S. Doherty, B. Dongol, G. Schellhorn, O. Travkin, and H. Wehrheim. Mechanized proofs of opacity: a comparison of two techniques. Formal Asp. Comput., 30(5):597--625, 2018. [ bib | Mechanisation ]
[22] 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. [ bib ]
[23] B. Dongol and J. Derrick. Verifying linearisability: A comparative survey. ACM Comput. Surv., 48(2):19, 2015. [ bib | DOI | http ]
[24] 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. [ bib | DOI | http ]
[25] 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. [ bib ]
[26] 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. [ bib ]
[27] 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. [ bib ]
[28] B. Dongol and I. J. Hayes. Deriving real-time action systems in a sampling logic. Sci. Comput. Program., 78(11):2047--2063, 2013. [ bib ]
[29] R. Colvin and B. Dongol. A general technique for proving lock-freedom. Sci. Comput. Program., 74(3):143--165, 2009. [ bib | PVS files ]
[30] B. Dongol and A. J. Mooij. Streamlining progress-based derivations of concurrent programs. Formal Asp. Comput., 20(2):141--160, 2008. [ bib ]
[31] 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. [ bib ]

Refereed Conference Publications

[32] S. Bodenmüller, J. Derrick, B. Dongol, G. Schellhorn, and H. Wehrheim. A fully verified persistency library. In VMCAI, LNCS. Springer, 2024. [ bib | DOI | arXiv | www: ]
[33] M. Semenyuk, M. Batty, and B. Dongol. Verifying read-copy update under RC11. In C. Ferreira and T. A. C. Willemse, editors, SEFM, volume 14323 of LNCS, pages 301--319. Springer, 2023. [ bib | DOI | http ]
[34] O. Lahav, B. Dongol, and H. Wehrheim. Rely-guarantee reasoning for causally consistent shared memory. In C. Enea and A. Lal, editors, CAV, volume 13964 of LNCS, pages 206--229. Springer, 2023. [ bib | DOI | http ]
[35] H. Wehrheim, L. Bargmann, and B. Dongol. Reasoning about promises in weak memory models with event structures. In M. Chechik, J.-P. Katoen, and M. Leucker, editors, FM, volume 14000 of LNCS, pages 282--300. Springer, 2023. [ bib | DOI | http ]
[36] J. Le-Papin, B. Dongol, H. Treharne, and S. Wesemeyer. Verifying list swarm attestation protocols. In I. Boureanu, S. Schneider, B. Reaves, and N. Ole Tippenhauer, editors, ACM WiSec, pages 163--174. ACM, 2023. [ bib | DOI | http ]
[37] M. Semenyuk and B. Dongol. Ownership-based Owicki-Gries reasoning. In J. Hong, M. Lanperne, J. W. Park, T. Cerný, and H. Shahriar, editors, ACM/SIGAPP SAC, pages 1685--1694. ACM, 2023. [ bib | DOI | http ]
[38] S. Ahmadi, B. Dongol, and M. Griffin. Proving memory access violations in Isabelle/HOL. In C. Artho and P. C. Ölveczky, editors, FTSCS, pages 45--55. ACM, 2022. [ bib | DOI | http ]
[39] B. Dongol, G. Schellhorn, and H. Wehrheim. Weak progressive forward simulation is necessary and sufficient for strong observational refinement. In B. Klin, S. Lasota, and A. Muscholl, editors, CONCUR, volume 243 of LIPIcs, pages 31:1--31:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. [ bib | DOI | http ]
[40] E. Vafeiadi Bila, B. Dongol, O. Lahav, A. Raad, and J. Wickerson. View-based Owicki-Gries reasoning for persistent x86-TSO. In I. Sergey, editor, ESOP, volume 13240 of LNCS, pages 234--261. Springer, 2022. Distinguished artifact award. [ bib | DOI | arXiv | http ]
[41] B. Dongol and J. Le-Papin. Checking opacity and durable opacity with FDR. In R. Calinescu and C. S. Pasareanu, editors, SEFM, volume 13085 of LNCS, pages 222--242. Springer, 2021. [ bib | DOI | http ]
[42] D. Wright, M. Batty, and B. Dongol. Owicki-Gries reasoning for C11 programs with relaxed dependencies. In M. Huisman, C. S. Pasareanu, and N. Zhan, editors, FM, volume 13047 of LNCS, pages 237--254. Springer, 2021. [ bib | DOI | http ]
[43] M. Griffin and B. Dongol. Verifying secure speculation in Isabelle/HOL. In M. Huisman, C. S. Pasareanu, and N. Zhan, editors, FM, volume 13047 of LNCS, pages 43--60. Springer, 2021. [ bib | DOI | http ]
[44] S. Dalvandi and B. Dongol. Verifying C11-style weak memory libraries. In Jaejin Lee and Erez Petrank, editors, PPoPP, pages 451--453. ACM, 2021. [ bib | DOI | http ]
[45] E. Bila, S. Doherty, B. Dongol, J. Derrick, G. Schellhorn, and H. Wehrheim. Defining and verifying durable opacity: Correctness for persistent software transactional memory. In FORTE, 2020. Best paper award. [ bib | DOI ]
[46] S. Dalvandi, S. Doherty, B. Dongol, and H. Wehrheim. Owicki-Gries reasoning for C11 RAR. In ECOOP, 2020. [ bib | DOI | www: ]
[47] J. Derrick, S. Doherty, B. Dongol, G. Schellhorn, and H. Wehrheim. Verifying correctness of persistent concurrent data structures. In M. H. ter Beek, A. McIver, and J. N. Oliveira, editors, FM, volume 11800 of LNCS, pages 179--195. Springer, 2019. [ bib | DOI | http ]
[48] K. Clark, B. Dongol, and P. Robinson. Temporal logic semantics for teleo-reactive robotic agent programs. In Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part I, volume 12232 of LNCS, pages 265--280. Springer, 2019. [ bib | DOI | http ]
[49] B. Dongol, I. J. Hayes, L. Meinicke, and G. Struth. Cylindric kleene lattices for program construction. In G. Hutton, editor, MPC, volume 11825 of LNCS, pages 197--225. Springer, 2019. [ bib | DOI | http ]
[50] M. Dalvandi and B. Dongol. Towards deductive verification of C11 programs with Event-B and ProB. In G. Ernst and T. Murray, editors, FTfJP. ACM, 2019. [ bib ]
[51] B. Dongol, R. Jagadeesan, and J. Riely. Modular transactions: bounding mixed races in space and time. In PPoPP, pages 82--93. ACM, 2019. [ bib ]
[52] S. Doherty, B. Dongol, H. Wehrheim, and J. Derrick. Verifying C11 programs operationally. In PPoPP, pages 355--365. ACM, 2019. [ bib | Full version ]
[53] S. Doherty, B. Dongol, H. Wehrheim, and J. Derrick. Brief announcement: Generalising concurrent correctness to weak memory. In U. Schmid and J. Widder, editors, DISC, volume 121 of LIPIcs, pages 45:1--45:3. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. [ bib | DOI | http ]
[54] S. Doherty, B. Dongol, H. Wehrheim, and J. Derrick. Making linearizability compositional for partially ordered executions. In C. A. Furia and K. Winter, editors, iFM, volume 11023 of LNCS, pages 110--129. Springer, 2018. [ bib | DOI | Full version | http ]
[55] B. Dongol, R. Jagadeesan, J. Riely, and A. Armstrong. On abstraction and compositionality for weak-memory linearisability. In VMCAI, volume 10747 of LNCS, pages 183--204. Springer, 2018. [ bib | Slides ]
[56] A. Armstrong and B. Dongol. Modularising opacity verification for hybrid transactional memory. In FORTE, volume 10321 of LNCS, pages 33--49. Springer, 2017. [ bib | Isabelle files ]
[57] A. Armstrong, B. Dongol, and S. Doherty. Proving opacity via linearizability: A sound and complete method. In FORTE, volume 10321 of LNCS, pages 50--66. Springer, 2017. [ bib | arXiv | Isabelle files ]
[58] 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. [ bib | Mechanisation | Isabelle files ]
[59] 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. [ bib ]
[60] B. Dongol and L. Groves. Contextual trace refinement for concurrent objects: Safety and progress. In ICFEM, volume 10009 of LNCS, pages 261--278, 2016. [ bib ]
[61] B. Dongol and R. M. Hierons. Decidability and complexity for quiescent consistency. In LICS, pages 116--125. ACM, 2016. [ bib ]
[62] 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. [ bib ]
[63] 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. [ bib | DOI ]
[64] 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. [ bib | DOI | Isabelle files ]
[65] 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. [ bib | DOI ]
[66] 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. [ bib | DOI ]
[67] 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. [ bib | DOI ]
[68] 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. [ bib | DOI ]
[69] 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. [ bib | DOI ]
[70] 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. [ bib ]
[71] B. Dongol and J. Derrick. Simplifying proofs of linearisability using layers of abstraction. ECEASST, 66, 2013. [ bib ]
[72] 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. [ bib ]
[73] 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. [ bib ]
[74] B. Dongol, J. Derrick, and I. J. Hayes. Fractional permissions and non-deterministic evaluators in interval temporal logic. ECEASST, 53, 2012. [ bib ]
[75] 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. [ bib ]
[76] 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. [ bib ]
[77] 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. [ bib ]
[78] 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. [ bib ]
[79] 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. [ bib ]
[80] 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. [ bib ]
[81] 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. [ bib ]
[82] 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. [ bib ]
[83] B. Dongol. Towards simpler proofs of lock-freedom. In Preliminary Proceedings of the 1st Asian Working Conference on Verified Software, pages 136--146, 2006. [ bib ]
[84] B. Dongol. Derivation of Java monitors. In ASWEC, pages 211--220. IEEE Computer Society, 2006. [ bib ]
[85] 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. [ bib ]
[86] 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. [ bib ]

Other

PhD Thesis

[87] 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. [ bib | .pdf ]

Technical reports (not elsewhere published)

[88] B. Dongol and J. Derrick. Proving linearisability via coarse-grained abstraction. CoRR, abs/1212.5116, 2012. [ bib | arXiv ]
[89] 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. [ bib ]
[90] 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. [ bib | http ]
[91] B. Dongol, V. B. F. Gomes, I. J. Hayes, and G. Struth. Partial semigroups and convolution algebras. Archive of Formal Proofs, 2017, 2017. [ bib | http ]

This file was generated by bibtex2html 1.99.