Edited Proceedings

[1] J. Derrick, B. Dongol, and S. Reeves, editors. Proceedings 19th Refinement Workshop, Refine@FM 2019, Porto, UK, 2019. [ bib ]
[2] 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 Lecture Notes in Computer Science. Springer, 2019. [ bib | DOI | http ]
[3] 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

[4] 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

[5] T. Y. Lam and Brijesh Dongol. A blockchain-enabled e-learning platform. Interactive Learning Environments, 0(0):1--23, 2020. [ bib | DOI | arXiv | http ]
[6] B. Dongol, R. Jagadeesan, and J. Riely. Transactions in relaxed memory architectures. PACMPL, 2(POPL):18:1--18:29, 2018. [ bib ]
[7] B. Dongol and R. M. Hierons. Decidability and complexity for quiescent consistency and its variations. Inf. Comput., 257:1--21, 2017. [ bib ]
[8] 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. Mechanisations available here: https://swt.informatik.uni-augsburg.de/swt/projects/Opacity-TML.html. [ bib ]
[9] 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 ]
[10] B. Dongol and J. Derrick. Verifying linearisability: A comparative survey. ACM Comput. Surv., 48(2):19, 2015. [ bib | DOI | http ]
[11] 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 ]
[12] 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 ]
[13] 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 ]
[14] 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 ]
[15] B. Dongol and I. J. Hayes. Deriving real-time action systems in a sampling logic. Sci. Comput. Program., 78(11):2047--2063, 2013. [ bib ]
[16] R. Colvin and B. Dongol. A general technique for proving lock-freedom. Sci. Comput. Program., 74(3):143--165, 2009. [ bib | PVS files ]
[17] B. Dongol and A. J. Mooij. Streamlining progress-based derivations of concurrent programs. Formal Asp. Comput., 20(2):141--160, 2008. [ bib ]
[18] 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

[19] Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, and Heike Wehrheim. Defining and verifying durable opacity: Correctness for persistent software transactional memory. In FORTE, 2020. [ bib | DOI | www: ]
[20] S. Dalvandi, Simon Doherty, and Brijesh Dongol Heike Wehrheim. Owicki-gries reasoning for c11 rar. In ECOOP, 2020. [ bib | DOI | www: ]
[21] John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim. Verifying correctness of persistent concurrent data structures. In Maurice H. ter Beek, Annabelle McIver, and José N. Oliveira, editors, Formal Methods - The Next 30 Years - Third World Congress, FM 2019, Porto, Portugal, October 7-11, 2019, Proceedings, volume 11800 of Lecture Notes in Computer Science, pages 179--195. Springer, 2019. [ bib | DOI | http ]
[22] K. Clark, B. Dongol, and P. Robinson. A temporal logic semantics for teleo-reactive procedures. In FMAS, 2019. To appear. [ bib ]
[23] Brijesh Dongol, Ian J. Hayes, Larissa Meinicke, and Georg Struth. Cylindric kleene lattices for program construction. In Graham Hutton, editor, Mathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Proceedings, volume 11825 of Lecture Notes in Computer Science, pages 197--225. Springer, 2019. [ bib | DOI | http ]
[24] 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 ]
[25] B. Dongol, R. Jagadeesan, and J. Riely. Modular transactions: bounding mixed races in space and time. In PPoPP, pages 82--93. ACM, 2019. [ bib ]
[26] S. Doherty, B. Dongol, H. Wehrheim, and J. Derrick. Verifying C11 programs operationally. In PPoPP, pages 355--365. ACM, 2019. [ bib | Full version ]
[27] 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 ]
[28] 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 ]
[29] 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 ]
[30] 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 ]
[31] 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). [ bib | Isabelle files ]
[32] 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. Further Isabelle details Isabelle/MSPessTM.html. [ bib | Isabelle files ]
[33] 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 ]
[34] 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. [ bib ]
[35] B. Dongol and R. M. Hierons. Decidability and complexity for quiescent consistency. In LICS, pages 116--125. ACM, 2016. [ bib ]
[36] 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 ]
[37] 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 ]
[38] 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 ]
[39] 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 ]
[40] 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 ]
[41] 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 ]
[42] 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 ]
[43] 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 ]
[44] 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 ]
[45] B. Dongol and J. Derrick. Simplifying proofs of linearisability using layers of abstraction. ECEASST, 66, 2013. [ bib ]
[46] 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 ]
[47] 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 ]
[48] B. Dongol, J. Derrick, and I. J. Hayes. Fractional permissions and non-deterministic evaluators in interval temporal logic. ECEASST, 53, 2012. [ bib ]
[49] 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 ]
[50] 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 ]
[51] 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 ]
[52] 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 ]
[53] 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 ]
[54] 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 ]
[55] 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 ]
[56] 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 ]
[57] 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 ]
[58] B. Dongol. Derivation of Java monitors. In ASWEC, pages 211--220. IEEE Computer Society, 2006. [ bib ]
[59] 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 ]
[60] 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

[61] 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)

[62] B. Dongol, I. J. Hayes, and G. Struth. Relational Convolution, Generalised Modalities and Incidence Algebras. ArXiv e-prints, February 2017. [ bib | arXiv ]
[63] B. Dongol and J. Derrick. Proving linearisability via coarse-grained abstraction. CoRR, abs/1212.5116, 2012. [ bib ]
[64] 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 ]
[65] 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 ]
[66] 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.