An Overview of the Annex System. - Duncan A. Grove; Toby C. Murray; Chris A. Owen; Chris J. North; J. A. Jones; Mark R. Beaumont; Bradley D. Hopkins (ACSAC, 2007)

On Refinement-Closed Security Properties and Nondeterministic Compositions. - Toby C. Murray; Gavin Lowe (AVoCS, 2008)

Non-delegatable authorities in capability systems. - Toby C. Murray; Duncan A. Grove (J. Comput. Secur., 2008)

Analysing the Information Flow Properties of Object-Capability Patterns. - Toby C. Murray; Gavin Lowe (Formal Aspects in Security and Trust, 2009)

Analysing the security properties of object-capability patterns. - Toby C. Murray (2010)

Provable Security: How Feasible Is It? - Gerwin Klein; Toby C. Murray; Peter Gammie; Thomas Sewell; Simon Winwood (HotOS, 2011)

seL4 Enforces Integrity. - Thomas Sewell; Simon Winwood; Peter Gammie; Toby C. Murray; June Andronick; Gerwin Klein (ITP, 2011)

Noninterference for Operating System Kernels. - Toby C. Murray; Daniel Matichuk; Matthew Brassil; Peter Gammie; Gerwin Klein (CPP, 2012)

Extensible Specifications for Automatic Re-use of Specifications and Proofs. - Daniel Matichuk; Toby C. Murray (SEFM, 2012)

It's Time for Trustworthy Systems. - Gernot Heiser; Toby C. Murray; Gerwin Klein (IEEE Secur. Priv., 2012)

Formal specifications better than function points for code sizing. - Mark Staples; Rafal Kolanski; Gerwin Klein; Corey Lewis; June Andronick; Toby C. Murray; D. Ross Jeffery; Len Bass (ICSE, 2013)

seL4: From General Purpose to a Proof of Information Flow Enforcement. - Toby C. Murray; Daniel Matichuk; Matthew Brassil; Peter Gammie; Timothy Bourke; Sean Seefried; Corey Lewis; Xin Gao; Gerwin Klein (IEEE Symposium on Security and Privacy, 2013)

On the limits of refinement-testing for model-checking CSP. - Toby C. Murray (Formal Aspects Comput., 2013)

The Last Mile: An Empirical Study of Timing Channels on seL4. - David A. Cock; Qian Ge 001; Toby C. Murray; Gernot Heiser (CCS, 2014)

Productivity for proof engineering. - Mark Staples; D. Ross Jeffery; June Andronick; Toby C. Murray; Gerwin Klein; Rafal Kolanski (ESEM, 2014)

An Isabelle Proof Method Language. - Daniel Matichuk; Makarius Wenzel; Toby C. Murray (ITP, 2014)

File systems deserve verification too! - Gabriele Keller; Toby C. Murray; Sidney Amani; Liam O'Connor; Zilin Chen; Leonid Ryzhyk; Gerwin Klein; Gernot Heiser (ACM SIGOPS Oper. Syst. Rev., 2014)

Comprehensive formal verification of an OS microkernel. - Gerwin Klein; June Andronick; Kevin Elphinstone; Toby C. Murray; Thomas Sewell; Rafal Kolanski; Gernot Heiser (ACM Trans. Comput. Syst., 2014)

Short Paper: On High-Assurance Information-Flow-Secure Programming Languages. - Toby C. Murray (PLAS@ECOOP, 2015)

Empirical Study Towards a Leading Indicator for Cost of Formal Software Verification. - Daniel Matichuk; Toby C. Murray; June Andronick; D. Ross Jeffery; Gerwin Klein; Mark Staples (ICSE (1), 2015)

Specifying a Realistic File System. - Sidney Amani; Toby C. Murray (MARS, 2015)

An empirical research agenda for understanding formal methods productivity. - D. Ross Jeffery; Mark Staples; June Andronick; Gerwin Klein; Toby C. Murray (Inf. Softw. Technol., 2015)

The cross domain desktop compositor: using hardware-based video compositing for a multi-level secure user interface. - Mark R. Beaumont; Jim McCarthy; Toby C. Murray (ACSAC, 2016)

CoGENT: Verifying High-Assurance File System Implementations. - Sidney Amani; Alex Hixon; Zilin Chen; Christine Rizkallah; Peter Chubb; Liam O'Connor; Joel Beeren; Yutaka Nagashima; Japheth Lim; Thomas Sewell; Joseph Tuong; Gabriele Keller; et al. (ASPLOS, 2016)

PLAS'16: ACM SIGPLAN 11th Workshop on Programming Languages and Analysis for Security. - Toby C. Murray; Deian Stefan (CCS, 2016)

Compositional Verification and Refinement of Concurrent Value-Dependent Noninterference. - Toby C. Murray; Robert Sison; Edward Pierzchalski; Christine Rizkallah (CSF, 2016)

Permission and Authority Revisited towards a formalisation. - Sophia Drossopoulou; James Noble 001; Mark S. Miller; Toby C. Murray (FTfJP@ECOOP, 2016)

Refinement through restraint: bringing down the cost of verification. - Liam O'Connor; Zilin Chen; Christine Rizkallah; Sidney Amani; Japheth Lim; Toby C. Murray; Yutaka Nagashima; Thomas Sewell; Gerwin Klein (ICFP, 2016)

A Framework for the Automatic Formal Verification of Refinement from Cogent to C. - Christine Rizkallah; Japheth Lim; Yutaka Nagashima; Thomas Sewell; Zilin Chen; Liam O'Connor; Toby C. Murray; Gabriele Keller; Gerwin Klein (ITP, 2016)

A Dependent Security Type System for Concurrent Imperative Programs. - Toby C. Murray; Robert Sison; Edward Pierzchalski; Christine Rizkallah (Arch. Formal Proofs, 2016)

Compositional Security-Preserving Refinement for Concurrent Imperative Programs. - Toby C. Murray; Robert Sison; Edward Pierzchalski; Christine Rizkallah (Arch. Formal Proofs, 2016)

COGENT: Certified Compilation for a Functional Systems Language. - Liam O'Connor; Christine Rizkallah; Zilin Chen; Sidney Amani; Japheth Lim; Yutaka Nagashima; Thomas Sewell; Alex Hixon; Gabriele Keller; Toby C. Murray; Gerwin Klein (CoRR, 2016)

Eisbach: A Proof Method Language for Isabelle. - Daniel Matichuk; Toby C. Murray; Makarius Wenzel (J. Autom. Reason., 2016)

Short Paper: Towards Information Flow Reasoning about Real-World C Code. - Samuel Grütter; Toby C. Murray (PLAS@CCS, 2017)

VST-Flow: Fine-grained low-level reasoning about real-world C code. - Samuel Grütter; Toby C. Murray (CoRR, 2017)

Special issue on verified information flow security. - Toby C. Murray; Andrei Sabelfeld; Lujo Bauer (J. Comput. Secur., 2017)

Abstract and Concrete Data Types vs Object Capabilities. - James Noble 001; Alex Potanin; Toby C. Murray; Mark S. Miller (Principled Software Development, 2018)

COVERN: A Logic for Compositional Verification of Information Flow Control. - Toby C. Murray; Robert Sison; Kai Engelhardt (EuroS&P, 2018)

In search of perfect users: towards understanding the usability of converged multi-level secure user interfaces. - Abdullah Issa; Toby Murray; Gidon Ernst (OZCHI, 2018)

BP: Formal Proofs, the Fine Print and Side Effects. - Toby C. Murray; Paul C. van Oorschot (SecDev, 2018)

Formally verified software in the real world. - Gerwin Klein; June Andronick; Matthew Fernandez; Ihor Kuz; Toby C. Murray; Gernot Heiser (Commun. ACM, 2018)

SecCSL: Security Concurrent Separation Logic. - Gidon Ernst; Toby Murray (CAV (2), 2019)

Empirically Analyzing Ethereum's Gas Mechanism. - Renlord Yang; Toby Murray; Paul Rimba; Udaya Parampalli (EuroS&P Workshops, 2019)

Value-Dependent Information-Flow Security on Weak Memory Models. - Graeme Smith 001; Nicholas Coughlin; Toby Murray (FM, 2019)

Can We Prove Time Protection? - Gernot Heiser; Gerwin Klein; Toby C. Murray (HotOS, 2019)

Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security. - Robert Sison; Toby Murray (ITP, 2019)

VERONICA: Expressive and Precise Concurrent Information Flow Security. - Daniel Schoepe; Toby Murray; Andrei Sabelfeld (CSF, 2020)

Legion: Best-First Concolic Testing (Competition Contribution). - Dongge Liu; Gidon Ernst; Toby Murray; Benjamin I. P. Rubinstein (FASE, 2020)

LEGION: Best-First Concolic Testing. - Dongge Liu; Gidon Ernst; Toby Murray; Benjamin I. P. Rubinstein (ASE, 2020)

An Under-Approximate Relational Logic. - Toby Murray (Arch. Formal Proofs, 2020)

VERONICA: Expressive and Precise Concurrent Information Flow Security (Extended Version with Technical Appendices). - Daniel Schoepe; Toby Murray; Andrei Sabelfeld (CoRR, 2020)

An Under-Approximate Relational Logic: Heralding Logics of Insecurity, Incorrect Implementation & More. - Toby Murray (CoRR, 2020)

Towards Provable Timing-Channel Prevention. - Gernot Heiser; Toby Murray; Gerwin Klein (ACM SIGOPS Oper. Syst. Rev., 2020)

Towards Systematic and Dynamic Task Allocation for Collaborative Parallel Fuzzing. - Van-Thuan Pham; Manh-Dung Nguyen; Quang-Trung Ta; Toby Murray; Benjamin I. P. Rubinstein (ASE, 2021)

Incremental Vulnerability Detection via Back-Propagating Symbolic Execution of Insecurity Separation Logic. - Toby Murray; Pengbo Yan; Gidon Ernst (CoRR, 2021)

Deductive Verification via the Debug Adapter Protocol. - Gidon Ernst; Johannes Blau; Toby Murray (F-IDE@NFM, 2021)

SecRSL: Security Separation Logic for C11 Release-Acquire Concurrency (Extended version with technical appendices). - Pengbo Yan; Toby Murray (CoRR, 2021)

Information-flow control on ARM and POWER multicore processors. - Graeme Smith 001; Nicholas Coughlin; Toby Murray (Formal Methods Syst. Des., 2021)

Cogent: uniqueness types and certifying compilation. - Liam O'Connor; Zilin Chen; Christine Rizkallah; Vincent Jackson; Sidney Amani; Gerwin Klein; Toby Murray; Thomas Sewell; Gabriele Keller (J. Funct. Program., 2021)

Verified secure compilation for mixed-sensitivity concurrent programs. - Robert Sison; Toby Murray (J. Funct. Program., 2021)

SecRSL: security separation logic for C11 release-acquire concurrency. - Pengbo Yan; Toby Murray (Proc. ACM Program. Lang., 2021)

A Hoare Logic with Regular Behavioral Specifications. - Gidon Ernst; Alexander Knapp; Toby Murray (ISoLA (1), 2022)

State Selection Algorithms and Their Impact on The Performance of Stateful Network Protocol Fuzzing. - Dongge Liu; Van-Thuan Pham; Gidon Ernst; Toby Murray; Benjamin I. P. Rubinstein (SANER, 2022)

"Free" as in Freedom to Protest? - Fabio Massacci; Antonino Sabetta; Jelena Mirkovic; Toby Murray; Hamed Okhravi; Mohammad Mannan; Anderson Rocha 001; Eric Bodden; Daniel E. Geer (IEEE Secur. Priv., 2022)

Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications. - Toby Murray; Mukesh Tiwari; Gidon Ernst; David A. Naumann (CCS, 2023)

Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems. - Robert Sison; Scott Buckley; Toby Murray; Gerwin Klein; Gernot Heiser (FM, 2023)

Beyond the Coverage Plateau: A Comprehensive Study of Fuzz Blockers (Registered Report). - Wentao Gao; Van-Thuan Pham; Dongge Liu; Oliver Chang; Toby Murray; Benjamin I. P. Rubinstein (FUZZING, 2023)

Compositional Vulnerability Detection with Insecurity Separation Logic. - Toby Murray; Pengbo Yan; Gidon Ernst (ICFEM, 2023)

Detecting Excessive Data Exposures in Web Server Responses with Metamorphic Fuzzing. - Lianglu Pan; Shaanan Cohney; Toby Murray; Van-Thuan Pham (CoRR, 2023)

Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications (Extended Version). - Toby Murray; Mukesh Tiwari; Gidon Ernst; David A. Naumann (CoRR, 2023)

Proving the Absence of Microarchitectural Timing Channels. - Scott Buckley; Robert Sison; Nils Wistoff; Curtis Millar; Toby Murray; Gerwin Klein; Gernot Heiser (CoRR, 2023)

OOBKey: Key Exchange with Implantable Medical Devices Using Out-Of-Band Channels. - Mo Zhang; Eduard Marin; Mark Ryan 001; Vassilis Kostakos; Toby Murray; Benjamin Tag; David F. Oswald (ARES, 2024)

Elephants Do Not Forget: Differential Privacy with State Continuity for Privacy Budget. - Jiankai Jin; Chitchanok Chuengsatiansup; Toby Murray; Benjamin I. P. Rubinstein; Yuval Yarom; Olga Ohrimenko (CCS, 2024)

Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms. - Pengbo Yan; Toby Murray; Olga Ohrimenko; Van-Thuan Pham; Robert Sison (FM (1), 2024)

EDEFuzz: A Web API Fuzzer for Excessive Data Exposures. - Lianglu Pan; Shaanan Cohney; Toby Murray; Van-Thuan Pham (ICSE, 2024)

A Generalised Union of Rely-Guarantee and Separation Logic Using Permission Algebras. - Vincent Jackson; Toby Murray; Christine Rizkallah (ITP, 2024)

Symbol Correctness in Deep Neural Networks Containing Symbolic Layers. - Aaron Bembenek; Toby Murray (CoRR, 2024)

Evaluating Program Repair with Semantic-Preserving Transformations: A Naturalness Assessment. - Thanh Le-Cong; Dat Nguyen; Bach Le 001; Toby Murray (CoRR, 2024)

Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms (Extended Version). - Pengbo Yan; Toby Murray; Olga Ohrimenko; Van-Thuan Pham; Robert Sison (CoRR, 2024)

Semantic-guided Search for Efficient Program Repair with Large Language Models. - Thanh Le-Cong; Bach Le 001; Toby Murray (CoRR, 2024)

Evict+Spec+Time: Exploiting Out-of-Order Execution to Improve Cache-Timing Attacks. - Shing Hing William Cheng; Chitchanok Chuengsatiansup; Daniel Genkin; Dallas McNeil; Toby Murray; Yuval Yarom; Zhiyuan Zhang 005 (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2024)

Can LLMs Reason About Program Semantics? A Comprehensive Evaluation of LLMs on Formal Specification Inference. - Thanh Le-Cong; Bach Le 001; Toby Murray (ACL (1), 2025)

A Formally Verified Robustness Certifier for Neural Networks. - James Tobler; Hira Taqdees Syeda; Toby Murray (CAV (2), 2025)

Trailblazer: Practical End-to-end Web API Fuzzing (Registered Report). - Lianglu Pan; Shaanan Cohney; Toby Murray; Van-Thuan Pham (ISSTA Companion, 2025)

A Formally Verified Robustness Certifier for Neural Networks (Extended Version). - James Tobler; Hira Taqdees Syeda; Toby Murray (CoRR, 2025)

Towards Reliable Evaluation of Neural Program Repair with Natural Robustness Testing. - Thanh Le-Cong; Dat Nguyen; Bach Le 001; Toby Murray (ACM Trans. Softw. Eng. Methodol., 2025)