Robert J. Colvin

26 papers B 4C 1Journal 17Unranked 3
YearRankTypeTitle / Venue / Authors
2026 J jnl
Weak Memory Model Formalisms: Introduction and Survey.
Concurr. Comput. Pract. Exp.
Roger C. Su, Robert J. Colvin
2025 J jnl
Rely-Guarantee Extensions and Locks.
Arch. Formal Proofs
Robert J. Colvin, Scott Heiner, Peter Höfner, Roger C. Su
2025 — conf
Structural Operational Semantics for Functional and Security Verification of Pipelined Processors.
CAV (1)
Robert J. Colvin, Roger C. Su
2025 J jnl
Weak Memory Model Formalisms: Introduction and Survey.
CoRR
Roger C. Su, Robert J. Colvin
2024 J jnl
Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures.
CoRR
Robert J. Colvin, Ian J. Hayes, Scott Heiner, Peter Höfner, Larissa Meinicke, Roger C. Su
2024 — ch.
Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures.
The Practice of Formal Methods (I)
Robert J. Colvin, Ian J. Hayes, Scott Heiner, Peter Höfner, Larissa Meinicke, Roger C. Su
2023 B conf
A Fine-Grained Semantics for Arrays and Pointers Under Weak Memory Models.
FM
Robert J. Colvin
2022 C conf
Separation of Concerning Things: A Simpler Basis for Defining and Programming with the C/C++ Memory Model.
ICFEM
Robert J. Colvin
2022 J jnl
Separation of concerning things: a simpler basis for defining and programming with the C/C++ memory model (extended version).
CoRR
Robert J. Colvin
2021 B conf
Parallelized Sequential Composition and Hardware Weak Memory Models.
SEFM
Robert J. Colvin
2021 J jnl
Parallelized sequential composition, pipelines, and hardware weak memory models.
CoRR
Robert J. Colvin
2020 J jnl
An abstract semantics of speculative execution for reasoning about security vulnerabilities.
CoRR
Robert J. Colvin, Kirsten Winter
2020 J jnl
Linearizability on hardware weak memory models.
Formal Aspects Comput.
Graeme Smith, Kirsten Winter, Robert J. Colvin
2019 J jnl
A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency.
Formal Aspects Comput.
Ian J. Hayes, Larissa A. Meinicke, Kirsten Winter, Robert J. Colvin
2019 — conf
An Abstract Semantics of Speculative Execution for Reasoning About Security Vulnerabilities.
FM Workshops (2)
Robert J. Colvin, Kirsten Winter
2018 B conf
A Wide-Spectrum Language for Verification of Programs on Weak Memory Models.
FM
Robert J. Colvin, Graeme Smith
2018 J jnl
A high-level operational semantics for hardware weak memory models.
CoRR
Robert J. Colvin, Graeme Smith
2018 J jnl
A sound and complete definition of linearizability on weak memory models.
CoRR
Graeme Smith, Kirsten Winter, Robert J. Colvin
2018 J jnl
A wide-spectrum language for verification of programs on weak memory models.
CoRR
Robert J. Colvin, Graeme Smith
2018 — conf
Correctness of Concurrent Objects under Weak Memory Models.
Refine@FM
Graeme Smith, Kirsten Winter, Robert J. Colvin
2017 J jnl
A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency.
CoRR
Ian J. Hayes, Larissa A. Meinicke, Kirsten Winter, Robert J. Colvin
2017 J jnl
Designing a semantic model for a wide-spectrum language with concurrency.
Formal Aspects Comput.
Robert J. Colvin, Ian J. Hayes, Larissa A. Meinicke
2016 B conf
An Algebra of Synchronous Atomic Steps.
FM
Ian J. Hayes, Robert J. Colvin, Larissa A. Meinicke, Kirsten Winter, Andrius Velykis
2016 J jnl
Designing a semantic model for a wide-spectrum language with concurrency.
CoRR
Robert J. Colvin, Ian J. Hayes, Larissa A. Meinicke
2016 J jnl
Modelling and analysing neural networks using a hybrid process algebra.
Theor. Comput. Sci.
Robert J. Colvin
2015 J jnl
Balancing expressiveness in formal approaches to concurrency.
Formal Aspects Comput.
Cliff B. Jones, Ian J. Hayes, Robert J. Colvin