[1]
ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS. Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel Krishnaswami, and Peter Sewell. In POPL 2019. Proc. ACM Program. Lang. 3, POPL, Article 71. [project page]. [pdf].
[2]
Lem: Reusable Engineering of Real-world Semantics. Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell. In ICFP 2014. [pdf].
[3]
Skeletal Semantics and their Interpretations. Martin Bodin, Philippa Gardner, Thomas Jensen, and Alan Schmitt. In POPL 2019. [pdf].
[4]
Improved Tool Support for Machine-Code Decompilation in HOL4. Anthony C. J. Fox. In ITP 2015. [pdf].
[5]
A Dependent Type Theory with Abstractable Names. A. M. Pitts, J. Matthiesen, and J. Derikx. In LSFA 2014. [pdf].
[6]
Running programming language specifications, Basile Clement, August 2014. MPRI report.
[7]
Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8. Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell. In POPL 2018. [project page]. [pdf].
[8]
Mixed-size Concurrency: ARM, POWER, C/C++11, and SC. Shaked Flur, Susmit Sarkar, Christopher Pulte, Kyndylan Nienhuis, Luc Maranget, Kathryn E. Gray, Ali Sezgin, Mark Batty, and Peter Sewell. In POPL 2017. [pdf].
[9]
A Consistency Checker for Memory Subsystem Traces. M. Naylor, S. W. Moore, and A. Mujumdar. In FMCAD 2016. [pdf].
[10]
Modelling the ARMv8 architecture, operationally: concurrency and ISA. Shaked Flur, Kathryn E. Gray, Christopher Pulte, Susmit Sarkar, Ali Sezgin, Luc Maranget, Will Deacon, and Peter Sewell. In POPL 2016. [pdf].
[11]
GPU Concurrency: Weak Behaviours and Programming Assumptions. Jade Alglave, Mark Batty, Alastair F. Donaldson, Ganesh Gopalakrishnan, Jeroen Ketema, Daniel Poetzl, Tyler Sorensen, and John Wickerson. In ASPLOS 2015. [url].
[12]
An integrated concurrency and core-ISA architectural envelope definition, and test oracle, for IBM POWER multiprocessors. Kathryn E. Gray, Gabriel Kerneis, Dominic P. Mulligan, Christopher Pulte, Susmit Sarkar, and Peter Sewell. In MICRO 2015. [pdf].
[13]
Rigorous Architectural Modelling for Production Multiprocessors, S. Flur, K. Gray, G. Kerneis, D. Mulligan, C. Pulte, S. Sarkar, and P. Sewell, May 2015. Presentation at HCSS 2015: the Fifteenth Annual High Confidence Software and Systems Conference.
[14]
The RISC-V Instruction Set Manual Volume I: Unprivileged ISA. Andrew Waterman and Krste Asanović, editors. December 2018. Document Version 20181221-Public-Review-draft. Contributors: Arvind, Krste Asanović, Rimas Avižienis, Jacob Bachmeyer, Christopher F. Batten, Allen J. Baum, Alex Bradbury, Scott Beamer, Preston Briggs, Christopher Celio, Chuanhua Chang, David Chisnall, Paul Clayton, Palmer Dabbelt, Roger Espasa, Shaked Flur, Stefan Freudenberger, Jan Gray, Michael Hamburg, John Hauser, David Horner, Bruce Hoult, Alexandre Joannou, Olof Johansson, Ben Keller, Yunsup Lee, Paul Loewenstein, Daniel Lustig, Yatin Manerkar, Luc Maranget, Margaret Martonosi, Joseph Myers, Vijayanand Nagarajan, Rishiyur Nikhil, Jonas Oberhauser, Stefan O’Rear, Albert Ou, John Ousterhout, David Patterson, Christopher Pulte, Jose Renau, Colin Schmidt, Peter Sewell, Susmit Sarkar, Michael Taylor, Wesley Terpstra, Matt Thomas, Tommy Thorn, Caroline Trippel, Ray VanDeWalker, Muralidaran Vijayaraghavan, Megan Wachs, Andrew Waterman, Robert Watson, Derek Williams, Andrew Wright, Reinoud Zandijk, and Sizhuo Zhang. [pdf].
[15]
Efficient Tagged Memory. Alexandre Joannou, Jonathan Woodruff, Robert Kovacsics, Simon W. Moore, Alex Bradbury, Hongyan Xia, Robert N. M. Watson, David Chisnall, Michael Roe, Brooks Davis, Edward Napierala, John Baldwin, Khilan Gudka, Peter G. Neumann, Alfredo Mazzinghi, Alex Richardson, Stacey Son, and A. Theodore Markettos. In ICCD 2017. [pdf].
[16]
Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture (Version 6). Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Jonathan Anderson, John Baldwin, David Chisnall, Brooks Davis, Alexandre Joannou, Ben Laurie, Simon W. Moore, Steven J. Murdoch, Robert Norton, Stacey Son, and Hongyan Xia. Technical Report UCAM-CL-TR-907, University of Cambridge, Computer Laboratory, April 2017. [pdf].
[17]
CHERI JNI: Sinking the Java Security Model into the C. David Chisnall, Brooks Davis, Khilan Gudka, David Brazdil, Alexandre Joannou, Jonathan Woodruff, A. Theodore Markettos, J. Edward Maste, Robert Norton, Stacey Son, Michael Roe, Simon W. Moore, Peter G. Neumann, Ben Laurie, and Robert N.M. Watson. In ASPLOS 2017. [url].
[18]
Fast Protection-Domain Crossing in the CHERI Capability-System Architecture. Robert N.M. Watson, Robert M. Norton, Jonathan Woodruff, Simon W. Moore, Peter G. Neumann, Jonathan Anderson, David Chisnall, Brooks Davis, Ben Laurie, Michael Roe, Nirav H. Dave, Khilan Gudka, Alexandre Joannou, A. Theodore Markettos, Ed Maste, Steven J. Murdoch, Colin Rothwell, Stacey D. Son, and Munraj Vadera. IEEE Micro, 36(5):38–49, September 2016. [pdf].
[19]
A generic synthesisable test bench. Matthew Naylor and Simon W. Moore. In MEMOCODE 2015. [pdf].
[20]
Capability Hardware Enhanced RISC Instructions: CHERI Instruction-Set Architecture. Robert N. M. Watson, Peter G. Neumann, Jonathan Woodruff, Michael Roe, Jonathan Anderson, David Chisnall, Brooks Davis, Alexandre Joannou, Ben Laurie, Simon W. Moore, Steven J. Murdoch, Robert Norton, and Stacey Son. Technical Report UCAM-CL-TR-876, University of Cambridge, Computer Laboratory, September 2015. [pdf].
[21]
Capability Hardware Enhanced RISC Instructions: CHERI Programmer’s Guide. Robert N. M. Watson, David Chisnall, Brooks Davis, Wojciech Koszek, Simon W. Moore, Steven J. Murdoch, Peter G. Neumann, and Jonathan Woodruff. Technical Report UCAM-CL-TR-877, University of Cambridge, Computer Laboratory, September 2015. [pdf].
[22]
CHERI: A Hybrid Capability-System Architecture for Scalable Software Compartmentalization. Robert N. M. Watson, Jonathan Woodruff, Peter G. Neumann, Simon W. Moore, Jonathan Anderson, David Chisnall, Nirav Dave, Brooks Davis, Khilan Gudka, Ben Laurie, Steven J. Murdoch, Robert Norton, Michael Roe, Stacey Son, and Munraj Vadera. In Security and Privacy 2015. [pdf].
[23]
Beyond the PDP-11: Processor support for a memory-safe C abstract machine. David Chisnall, Colin Rothwell, Brooks Davis, Robert N.M. Watson, Jonathan Woodruff, Munraj Vadera, Simon W. Moore, Peter G. Neumann, and Michael Roe. In ASPLOS 2015.
[24]
Extracting Behaviour from an Executable Instruction Set Model. Brian Campbell and Ian Stark. In FMCAD 2016. Full proceedings http://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD16/proceedings/fmcad-2016-proceedings.pdf. [pdf].
[25]
Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation. Brian Campbell and Ian Stark. Sci. Comput. Program., 118:60–76, March 2016. [pdf].
[26]
Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation. Brian Campbell and Ian Stark. In FMICS 2014. [pdf].
[27]
Into the depths of C: elaborating the de facto standards. Kayvan Memarian, Justus Matthiesen, James Lingard, Kyndylan Nienhuis, David Chisnall, Robert N.M. Watson, and Peter Sewell. In PLDI 2016. PLDI 2016 Distinguished Paper award. [pdf].
[28]
Exploring C Semantics and Pointer Provenance. Kayvan Memarian, Victor B. F. Gomes, Brooks Davis, Stephen Kell, Alexander Richardson, Robert N. M. Watson, and Peter Sewell. In POPL 2019. Proc. ACM Program. Lang. 3, POPL, Article 67. [project page]. [pdf].
[29]
Clarifying the C memory object model, Kayvan Memarian and Peter Sewell. ISO SC22 WG14 N2012, March 2016. [html].
[30]
C memory object and value semantics: the space of de facto and ISO standards, David Chisnall, Justus Matthiesen, Kayvan Memarian, Kyndylan Nienhuis, Peter Sewell, and Robert N. M. Watson. ISO SC22 WG14 N2013, March 2016. [pdf].
[31]
What is C in practice? (Cerberus survey v2): Analysis of Responses, Kayvan Memarian and Peter Sewell. ISO SC22 WG14 N2014, March 2016. [html].
[32]
What is C in practice? (Cerberus survey v2): Analysis of Responses – with Comments, Kayvan Memarian and Peter Sewell. ISO SC22 WG14 N2015, March 2016. [url].
[33]
Clarifying Unspecified Values (Draft Defect Report or Proposal for C2x), Kayvan Memarian and Peter Sewell. ISO SC22 WG14 N2089, September 2016. [html].
[34]
Clarifying Pointer Provenance (Draft Defect Report or Proposal for C2x), Kayvan Memarian and Peter Sewell. ISO SC22 WG14 N2090, September 2016. [html].
[35]
Clarifying Trap Representations (Draft Defect Report or Proposal for C2x), Kayvan Memarian and Peter Sewell. ISO SC22 WG14 N2091, September 2016. [html].
[36]
N2223: Clarifying the C Memory Object Model: Introduction to N2219 – N2222, Kayvan Memarian, Victor Gomes, and Peter Sewell. ISO SC22 WG14 N2223, March 2018. [project page]. [html].
[37]
N2219: Clarifying Pointer Provenance (Q1-Q20) v3, Kayvan Memarian, Victor Gomes, and Peter Sewell. ISO SC22 WG14 N2219, March 2018. [project page]. [html].
[38]
N2220: Clarifying Trap Representations (Q47) v3, Kayvan Memarian, Victor Gomes, and Peter Sewell. ISO SC22 WG14 N2220, March 2018. [project page]. [html].
[39]
N2221: Clarifying Unspecified Values (Q48-Q59) v3, Kayvan Memarian, Victor Gomes, and Peter Sewell. ISO SC22 WG14 N2221, March 2018. [project page]. [html].
[40]
N2222: Further Pointer Issues (Q21-Q46), Kayvan Memarian, Victor Gomes, and Peter Sewell. ISO SC22 WG14 N2222, March 2018. [project page]. [html].
[41]
N2263 Sewell,Clarifying Pointer Provenance (Q1-Q20) v4, Kayvan Memarian, Victor Gomes, and Peter Sewell. ISO SC22 WG14 N2263, March 2018. [project page]. [html].
[42]
Cerberus: towards an Executable Semantics for Sequential and Concurrent C11, Kayvan Memarian, Kyndylan Nienhuis, Justus Matthiesen, James Lingard, and Peter Sewell, May 2015. Presentation at HCSS 2015: the Fifteenth Annual High Confidence Software and Systems Conference.
[43]
An operational semantics for C/C++11 concurrency. Kyndylan Nienhuis, Kayvan Memarian, and Peter Sewell. In OOPSLA 2016. [pdf].
[44]
A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions. Jean Pichon-Pharabod and Peter Sewell. In POPL 2016. [pdf].
[45]
The Problem of Programming Language Concurrency Semantics. Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell. In ESOP 2015. [pdf].
[46]
The C11 and C++11 Concurrency Model. Mark John Batty. PhD thesis, University of Cambridge Computer Laboratory, November 2014. Winner of 2015 ACM SIGPLAN John C. Reynolds Doctoral Dissertation Award and 2015 CPHC/BCS Distinguished Dissertation competition.
[47]
A no-thin-air memory model for programming languages. Jean Pichon-Pharabod. PhD thesis, University of Cambridge, 2018.
[48]
QEMU/CPC: static analysis and CPS conversion for safe, portable, and efficient coroutines. Gabriel Kerneis, Charlie Shepherd, and Stefan Hajnoczi. In PEPM 2014. [url].
[49]
Efficient code generation for weakly ordered architectures, Reinoud Elhorst, Mark Batty, and David Chisnall. Presentation at the 4th European LLVM conference (EuroLLVM), April 2014. Slides and report available at http://llvm.org/devmtg/2014-04/.
[50]
Lowering C11 Atomics for ARM in LLVM, Reinoud Elhorst, March 2014. [pdf].
[51]
Some were meant for C: the endurance of an unmanageable language. Stephen Kell. In Onward! 2017. [pdf].
[52]
Dynamically diagnosing type errors in unsafe code. Stephen Kell. In OOPSLA 2016. [pdf].
[53]
In Search of Types. Stephen Kell. In Onward! 2014. [url].
[54]
The missing link: explaining ELF static linking, semantically. Stephen Kell, Dominic P. Mulligan, and Peter Sewell. In OOPSLA 2016. [pdf].
[55]
Towards a dynamic object model within Unix processes. Stephen Kell. In Onward! 2015. [pdf].
[56]
Clean Application Compartmentalization with SOAAP. Khilan Gudka, Robert N. M. Watson, Jonathan Anderson, David Chisnall, Brooks Davis, Ben Laurie, Ilias Marinos, Peter G. Neumann, and Alex Richardson. In CCS 2015. [pdf].
[57]
CheriABI: Enforcing Valid Pointer Provenance and Minimizing Pointer Privilege in the POSIX C Run-time Environment. Brooks Davis, Robert N. M. Watson, Alexander Richardson, Peter G. Neumann, Simon W. Moore, John Baldwin, David Chisnall, James Clarke, Nathaniel Wesley Filardo, Khilan Gudka, Alexandre Joannou, Ben Laurie, A. Theodore Markettos, J. Edward Maste, Alfredo Mazzinghi, Edward Tomasz Napierala, Robert M. Norton, Michael Roe, Peter Sewell, Stacey Son, and Jonathan Woodruff. In ASPLOS 2019. Best paper award. [pdf].
[58]
Symbolic Execution for JavaScript. José Fragoso Santos, Petar Maksimovic, Théotime Grohens, Julian Dolby, and Philippa Gardner. In PPDP 2018. [url].
[59]
JaVerT: JavaScript verification toolchain. José Fragoso Santos, Petar Maksimović, Daiva Naudžiūnienė, Thomas Wood, and Philippa Gardner. In POPL 2018. [pdf].
[60]
JSExplain: a Double Debugger for JavaScript. Arthur Charguéraud, Alan Schmitt, and Thomas Wood. In WWW. [pdf].
[61]
Towards Logic-Based Verification of JavaScript Programs. José Fragoso Santos, Philippa Gardner, Petar Maksimovic, and Daiva Naudziuniene. In CADE 2017. [url].
[62]
DOM: Specification and Client Reasoning. Azalea Raad, José Fragoso Santos, and Philippa Gardner. In APLAS 2016. [url].
[63]
JaVerT 2.0: Compositional Symbolic Execution for JavaScript. José Fragoso Santos, Petar Maksimović, Gabriela Sampaio, and Philippa Gardner. In POPL 2019. [pdf].
[64]
Verified compilation of CakeML to multiple machine-code targets. Anthony C. J. Fox, Magnus O. Myreen, Yong Kiam Tan, and Ramana Kumar. In CPP 2017. [pdf].
[65]
A New Verified Compiler Backend for CakeML. Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, and Michael Norrish. In ICFP 2016. [pdf].
[66]
CakeML: a verified implementation of ML. Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. In POPL 2014. [url].
[67]
Proof-producing translation of higher-order logic into pure and stateful ML. Magnus O. Myreen and Scott Owens. J. Funct. Program., 24(2-3):284–315, January 2014. [url].
[68]
Mechanising and Verifying the WebAssembly Specification. Conrad Watt. In CPP 2018. [pdf].
[69]
CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem. Conrad Watt, John Renner, Natalie Popescu, Sunjay Cauligi, and Deian Stefan. In POPL 2019. [pdf].
[70]
Bounding Data Races in Space and Time. Stephen Dolan, KC Sivaramakrishnan, and Anil Madhavapeddy. In PLDI 2018. [pdf].
[71]
A modular foreign function interface. Jeremy Yallop, David Sheets, and Anil Madhavapeddy. Science of Computer Programming, April 2017. [pdf].
[72]
Generic Partially-static Data (Extended Abstract). David Kaloper-Meršinjak and Jeremy Yallop. In TyDe 2016. [pdf].
[73]
Conex — establishing trust into data repositories. Hannes Mehnert and Louis Gesbert. In OCaml 2016. [url].
[74]
OCaml inside: a drop-in replacement for libtls (extended abstract). Enguerrand Decorne, Jeremy Yallop, and David Meršinjak. In OCaml 2016. [url].
[75]
Not-quite-so-broken TLS 1.3 mechanised conformance checking. David Kaloper-Meršinjak and Hannes Mehnert. In TRON workshop 2016. [pdf].
[76]
Not-Quite-So-Broken TLS: Lessons in Re-Engineering a Security Protocol Specification and Implementation. David Kaloper-Mersinjak, Hannes Mehnert, Anil Madhavapeddy, and Peter Sewell. In USENIX Security 2015. [pdf].
[77]
Transport Layer Security purely in OCaml. Hannes Mehnert and David Kaloper Mersinjak. In OCaml 2014. [url].
[78]
Trustworthy secure modular operating system engineering, David Kaloper Meršinjak and Hannes Mehnert. Invited talk at 31st Chaos Communication Congress (31C3), January 2015.
[79]
Not-quite-so-broken TLS: lessons in re-engineering a security protocol specification and implementation, David Kaloper Meršinjak, Hannes Mehnert, Anil Madhavapeddy, and Peter Sewell, May 2015. Presentation at HCSS 2015: the Fifteenth Annual High Confidence Software and Systems Conference.
[80]
Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API. Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom Ridge, Peter Sewell, Michael Smith, and Keith Wansbrough. J. ACM, 66(1):1:1–1:77, December 2018. [project page]. [pdf].
[81]
SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems. Tom Ridge, David Sheets, Thomas Tuerk, Andrea Giugliano, Anil Madhavapeddy, and Peter Sewell. In SOSP 2015. [pdf].
[82]
A Concurrent Specification of POSIX File Systems. Gian Ntzik, Pedro da Rocha Pinto, Julian Sutherland, and Philippa Gardner. In ECOOP 2018. [pdf].
[83]
Reasoning About POSIX File Systems. Gian Ntzik. PhD thesis, Imperial College London, September 2016. [url].
[84]
Reasoning about the POSIX File System: Local Update and Global Pathnames. Gian Ntzik and Philippa Gardner. In OOPSLA 2015.
[85]
Fault-tolerant Resource Reasoning. Gian Ntzik, Pedro da Rocha Pinto, and Philippa Gardner. In APLAS 2015. [pdf].
[86]
Local Reasoning for the POSIX File System. Philippa Gardner, Gian Ntzik, and Adam Wright. In ESOP 2014. [url].
[87]
Verified trustworthy software systems. Philippa Gardner. Philosophical Transactions of the Royal Society of London A, 375(2104), September 2017. [pdf].
[88]
A Perspective on Specifying and Verifying Concurrent Modules. Thomas Dinsdale-Young, Pedro da Rocha Pinto, and Philippa Gardner. Journal of Logical and Algebraic Methods in Programming, 98:1–25, August 2018. [pdf].
[89]
On abstraction and compositionality for weak-memory linearisability. Brijesh Dongol, Radha Jagadeesan, James Riely, and Alasdair Armstrong. In VMCAI 2018. [url].
[90]
A separation logic for a promising semantics. Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, and Viktor Vafeiadis. In ESOP 2018. [pdf].
[91]
Algebraic Laws for Weak Consistency. Andrea Cerone, Alexey Gotsman, and Hongseok Yang. In CONCUR 2017. [url].
[92]
Verifying Strong Eventual Consistency in Distributed Systems. Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, and Alastair R. Beresford. In OOPSLA 2017. Distinguished Paper award. [url].
[93]
A Relational Model of Types-and-Effects in Higher-Order Concurrent Separation Logic. Morten Krogh-Jespersen, Kasper Svendsen, and Lars Birkedal. In POPL 2017. [url].
[94]
Trace Properties from Separation Logic Specifications. Lars Birkedal, Thomas Dinsdale-Young, Guilhem Jaber, Kasper Svendsen, and Nikos Tzevelekos. CoRR, abs/1702.02972, February 2017. [pdf].
[95]
Caper: Automatic Verification for Fine-grained Concurrency. Thomas Dinsdale-Young, Pedro da Rocha Pinto, Kristoffer Just Andersen, and Lars Birkedal. In ESOP 2017. [pdf].
[96]
Abstract Specifications for Concurrent Maps. Shale Xiong, Pedro da Rocha Pinto, Gian Ntzik, and Philippa Gardner. In ESOP 2017. [pdf].
[97]
Reasoning with Time and Data Abstractions. Pedro da Rocha Pinto. PhD thesis, Imperial College London, September 2016. [url].
[98]
Abstraction, Refinement and Concurrent Reasoning. Azalea Raad. PhD thesis, Imperial College London, September 2016. [url].
[99]
Verifying Concurrent Graph Algorithms. Azalea Raad, Aquinas Hobor, Jules Villard, and Philippa Gardner. In APLAS 2016. [url].
[100]
Local Linearizability for Concurrent Container-Type Data Structures. Andreas Haas, Thomas A. Henzinger, Andreas Holzer, Christoph M. Kirsch, Michael Lippautz, Hannes Payer, Ali Sezgin, Ana Sokolova, and Helmut Veith. In CONCUR 2016. [pdf].
[101]
Modular Termination Verification for Non-blocking Concurrency. Pedro da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner, and Julian Sutherland. In ESOP 2016. [project page]. [pdf].
[102]
Transfinite Step-indexing: Decoupling Concrete and Logical Steps. Kasper Svendsen, Filip Sieczkowski, and Lars Birkedal. In ESOP 2016. [pdf].
[103]
Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper). Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. In MFPS 2015. [pdf].
[104]
Moving Around: Lipton’s Reduction for TSO - (Regular Submission). Ali Sezgin and Serdar Tasiran. In VSTTE 2015. [url].
[105]
A Separation Logic for Fictional Sequential Consistency. Filip Sieczkowski, Kasper Svendsen, Lars Birkedal, and Jean Pichon-Pharabod. In ESOP 2015.
[106]
CoLoSL: Concurrent Local Subjective Logic. Azalea Raad, Jules Villard, and Philippa Gardner. In ESOP 2015. [pdf].
[107]
Aspect-oriented linearizability proofs. Soham Chakraborty, Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. Logical Methods in Computer Science, 11(1):1–33, April 2015. [url].
[108]
Abstract Local Reasoning for Concurrent Libraries: Mind the Gap. Philippa Gardner, Azalea Raad, Mark J. Wheelhouse, and Adam Wright. MFPS 2014: Electr. Notes Theor. Comput. Sci., 308:147–166, June 2014. [url].
[109]
TaDA: A Logic for Time and Data Abstraction. Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. In ECOOP 2014. [url].
[110]
Developments in Concurrent Kleene Algebra. Tony Hoare, Stephan van Staden, Bernhard Möller, Georg Struth, Jules Villard, Huibiao Zhu, and Peter W. O’Hearn. In RAMiCS 2014. [url].
[111]
Kleene Algebras with Domain. Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth, and Tjark Weber. Archive of Formal Proofs, 2016, April 2016. [url].
[112]
Modal Kleene algebra applied to program correctness. Victor B. F. Gomes and Georg Struth. In FM 2016. [pdf].
[113]
Program Construction and Verification Components Based on Kleene Algebra. Victor B. F. Gomes and Georg Struth. Archive of Formal Proofs, 2016, June 2016. [url].
[114]
CoSMed: A Confidentiality-Verified Social Media Platform. Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, and Franco Raimondi. J. Automated Reasoning, December 2017. [url].
[115]
Programming and proving with classical types. Cristina Matache, Victor B. F. Gomes, and Dominic P. Mulligan. In APLAS 2017. [url].