@article{DBLP:journals/fac/DongolT22,
author = {B. Dongol and
E. Troubitsyna},
title = {Introduction to the Special Section on {iFM} 2020},
journal = {Formal Aspects Comput.},
volume = {34},
number = {1},
pages = {1},
year = {2022},
url = {https://doi.org/10.1145/3546592},
doi = {10.1145/3546592},
timestamp = {Tue, 17 Jan 2023 16:47:15 +0100},
biburl = {https://dblp.org/rec/journals/fac/DongolT22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{Robosoft,
editor = {A. Cavalcanti and B. Dongol and R. Heirons and J. Timmis and J. Woodcock},
title = {Software Engineering for Robotics},
publisher = {Springer},
year = {2021},
optkey = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
optedition = {},
optmonth = {},
optnote = {},
optannote = {}
}
@proceedings{DBLP:conf/ifm/2020,
editor = {B. Dongol and
E. Troubitsyna},
title = {{Integrated Formal Methods} - 16th International Conference, {IFM} 2020,
Lugano, Switzerland, November 16-20, 2020, Proceedings},
series = {LNCS},
volume = {12546},
publisher = {Springer},
year = {2020},
ourl = {https://doi.org/10.1007/978-3-030-63461-2},
odoi = {10.1007/978-3-030-63461-2},
isbn = {978-3-030-63460-5},
otimestamp = {Tue, 17 Nov 2020 15:21:11 +0100},
obiburl = {https://dblp.org/rec/conf/ifm/2020.bib},
obibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/fm/2019-w1,
editor = {E. Sekerinski and
N. Moreira and
J. N. Oliveira and
D. Ratiu and
R. Guidotti and
M. Farrell and
M. Luckcuck and
D. Marmsoler and
J. Campos and
T. Astarte and
L. Gonnord and
A. Cerone and
L. Couto and
B. Dongol and
M. Kutrib and
P. Monteiro and
D. Delmas},
title = {Formal Methods. {FM} 2019 International Workshops - Porto, Portugal,
October 7-11, 2019, Revised Selected Papers, Part {I}},
series = {LNCS},
volume = {12232},
publisher = {Springer},
year = {2020},
url = {https://doi.org/10.1007/978-3-030-54994-7},
doi = {10.1007/978-3-030-54994-7},
isbn = {978-3-030-54993-0},
timestamp = {Mon, 17 Aug 2020 17:09:20 +0200},
biburl = {https://dblp.org/rec/conf/fm/2019-w1.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{Refine-2019,
editor = {J. Derrick and
B. Dongol and
S. Reeves},
title = {Proceedings 19th Refinement Workshop, Refine@FM 2019, Porto, UK},
oseries = {{EPTCS}},
ovolume = {282},
year = {2019},
ourl = {https://doi.org/10.4204/EPTCS.282},
odoi = {10.4204/EPTCS.282},
otimestamp = {Tue, 04 Dec 2018 16:00:11 +0100},
obiburl = {https://dblp.org/rec/bib/journals/corr/abs-1810-08739},
obibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/tfm/2019,
editor = {B. Dongol and
L. Petre and
G. Smith},
title = {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},
series = {LNCS},
volume = {11758},
publisher = {Springer},
year = {2019},
url = {https://doi.org/10.1007/978-3-030-32441-4},
doi = {10.1007/978-3-030-32441-4},
isbn = {978-3-030-32440-7},
timestamp = {Wed, 25 Sep 2019 12:57:12 +0200},
biburl = {https://dblp.org/rec/bib/conf/tfm/2019},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{abs-1810-08739,
editor = {J. Derrick and
B. Dongol and
S. Reeves},
title = {Proceedings 18th Refinement Workshop, Refine@FM 2018, Oxford, UK,
18th July 2018},
series = {{EPTCS}},
volume = {282},
year = {2018},
url = {https://doi.org/10.4204/EPTCS.282},
doi = {10.4204/EPTCS.282},
timestamp = {Tue, 04 Dec 2018 16:00:11 +0100},
biburl = {https://dblp.org/rec/bib/journals/corr/abs-1810-08739},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inbook{Dongol2024,
author = {Dongol, B.
and Lahav, O.
and Wehrheim, H.},
title = {A Rely-Guarantee Framework for Proving Deadlock Freedom under Causal Consistency},
booktitle = {Festschrift Cliff Jones},
year = {2024},
publisher = {Springer},
volume = 14780
}
@inbook{Dongol2021,
author = {Dongol, B.
and Bell, R.
and Habli, I.
and Lawford, M.
and Moore, P.
and Saigol, Z.},
title = {Panel Discussion: Regulation and Ethics of Robotics and Autonomous Systems},
booktitle = {Software Engineering for Robotics},
year = {2021},
publisher = {Springer International Publishing},
address = {Cham},
pages = {467--483},
oabstract = {This chapter summarises a panel discussion on the topics of Regulation and Ethics in Software Engineering for Robotics at RoboSoft, chaired by Jon Timmis (University of Sunderland). The panel members were Ron Bell (Engineering Safety Consultants), Mark Lawford (McMaster University), Ibrahim Habli (University of York), and Pippa Moore (Civil Aviation Authority), whose views are summarised below. The chapter also integrates the issues raised in a talk on ``Extending automotive certification processes to handle autonomous vehicles'' by Zeyn Saigol (Connected Places Catapult), which provides a case study for the issues being discussed.},
isbn = {978-3-030-66494-7},
doi = {10.1007/978-3-030-66494-7_14},
url = {https://doi.org/10.1007/978-3-030-66494-7_14}
}
@incollection{DBLP:books/sp/17/DerrickSGD17,
author = {J. Derrick and
G. Smith and
L. Groves and
B. Dongol},
title = {A Proof Method for Linearizability on {TSO} Architectures},
booktitle = {Provably Correct Systems},
series = {{NASA} Monographs in Systems and Software Engineering},
pages = {61--91},
publisher = {Springer},
year = {2017}
}
@article{OOPSLA-24,
author = {G. Ambal and B. Dongol and H. Eran and V. Klimis and O. Lahav and A. Raad},
title = {Semantics of Remote Direct Memory Access: Operational and Declarative Models of {RDMA} on {TSO} Architectures},
journal = {Proc. ACM Program. Lang.},
volume = {6(OOPSLA2)},
pages = {},
year = {2024},
note = {To Appear}
}
@article{FMSD,
author = {E. Bila and B. Dongol},
title = {A Verified Durable Transactional Mutex Lock for Persistent x86-TSO},
journal = {Formal Methods in System Design},
volume = {},
pages = {},
year = {2024},
note = {To appear}
}
@article{10.1145/3670419,
author = {Dongol, B. and Dubois, C. and Hallerstede, S. and Hehner, E. and Morgan, C. and M\"{u}ller, P. and Ribeiro, L. and Silva, A. and Smith, G. and de Vink, E.},
title = {On Formal Methods Thinking in Computer Science Education},
year = {2024},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
issn = {0934-5043},
url = {https://doi.org/10.1145/3670419},
doi = {10.1145/3670419},
note = {Just Accepted},
journal = {Form. Asp. Comput.},
month = {jun}
}
@article{DBLP:journals/scp/AhmadiDG24,
author = {Sharar Ahmadi and
Brijesh Dongol and
Matt Griffin},
title = {Operationally proving memory access violations in Isabelle/HOL},
journal = {Sci. Comput. Program.},
volume = {234},
pages = {103088},
year = {2024},
url = {https://doi.org/10.1016/j.scico.2024.103088},
doi = {10.1016/J.SCICO.2024.103088},
timestamp = {Thu, 30 May 2024 10:59:09 +0200},
biburl = {https://dblp.org/rec/journals/scp/AhmadiDG24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fac/WrightDBD23,
author = {Daniel Wright and
Sadegh Dalvandi and
Mark Batty and
Brijesh Dongol},
title = {Mechanised Operational Reasoning for {C11} Programs with Relaxed Dependencies},
journal = {Formal Aspects Comput.},
volume = {35},
number = {2},
pages = {10:1--10:27},
year = {2023},
url = {https://doi.org/10.1145/3580285},
doi = {10.1145/3580285},
timestamp = {Wed, 06 Dec 2023 18:19:51 +0100},
biburl = {https://dblp.org/rec/journals/fac/WrightDBD23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{OOPSLA-22,
author = {S. Dalvandi and B. Dongol},
title = {Implementing and verifying release-acquire transactional memory in {C11}},
journal = {Proc. ACM Program. Lang.},
volume = {6(OOPSLA2)},
pages = {1817-1844},
year = {2022}
}
@article{DBLP:journals/lmcs/BilaDDDSW22,
author = {E. Bila and
J. Derrick and
S. Doherty and
B. Dongol and
G. Schellhorn and
H. Wehrheim},
title = {Modularising Verification Of Durable Opacity},
journal = {Log. Methods Comput. Sci.},
volume = {18},
number = {3},
year = {2022},
url = {https://doi.org/10.46298/lmcs-18(3:7)2022},
doi = {10.46298/lmcs-18(3:7)2022},
timestamp = {Tue, 24 Jan 2023 10:48:24 +0100},
biburl = {https://dblp.org/rec/journals/lmcs/BilaDDDSW22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tocl/DohertyDDW22,
author = {S. Doherty and
S. Dalvandi and
B. Dongol and
H. Wehrheim},
title = {Unifying Operational Weak Memory Verification: An Axiomatic Approach},
journal = {{ACM} Trans. Comput. Log.},
volume = {23},
number = {4},
pages = {27:1--27:39},
year = {2022},
url = {https://doi.org/10.1145/3545117},
doi = {10.1145/3545117},
timestamp = {Mon, 05 Dec 2022 13:35:14 +0100},
biburl = {https://dblp.org/rec/journals/tocl/DohertyDDW22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fac/KulikDLMSTW22,
author = {T. Kulik and
B. Dongol and
P. Gorm Larsen and
H. Daniel Macedo and
S. Schneider and
P. D. W. V. Tran{-}J{\o}rgensen and
J. Woodcock},
title = {A Survey of Practical Formal Methods for Security},
journal = {Formal Aspects Comput.},
volume = {34},
number = {1},
pages = {1--39},
year = {2022},
url = {https://doi.org/10.1145/3522582},
doi = {10.1145/3522582},
timestamp = {Fri, 17 Feb 2023 09:02:03 +0100},
biburl = {https://dblp.org/rec/journals/fac/KulikDLMSTW22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/DalvandiDDW22,
author = {S. Dalvandi and
B. Dongol and
S. Doherty and
H. Wehrheim},
title = {Integrating {Owicki-Gries} for {C11-Style} Memory Models into {Isabelle/HOL}},
journal = {J. Autom. Reason.},
volume = {66},
number = {1},
pages = {141--171},
year = {2022},
url = {https://doi.org/10.1007/s10817-021-09610-2},
doi = {10.1007/s10817-021-09610-2},
timestamp = {Fri, 21 Jan 2022 22:01:13 +0100},
biburl = {https://dblp.org/rec/journals/jar/DalvandiDDW22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/fac/DerrickDDSW21,
author = {J. Derrick and
S. Doherty and
B. Dongol and
G. Schellhorn and
H. Wehrheim},
title = {Verifying correctness of persistent concurrent data structures: a
sound and complete method},
journal = {Formal Aspects Comput.},
volume = {33},
number = {4-5},
pages = {547--573},
year = {2021},
url = {https://doi.org/10.1007/s00165-021-00541-8},
doi = {10.1007/s00165-021-00541-8},
timestamp = {Wed, 05 Jan 2022 16:46:09 +0100},
biburl = {https://dblp.org/rec/journals/fac/DerrickDDSW21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/lmcs/DongolHS21,
author = {B. Dongol and
I. J. Hayes and
G. Struth},
title = {Convolution Algebras: Relational Convolution, Generalised Modalities
and Incidence Algebras},
journal = {Log. Methods Comput. Sci.},
volume = {17},
number = {1},
year = {2021},
url = {https://lmcs.episciences.org/7164},
timestamp = {Mon, 08 Mar 2021 17:46:18 +0100},
biburl = {https://dblp.org/rec/journals/lmcs/DongolHS21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{doi:10.1080/10494820.2020.1716022,
author = {T. Y. Lam and B. Dongol},
title = {A blockchain-enabled e-learning platform},
journal = {Interactive Learning Environments},
volume = {0},
number = {0},
pages = {1-23},
year = {2020},
publisher = {Routledge},
doi = {10.1080/10494820.2020.1716022},
url = {https://doi.org/10.1080/10494820.2020.1716022}
}
@article{DBLP:journals/pacmpl/DongolJR18,
author = {B. Dongol and
R. Jagadeesan and
J. Riely},
title = {Transactions in relaxed memory architectures},
journal = {{PACMPL}},
volume = {2},
number = {{POPL}},
pages = {18:1--18:29},
year = {2018}
}
@article{DBLP:journals/iandc/DongolH17,
author = {B. Dongol and
R. M. Hierons},
title = {Decidability and complexity for quiescent consistency and its variations},
journal = {Inf. Comput.},
volume = {257},
pages = {1--21},
year = {2017}
}
@article{DDDSTW17,
author = {J. Derrick and
S. Doherty and
B. Dongol and
G. Schellhorn and
O. Travkin and
H. Wehrheim},
title = {Mechanized proofs of opacity: a comparison of two techniques},
journal = {Formal Asp. Comput.},
volume = 30,
number = 5,
pages = {597--625},
year = 2018,
mechanisation = {https://swt.informatik.uni-augsburg.de/swt/projects/Opacity-TML.html}
}
@article{DongolHS16,
author = {B. Dongol and
I. J. Hayes and
G. Struth},
title = {Convolution as a Unifying Concept: Applications in Separation Logic,
Interval Calculi, and Concurrency},
journal = {{ACM} Trans. Comput. Log.},
volume = {17},
number = {3},
pages = {15:1--15:25},
year = {2016}
}
@article{DongolD15-CSUR,
author = {B. Dongol and
J. Derrick},
title = {Verifying Linearisability: {A} Comparative Survey},
journal = {{ACM} Comput. Surv.},
volume = {48},
number = {2},
pages = {19},
year = {2015},
url = {http://doi.acm.org/10.1145/2796550},
doi = {10.1145/2796550},
timestamp = {Tue, 08 Dec 2015 19:11:17 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/csur/DongolD15},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/scp/DongolD15,
author = {B. Dongol and
J. Derrick},
title = {Interval-based data refinement: {A} uniform approach to true concurrency
in discrete and real-time systems},
journal = {Sci. Comput. Program.},
volume = {111},
pages = {214-247},
year = {2015},
url = {http://dx.doi.org/10.1016/j.scico.2015.05.005},
doi = {10.1016/j.scico.2015.05.005},
timestamp = {Wed, 13 Jan 2016 12:54:06 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/scp/DongolD15},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@article{DBLP:journals/fac/DongolHR14,
author = {B. Dongol and
I. J. Hayes and
P. J. Robinson},
title = {Reasoning about goal-directed real-time teleo-reactive programs},
journal = {Formal Asp. Comput.},
volume = {26},
number = {3},
year = {2014},
pages = {563-589},
ee = {http://dx.doi.org/10.1007/s00165-012-0272-1},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/scp/DongolHD14,
author = {B. Dongol and
I. J. Hayes and
J. Derrick},
title = {Deriving real-time action systems with multiple time bands
using algebraic reasoning},
journal = {Sci. Comput. Program.},
volume = {85},
year = {2014},
pages = {137-165},
ee = {http://dx.doi.org/10.1016/j.scico.2013.08.009},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/cj/HayesBDJ13,
author = {I. J. Hayes and
A. Burns and
B. Dongol and
C. B. Jones},
title = {Comparing Degrees of Non-Determinism in Expression Evaluation},
journal = {Comput. J.},
volume = {56},
number = {6},
year = {2013},
pages = {741-755},
ee = {http://dx.doi.org/10.1093/comjnl/bxt005},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DH13-MPCj,
author = {B. Dongol and
I. J. Hayes},
title = {Deriving real-time action systems in a sampling logic},
journal = {Sci. Comput. Program.},
volume = {78},
number = {11},
year = {2013},
pages = {2047-2063},
ee = {http://dx.doi.org/10.1016/j.scico.2012.07.008},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/scp/ColvinD09,
author = {R. Colvin and
B. Dongol},
title = {A general technique for proving lock-freedom},
journal = {Sci. Comput. Program.},
volume = 74,
number = 3,
year = 2009,
pages = {143-165},
ee = {http://dx.doi.org/10.1016/j.scico.2008.09.013},
bibsource = {DBLP, http://dblp.uni-trier.de},
pvs = {mechanisation/SCP-2009-PVS.zip}
}
@article{DBLP:journals/fac/DongolM08,
author = {B. Dongol and
A. J. Mooij},
title = {Streamlining progress-based derivations of concurrent programs},
journal = {Formal Asp. Comput.},
volume = 20,
number = 2,
year = 2008,
pages = {141-160},
ee = {http://dx.doi.org/10.1007/s00165-007-0037-4},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/lmcs/DongolG06,
author = {B. Dongol and
D. Goldson},
title = {Extending the theory of {Owicki and Gries} with a logic of
progress},
journal = {Logical Methods in Computer Science},
volume = 2,
number = 1,
year = 2006,
ee = {http://dx.doi.org/10.2168/LMCS-2(1:6)2006},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DISC24,
author = {Armando Castenada and
Gregory V. Chockler and
Brijesh Dongol and
Ori Lahav},
editor = {},
title = {What Cannot Be Implemented on Weak Memory?},
booktitle = {DISC},
pages = {},
publisher = {},
year = {2024},
note = {To appear}
}
@inproceedings{FM24,
author = {L. Bargmann and
B. Dongol and
H. Wehrheim},
editor = {},
title = {Unifying Weak Memory Verification using Potentials},
booktitle = {FM},
pages = {},
publisher = {},
year = {2024},
note = {To appear}
}
@inproceedings{CSF24,
author = {B. Dongol and M. Griffin and A. Popescu and J. Wright},
booktitle = {CSF},
title = {Relative Security: Formally Modeling and (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities},
year = {2024},
volume = {},
issn = {2374-8303},
pages = {409-424},
doi = {10.1109/CSF61375.2024.00027},
url = {https://doi.ieeecomputersociety.org/10.1109/CSF61375.2024.00027},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
month = {jul}
}
@inproceedings{DBLP:conf/usenix/EgorovCDOK24,
author = {S. Egorov and
G. V. Chockler and
B. Dongol and
D. O'Keeffe and
S. Keshavarzi},
editor = {S. Bagchi and
Y. Zhang},
title = {Mangosteen: Fast Transparent Durability for Linearizable Applications
using {NVM}},
booktitle = {Proceedings of the 2024 {USENIX} Annual Technical Conference, {USENIX}
{ATC} 2024, Santa Clara, CA, USA, July 10-12, 2024},
pages = {799--815},
publisher = {{USENIX} Association},
year = {2024},
url = {https://www.usenix.org/conference/atc24/presentation/egorov},
timestamp = {Tue, 16 Jul 2024 22:11:07 +0200},
biburl = {https://dblp.org/rec/conf/usenix/EgorovCDOK24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/esop/RaadLWBD24,
author = {A. Raad and
O. Lahav and
J. Wickerson and
P. Balcer and
B. Dongol},
editor = {S. Weirich},
title = {Intel {PMDK} Transactions: Specification, Validation and Concurrency},
booktitle = {ESOP},
series = {LNCS},
volume = {14577},
pages = {150--179},
publisher = {Springer},
year = {2024},
url = {https://doi.org/10.1007/978-3-031-57267-8\_6},
doi = {10.1007/978-3-031-57267-8\_6},
timestamp = {Sat, 04 May 2024 10:54:46 +0200},
biburl = {https://dblp.org/rec/conf/esop/RaadLWBD24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/esop/RaadLWBD24a,
author = {A. Raad and
O. Lahav and
J. Wickerson and
P. Balcer and
B. Dongol},
editor = {S. Weirich},
title = {Artifact Report: Intel {PMDK} Transactions: Specification, Validation
and Concurrency},
booktitle = {ESOP},
series = {LNCS},
volume = 14577,
pages = {180--184},
publisher = {Springer},
year = 2024,
url = {https://doi.org/10.1007/978-3-031-57267-8\_7},
doi = {10.1007/978-3-031-57267-8\_7},
timestamp = {Sat, 04 May 2024 10:54:46 +0200},
biburl = {https://dblp.org/rec/conf/esop/RaadLWBD24a.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{VMCAI2023,
author = {S. Bodenmüller and J. Derrick and B. Dongol and G. Schellhorn and H. Wehrheim},
editor = {},
title = {A Fully Verified Persistency Library},
booktitle = {VMCAI},
series = {LNCS},
volume = {},
pages = {},
publisher = {Springer},
year = {2024},
url = {},
doi = {},
eprint = {}
}
@inproceedings{DBLP:conf/sefm/SemenyukBD23,
author = {M. Semenyuk and
M. Batty and
B. Dongol},
editor = {C. Ferreira and
T. A. C. Willemse},
title = {Verifying Read-Copy Update Under {RC11}},
booktitle = {{SEFM}},
series = {LNCS},
volume = 14323,
pages = {301--319},
publisher = {Springer},
year = 2023,
url = {https://doi.org/10.1007/978-3-031-47115-5\_17},
doi = {10.1007/978-3-031-47115-5\_17},
timestamp = {Mon, 13 Nov 2023 20:30:30 +0100},
biburl = {https://dblp.org/rec/conf/sefm/SemenyukBD23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cav/LahavDW23,
author = {O. Lahav and
B. Dongol and
H. Wehrheim},
editor = {C. Enea and
A. Lal},
title = {Rely-Guarantee Reasoning for Causally Consistent Shared Memory},
booktitle = {{CAV}},
series = {LNCS},
volume = 13964,
pages = {206--229},
publisher = {Springer},
year = 2023,
url = {https://doi.org/10.1007/978-3-031-37706-8\_11},
doi = {10.1007/978-3-031-37706-8\_11},
timestamp = {Sat, 05 Aug 2023 00:01:30 +0200},
biburl = {https://dblp.org/rec/conf/cav/LahavDW23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fm/WehrheimBD23,
author = {H. Wehrheim and
L. Bargmann and
B. Dongol},
editor = {M. Chechik and
J.{-}P. Katoen and
M. Leucker},
title = {Reasoning About Promises in Weak Memory Models with Event Structures},
booktitle = {{FM}},
series = {LNCS},
volume = 14000,
pages = {282--300},
publisher = {Springer},
year = 2023,
url = {https://doi.org/10.1007/978-3-031-27481-7\_17},
doi = {10.1007/978-3-031-27481-7\_17},
timestamp = {Sat, 11 Mar 2023 00:11:48 +0100},
biburl = {https://dblp.org/rec/conf/fm/WehrheimBD23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/wisec/Le-PapinDTW23,
author = {J. Le{-}Papin and
B. Dongol and
H. Treharne and
S. Wesemeyer},
editor = {I. Boureanu and
S. Schneider and
B. Reaves and
N. Ole Tippenhauer},
title = {Verifying List Swarm Attestation Protocols},
booktitle = {{ACM} WiSec},
pages = {163--174},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3558482.3581778},
doi = {10.1145/3558482.3581778},
timestamp = {Fri, 07 Jul 2023 23:30:24 +0200},
biburl = {https://dblp.org/rec/conf/wisec/Le-PapinDTW23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/sac/SemenyukD23,
author = {M. Semenyuk and
B. Dongol},
editor = {J. Hong and
M. Lanperne and
J. W. Park and
T. Cern{\'{y}} and
H. Shahriar},
title = {Ownership-Based {Owicki-Gries} Reasoning},
booktitle = {{ACM/SIGAPP}
{SAC}},
pages = {1685--1694},
publisher = {{ACM}},
year = {2023},
url = {https://doi.org/10.1145/3555776.3577636},
doi = {10.1145/3555776.3577636},
timestamp = {Fri, 21 Jul 2023 22:25:35 +0200},
biburl = {https://dblp.org/rec/conf/sac/SemenyukD23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ftscs/AhmadiDG22,
author = {S. Ahmadi and
B. Dongol and
M. Griffin},
editor = {C. Artho and
P. C. {\"{O}}lveczky},
title = {Proving Memory Access Violations in {Isabelle/HOL}},
booktitle = {{FTSCS}},
pages = {45--55},
publisher = {{ACM}},
year = {2022},
url = {https://doi.org/10.1145/3563822.3568010},
doi = {10.1145/3563822.3568010},
timestamp = {Mon, 05 Dec 2022 10:14:57 +0100},
biburl = {https://dblp.org/rec/conf/ftscs/AhmadiDG22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/concur/DongolSW22,
author = {B. Dongol and
G. Schellhorn and
H. Wehrheim},
editor = {B. Klin and
S. Lasota and
A. Muscholl},
title = {Weak Progressive Forward Simulation Is Necessary and Sufficient for
Strong Observational Refinement},
booktitle = {CONCUR},
series = {LIPIcs},
volume = {243},
pages = {31:1--31:23},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2022},
url = {https://doi.org/10.4230/LIPIcs.CONCUR.2022.31},
doi = {10.4230/LIPIcs.CONCUR.2022.31},
timestamp = {Mon, 26 Sep 2022 17:09:13 +0200},
biburl = {https://dblp.org/rec/conf/concur/DongolSW22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-2201-05860,
author = {E. Vafeiadi Bila and
B. Dongol and
O. Lahav and
A. Raad and
J. Wickerson},
editor = {I. Sergey},
title = {View-Based {Owicki-Gries} Reasoning for Persistent {x86-TSO}},
booktitle = {ESOP},
series = {LNCS},
volume = {13240},
pages = {234--261},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-030-99336-8\_9},
doi = {10.1007/978-3-030-99336-8\_9},
note = {{\bf Distinguished artifact award}},
eprint = {2201.05860}
}
@inproceedings{DBLP:conf/sefm/DongolL21,
author = {B. Dongol and
J. Le{-}Papin},
editor = {R. Calinescu and
C. S. Pasareanu},
title = {Checking Opacity and Durable Opacity with {FDR}},
booktitle = {SEFM},
series = {LNCS},
volume = {13085},
pages = {222--242},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-92124-8\_13},
doi = {10.1007/978-3-030-92124-8\_13},
timestamp = {Tue, 07 Dec 2021 17:02:17 +0100},
biburl = {https://dblp.org/rec/conf/sefm/DongolL21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fm/WrightBD21,
author = {D. Wright and
M. Batty and
B. Dongol},
editor = {M. Huisman and
C. S. Pasareanu and
N. Zhan},
title = {{Owicki-Gries} Reasoning for {C11} Programs with Relaxed Dependencies},
booktitle = {FM},
series = {LNCS},
volume = {13047},
pages = {237--254},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-90870-6\_13},
doi = {10.1007/978-3-030-90870-6\_13},
timestamp = {Thu, 11 Nov 2021 16:19:19 +0100},
biburl = {https://dblp.org/rec/conf/fm/WrightBD21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fm/GriffinD21,
author = {M. Griffin and
B. Dongol},
editor = {M. Huisman and
C. S. Pasareanu and
N. Zhan},
title = {Verifying Secure Speculation in {Isabelle/HOL}},
booktitle = {FM},
series = {LNCS},
volume = {13047},
pages = {43--60},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-90870-6\_3},
doi = {10.1007/978-3-030-90870-6\_3},
timestamp = {Wed, 15 Dec 2021 10:33:04 +0100},
biburl = {https://dblp.org/rec/conf/fm/GriffinD21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ppopp/DalvandiD21,
author = {S. Dalvandi and
B. Dongol},
editor = {Jaejin Lee and
Erez Petrank},
title = {Verifying {C11-style} weak memory libraries},
booktitle = {PPoPP},
pages = {451--453},
publisher = {{ACM}},
year = 2021,
url = {https://doi.org/10.1145/3437801.3441619},
doi = {10.1145/3437801.3441619},
timestamp = {Wed, 24 Feb 2021 18:09:33 +0100},
biburl = {https://dblp.org/rec/conf/ppopp/DalvandiD21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{BDDDSW20,
author = {E. Bila and S. Doherty and B. Dongol and J. Derrick and G. Schellhorn and H. Wehrheim},
editor = {},
title = {Defining and Verifying Durable Opacity: {Correctness} for Persistent Software Transactional Memory},
booktitle = {FORTE},
series = {},
volume = {},
pages = {},
publisher = {},
year = {2020},
note = {{\bf Best paper award.}},
doi = {}
}
@inproceedings{DDDW20,
author = {S. Dalvandi and
S. Doherty and
B. Dongol and
H. Wehrheim},
editor = {},
title = {{Owicki-Gries} Reasoning for {C11 RAR}},
booktitle = {ECOOP},
series = {},
volume = {},
pages = {},
publisher = {},
year = {2020},
url = {},
doi = {}
}
@inproceedings{DBLP:conf/fm/DerrickDDSW19,
author = {J. Derrick and
S. Doherty and
B. Dongol and
G. Schellhorn and
H. Wehrheim},
editor = {M. H. ter Beek and
A. McIver and
J. N. Oliveira},
title = {Verifying Correctness of Persistent Concurrent Data Structures},
booktitle = {FM},
series = {LNCS},
volume = {11800},
pages = {179--195},
publisher = {Springer},
year = {2019},
url = {https://doi.org/10.1007/978-3-030-30942-8\_12},
doi = {10.1007/978-3-030-30942-8\_12},
timestamp = {Mon, 23 Sep 2019 13:52:37 +0200},
biburl = {https://dblp.org/rec/bib/conf/fm/DerrickDDSW19},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fm/ClarkDR19,
author = {K. Clark and
B. Dongol and
P. Robinson},
editor = {},
title = {Temporal Logic Semantics for Teleo-Reactive Robotic Agent Programs},
booktitle = {Formal Methods. {FM} 2019 International Workshops - Porto, Portugal,
October 7-11, 2019, Revised Selected Papers, Part {I}},
series = {LNCS},
volume = {12232},
pages = {265--280},
publisher = {Springer},
year = {2019},
url = {https://doi.org/10.1007/978-3-030-54994-7\_19},
doi = {10.1007/978-3-030-54994-7\_19},
timestamp = {Wed, 09 Sep 2020 16:57:55 +0200},
biburl = {https://dblp.org/rec/conf/fm/ClarkDR19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mpc/DongolHMS19,
author = {B. Dongol and
I. J. Hayes and
L. Meinicke and
G. Struth},
editor = {G. Hutton},
title = {Cylindric Kleene Lattices for Program Construction},
booktitle = {MPC},
series = {LNCS},
volume = {11825},
pages = {197--225},
publisher = {Springer},
year = {2019},
url = {https://doi.org/10.1007/978-3-030-33636-3\_8},
doi = {10.1007/978-3-030-33636-3\_8},
timestamp = {Thu, 07 Nov 2019 09:20:32 +0100},
biburl = {https://dblp.org/rec/bib/conf/mpc/DongolHMS19},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DD19,
author = {M. Dalvandi and B. Dongol},
title = {Towards Deductive Verification of {C11} Programs with {Event-B} and {ProB}},
optcrossref = {},
optkey = {},
booktitle = {FTfJP},
year = {2019},
editor = {G. Ernst and T. Murray},
optvolume = {},
optnumber = {},
optseries = {},
optpages = {},
optmonth = {},
optaddress = {},
optorganization = {},
publisher = {ACM},
optnote = {},
optannote = {}
}
@inproceedings{DBLP:conf/ppopp/DongolJR19,
author = {B. Dongol and
R. Jagadeesan and
J. Riely},
title = {Modular transactions: bounding mixed races in space and time},
booktitle = {PPoPP},
pages = {82--93},
publisher = {{ACM}},
year = {2019}
}
@inproceedings{DBLP:conf/ppopp/DohertyDWD19,
author = {S. Doherty and
B. Dongol and
H. Wehrheim and
J. Derrick},
title = {Verifying {C11} programs operationally},
booktitle = {PPoPP},
pages = {355--365},
publisher = {{ACM}},
year = 2019,
fullversion = {full-version/PPoPP-2019-full.pdf}
}
@inproceedings{DohertyDWD18,
author = {S. Doherty and
B. Dongol and
H. Wehrheim and
J. Derrick},
editor = {U. Schmid and
J. Widder},
title = {Brief Announcement: Generalising Concurrent Correctness to Weak Memory},
booktitle = {DISC},
series = {LIPIcs},
volume = {121},
pages = {45:1--45:3},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
year = {2018},
url = {https://doi.org/10.4230/LIPIcs.DISC.2018.45},
doi = {10.4230/LIPIcs.DISC.2018.45},
timestamp = {Tue, 09 Oct 2018 13:57:40 +0200},
biburl = {https://dblp.org/rec/bib/conf/wdag/DohertyDWD18},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ifm/DohertyDWD18,
author = {S. Doherty and
B. Dongol and
H. Wehrheim and
J. Derrick},
editor = {C. A. Furia and
K. Winter},
title = {Making Linearizability Compositional for Partially Ordered Executions},
booktitle = {iFM},
series = {LNCS},
volume = {11023},
pages = {110--129},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-98938-9\_7},
doi = {10.1007/978-3-319-98938-9\_7},
timestamp = {Wed, 22 Aug 2018 11:24:17 +0200},
biburl = {https://dblp.org/rec/bib/conf/ifm/DohertyDWD18},
bibsource = {dblp computer science bibliography, https://dblp.org},
fullversion = {full-version/IFM-2018-full.pdf}
}
@inproceedings{DBLP:conf/vmcai/DongolJRA18,
author = {B. Dongol and
R. Jagadeesan and
J. Riely and
A. Armstrong},
title = {On abstraction and compositionality for weak-memory linearisability},
booktitle = {{VMCAI}},
series = {LNCS},
volume = {10747},
pages = {183--204},
publisher = {Springer},
year = {2018},
slides = {slides/VMCAI18-pres.pdf}
}
@inproceedings{DBLP:conf/forte/ArmstrongD17,
author = {A. Armstrong and
B. Dongol},
title = {Modularising Opacity Verification for Hybrid Transactional Memory},
booktitle = {{FORTE}},
series = {LNCS},
volume = {10321},
pages = {33--49},
publisher = {Springer},
isabelle = {mechanisation/FORTE-2017-Isabelle.zip},
year = {2017}
}
@inproceedings{DBLP:conf/forte/ArmstrongDD17,
author = {A. Armstrong and
B. Dongol and
S. Doherty},
title = {Proving Opacity via Linearizability: {A} Sound and Complete Method},
booktitle = {{FORTE}},
series = {LNCS},
volume = {10321},
pages = {50--66},
publisher = {Springer},
isabelle = {mechanisation/FORTE-2017-lin-Isabelle.zip},
eprint = {1610.01004},
year = {2017}
}
@inproceedings{DBLP:conf/opodis/DohertyDDSW16,
author = {S. Doherty and
B. Dongol and
J. Derrick and
G. Schellhorn and
H. Wehrheim},
title = {Proving Opacity of a Pessimistic {STM}},
booktitle = {{OPODIS}},
series = {LIPIcs},
volume = {70},
pages = {35:1--35:17},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
isabelle = {mechanisation/OPODIS-2016-Isabelle.zip},
mechanisation = {https://kiv.isse.de/projects/MSPessTM.html},
year = {2016}
}
@inproceedings{DBLP:conf/ftscs/Dongol16,
author = {B. Dongol},
title = {An Interval Logic for Stream-Processing Functions: {A} Convolution-Based
Construction},
booktitle = {{FTSCS}},
series = {Communications in Computer and Information Science},
volume = {694},
pages = {20--35},
year = {2016}
}
@inproceedings{DongolG16,
author = {B. Dongol and
L. Groves},
title = {Contextual Trace Refinement for Concurrent Objects: Safety and Progress},
booktitle = {{ICFEM}},
series = {LNCS},
volume = {10009},
pages = {261--278},
year = {2016}
}
@inproceedings{DongolH16,
author = {B. Dongol and
R. M. Hierons},
title = {Decidability and Complexity for Quiescent Consistency},
booktitle = {{LICS}},
pages = {116--125},
publisher = {{ACM}},
year = {2016}
}
@inproceedings{DongolG16a,
author = {B. Dongol and
L. Groves},
title = {Towards linking correctness conditions for concurrent objects and
contextual trace refinement},
booktitle = {Refine@FM},
series = {{EPTCS}},
volume = {209},
pages = {107--111},
year = {2015}
}
@inproceedings{DBLP:conf/fm/DerrickDSTW15,
author = {J. Derrick and
B. Dongol and
G. Schellhorn and
O. Travkin and
H. Wehrheim},
editor = {N. Bj{\o}rner and
F. D. de Boer},
title = {Verifying Opacity of a Transactional Mutex Lock},
booktitle = {{FM}},
series = {LNCS},
volume = {9109},
pages = {161-177},
publisher = {Springer},
year = {2015},
doi = {10.1007/978-3-319-19249-9_11},
timestamp = {Tue, 26 May 2015 14:26:29 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/fm/DerrickDSTW15},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/mpc/DongolGS15,
author = {B. Dongol and
V. B. F. Gomes and
G. Struth},
editor = {R. Hinze and
J. Voigtl{\"{a}}nder},
title = {A Program Construction and Verification Tool for Separation Logic},
booktitle = {MPC},
series = {LNCS},
volume = {9129},
pages = {137-158},
publisher = {Springer},
year = {2015},
isabelle = {mechanisation/MPC-2015-Isabelle.zip},
doi = {10.1007/978-3-319-19797-5_7},
timestamp = {Tue, 09 Jun 2015 13:13:03 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/mpc/DongolGS15},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/ecoop/DongolDGS15,
author = {B. Dongol and
J. Derrick and
L. Groves and
G. Smith},
editor = {J. T. Boyland},
title = {Defining Correctness Conditions for Concurrent Objects in Multicore
Architectures},
booktitle = {ECOOP},
series = {LIPIcs},
volume = {37},
pages = {470-494},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
year = {2015},
doi = {10.4230/LIPIcs.ECOOP.2015.470},
timestamp = {Mon, 29 Jun 2015 15:28:15 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/ecoop/DongolDGS15},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/hvc/DerrickSGD14,
author = {J. Derrick and
G. Smith and
L. Groves and
B. Dongol},
editor = {E. Yahav},
title = {Using Coarse-Grained Abstractions to Verify Linearizability on {TSO}
Architectures},
booktitle = {HVC},
series = {LNCS},
volume = {8855},
pages = {1-16},
publisher = {Springer},
year = {2014},
doi = {10.1007/978-3-319-13338-6_1},
timestamp = {Mon, 03 Nov 2014 14:03:59 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/hvc/DerrickSGD14},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/facs2/SmithDD14,
author = {G. Smith and
J. Derrick and
B. Dongol},
editor = {I. Lanese and
E. Madelaine},
title = {Admit Your Weakness: Verifying Correctness on {TSO} Architectures},
booktitle = {FACS},
series = {LNCS},
volume = {8997},
pages = {364-383},
publisher = {Springer},
year = {2014},
doi = {10.1007/978-3-319-15317-9_22},
timestamp = {Tue, 03 Feb 2015 13:29:22 +0100},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/facs2/SmithDD14},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/ifm/DerrickSD14,
author = {J. Derrick and
G. Smith and
B. Dongol},
editor = {E. Albert and
E. Sekerinski},
title = {Verifying Linearizability on {TSO} Architectures},
booktitle = {iFM},
series = {LNCS},
volume = {8739},
pages = {341-356},
publisher = {Springer},
year = {2014},
doi = {10.1007/978-3-319-10181-1_21},
timestamp = {Mon, 15 Sep 2014 11:03:36 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/ifm/DerrickSD14},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/ictac/DongolDS14,
author = {B. Dongol and
J. Derrick and
G. Smith},
editor = {G. Ciobanu and
D. M{\'{e}}ry},
title = {Reasoning Algebraically About Refinement on {TSO} Architectures},
booktitle = {ICTAC},
series = {LNCS},
volume = {8687},
pages = {151-168},
publisher = {Springer},
year = {2014},
doi = {10.1007/978-3-319-10882-7_10},
timestamp = {Sun, 14 Sep 2014 16:30:33 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/conf/ictac/DongolDS14},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/fm/DerrickDSTTW14,
author = {J. Derrick and
B. Dongol and
G. Schellhorn and
B. Tofan and
O. Travkin and
H. Wehrheim},
title = {Quiescent Consistency: Defining and Verifying Relaxed Linearizability},
pages = {200-214},
ee = {http://dx.doi.org/10.1007/978-3-319-06410-9_15},
editor = {C. B. Jones and
P. Pihlajasaari and
J. Sun},
booktitle = {FM},
publisher = {Springer},
series = {LNCS},
volume = 8442,
year = 2014,
isbn = {978-3-319-06409-3},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DBLP:journals/eceasst/DongolD13,
author = {B. Dongol and
J. Derrick},
title = {Simplifying proofs of linearisability using layers of abstraction},
journal = {ECEASST},
volume = 66,
year = 2013,
ee = {http://journal.ub.tu-berlin.de/eceasst/article/view/889},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DTDW13,
author = {B. Dongol and
O. Travkin and
J. Derrick and
H. Wehrheim},
title = {A High-Level Semantics for Program Execution under Total
Store Order Memory},
pages = {177-194},
editor = {Z. Liu and
J. Woodcock and
H. Zhu},
booktitle = {ICTAC},
publisher = {Springer},
series = {LNCS},
volume = 8049,
year = 2013,
isbn = {978-3-642-39717-2},
ee = {http://dx.doi.org/10.1007/978-3-642-39718-9},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DD13-REFINE,
author = {B. Dongol and
J. Derrick},
title = {Data refinement for true concurrency},
pages = {15-35},
ee = {http://dx.doi.org/10.4204/EPTCS.115.2},
editor = {J. Derrick and
E. A. Boiten and
S. Reeves},
booktitle = {Refine},
series = {EPTCS},
volume = 115,
year = 2013,
ee = {http://dx.doi.org/10.4204/EPTCS.115},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DDH12,
author = {B. Dongol and
J. Derrick and
I. J. Hayes},
title = {Fractional Permissions and Non-Deterministic Evaluators
in Interval Temporal Logic},
journal = {ECEASST},
volume = 53,
year = 2012,
ee = {http://journal.ub.tu-berlin.de/eceasst/article/view/792},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DHMS12,
author = {B. Dongol and
I. J. Hayes and
L. Meinicke and
K. Solin},
title = {Towards an Algebra for Real-Time Programs},
year = 2012,
pages = {50-65},
ee = {http://dx.doi.org/10.1007/978-3-642-33314-9_4},
bibsource = {DBLP, http://dblp.uni-trier.de},
editor = {W. Kahl and
T. G. Griffin},
booktitle = {RAMICS},
publisher = {Springer},
series = {LNCS},
volume = 7560,
isbn = {978-3-642-33313-2},
ee = {http://dx.doi.org/10.1007/978-3-642-33314-9},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DH12-MPC,
author = {B. Dongol and
I. J. Hayes},
title = {Deriving Real-Time Action Systems Controllers from Multiscale
System Specifications},
year = 2012,
pages = {102-131},
ee = {http://dx.doi.org/10.1007/978-3-642-31113-0_7},
editor = {J. Gibbons and
P. Nogueira},
booktitle = {MPC},
publisher = {Springer},
series = {LNCS},
volume = 7342,
isbn = {978-3-642-31112-3},
ee = {http://dx.doi.org/10.1007/978-3-642-31113-0},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DH12-iFM,
author = {B. Dongol and
I. J. Hayes},
title = {Rely/Guarantee Reasoning for Teleo-reactive Programs over
Multiple Time Bands},
year = 2012,
pages = {39-53},
ee = {http://dx.doi.org/10.1007/978-3-642-30729-4_4},
editor = {J. Derrick and
S. Gnesi and
D. Latella and
H. Treharne},
booktitle = {IFM},
publisher = {Springer},
series = {LNCS},
volume = 7321,
isbn = {978-3-642-30728-7},
ee = {http://dx.doi.org/10.1007/978-3-642-30729-4},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@article{DH12-AVoCS,
author = {B. Dongol and I. J. Hayes},
title = {Approximating idealised real-time specifications using time bands},
journal = {ECEASST},
year = 2012,
volume = 46,
pages = {1-16},
ee = {http://journal.ub.tu-berlin.de/eceasst/article/view/684},
note = {11th International Workshop on Automated Verification of Critical Systems}
}
@inproceedings{DH10,
author = {B. Dongol and
I. J. Hayes},
title = {Compositional Action System Derivation Using Enforced Properties},
booktitle = {MPC},
year = 2010,
pages = {119-139},
ee = {http://dx.doi.org/10.1007/978-3-642-13321-3_9},
editor = {C. Bolduc and
J. Desharnais and
B. Ktari},
publisher = {Springer},
series = {LNCS},
volume = 6120,
isbn = {978-3-642-13320-6},
ee = {http://dx.doi.org/10.1007/978-3-642-13321-3}
}
@inproceedings{DH09,
author = {B. Dongol and
I. J. Hayes},
title = {Enforcing Safety and Progress Properties: {An} Approach to
Concurrent Program Derivation},
pages = {3-12},
ee = {http://dx.doi.org/10.1109/ASWEC.2009.12},
booktitle = {ASWEC},
publisher = {IEEE Computer Society},
year = 2009,
isbn = {978-0-7695-3599-9},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{CD07,
author = {R. Colvin and
B. Dongol},
title = {Verifying Lock-Freedom Using Well-Founded Orders},
year = {2007},
pages = {124-138},
ee = {http://dx.doi.org/10.1007/978-3-540-75292-9_9},
editor = {C. B. Jones and
Z. Liu and
J. Woodcock},
booktitle = {ICTAC},
publisher = {Springer},
series = {LNCS},
volume = {4711},
isbn = {978-3-540-75290-5},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{Don06,
author = {B. Dongol},
title = {Formalising Progress Properties of Non-blocking Programs},
pages = {284-303},
ee = {http://dx.doi.org/10.1007/11901433_16},
editor = {Z. Liu and
J. He},
booktitle = {ICFEM},
publisher = {Springer},
series = {LNCS},
volume = 4260,
year = 2006,
isbn = {3-540-47460-9},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{Don06-AWCVS,
author = {B. Dongol},
title = {Towards simpler proofs of lock-freedom},
optcrossref = {},
optkey = {},
booktitle = {Preliminary Proceedings of the 1st Asian Working Conference on
Verified Software},
pages = {136-146},
year = {2006},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
optaddress = {},
optmonth = {},
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {}
}
@inproceedings{D06,
author = {B. Dongol},
title = {Derivation of {Java} Monitors},
year = 2006,
pages = {211-220},
ee = {http://doi.ieeecomputersociety.org/10.1109/ASWEC.2006.23},
booktitle = {ASWEC},
publisher = {IEEE Computer Society},
isbn = {0-7695-2551-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DM06,
author = {B. Dongol and
A. J. Mooij},
title = {Progress in Deriving Concurrent Programs: {Emphasizing} the
Role of Stable Guards},
pages = {140-161},
ee = {http://dx.doi.org/10.1007/11783596_11},
editor = {T. Uustalu},
booktitle = {MPC},
publisher = {Springer},
series = {LNCS},
volume = 4014,
year = 2006,
isbn = {3-540-35631-2},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cats/GoldsonD05,
author = {D. Goldson and
B. Dongol},
title = {Concurrent Program Design in the Extended Theory of {Owicki
and Gries}},
pages = {41-50},
ee = {http://crpit.com/confpapers/CRPITV41Goldson.pdf},
editor = {M. D. Atkinson and
F. K. H. A. Dehne},
booktitle = {CATS},
publisher = {Australian Computer Society},
series = {CRPIT},
volume = 41,
year = 2005,
isbn = {1-920682-23-6},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@phdthesis{Dongol09,
author = {B. Dongol},
title = {Progress-based verification and derivation of concurrent programs},
school = {School of Information Technology and Electrical Engineering, The University of Queensland},
year = 2009,
address = {Qld, Australia},
month = {October},
url = {thesis.pdf}
}
@article{DBLP:journals/corr/abs-1212-5116,
author = {B. Dongol and
J. Derrick},
title = {Proving linearisability via coarse-grained abstraction},
journal = {CoRR},
volume = {abs/1212.5116},
year = {2012},
eprint = {1212.5116}
}
@techreport{dongolH11,
author = {B. Dongol and I. J. Hayes},
title = {Reasoning About Teleo-Reactive Programs Under Parallel Composition},
institution = {Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland, QLD 4072, Australia},
year = 2011,
number = {SSE-2011-01},
month = {April}
}
@techreport{dongolH07,
author = {B. Dongol and I. J. Hayes},
title = {Trace Semantics for the {Owicki-Gries} Theory Integrated with the Progress Logic from {UNITY}},
institution = {Division of Systems and Software Engineering Research, School of Information Technology and Electrical Engineering, The University of Queensland, QLD 4072, Australia},
year = 2007,
number = {SSE-2007-02},
month = {April},
url = {http://espace.library.uq.edu.au/view.php?pid=UQ:13614}
}
@article{DGHS17,
author = {B. Dongol and
V. B. F. Gomes and
I. J. Hayes and
G. Struth},
title = {Partial Semigroups and Convolution Algebras},
journal = {Archive of Formal Proofs},
volume = {2017},
year = {2017},
url = {https://www.isa-afp.org/entries/PSemigroupsConvolution.shtml},
timestamp = {Fri, 30 Jun 2017 19:26:27 +0200},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/afp/DongolGHS17},
bibsource = {dblp computer science bibliography, http://dblp.org}
}
This file was generated by bibtex2html 1.99.