Oracle Semantics for Concurrent Separation Logic. - Aquinas Hobor; Andrew W. Appel; Francesco Zappa Nardelli (ESOP, 2008)

Multimodal Separation Logic for Reasoning About Operational Semantics. - Robert Dockins; Andrew W. Appel; Aquinas Hobor (MFPS, 2008)

A Fresh Look at Separation Algebras and Share Accounting. - Robert Dockins; Aquinas Hobor; Andrew W. Appel (APLAS, 2009)

A Logical Mix of Approximation and Separation. - Aquinas Hobor; Robert Dockins; Andrew W. Appel (APLAS, 2010)

A Theory of Termination via Indirection. - Robert Dockins; Aquinas Hobor (Modelling, Controlling and Reasoning About State, 2010)

A theory of indirection via approximation. - Aquinas Hobor; Robert Dockins; Andrew W. Appel (POPL, 2010)

Teaching Experience: Logic and Formal Methods with Coq. - Martin Henz; Aquinas Hobor (CPP, 2011)

Barriers in Concurrent Separation Logic. - Aquinas Hobor; Cristian Gherghina (ESOP, 2011)

Decision Procedures over Sophisticated Fractional Permissions. - Xuan Bach Le; Cristian Gherghina; Aquinas Hobor (APLAS, 2012)

Barriers in Concurrent Separation Logic: Now With Tool Support! - Aquinas Hobor; Cristian Gherghina (Log. Methods Comput. Sci., 2012)

Time Bounds for General Function Pointers. - Robert Dockins; Aquinas Hobor (MFPS, 2012)

The ramifications of sharing in data structures. - Aquinas Hobor; Jules Villard (POPL, 2013)

A Resource-Based Logic for Termination and Non-termination Proofs. - Ton Chanh Le; Cristian Gherghina; Aquinas Hobor; Wei-Ngan Chin (ICFEM, 2014)

Certified Reasoning with Infinity. - Asankhaya Sharma; Shengyi Wang; Andreea Costea; Aquinas Hobor; Wei-Ngan Chin (FM, 2015)

Specifying Compatible Sharing in Data Structures. - Asankhaya Sharma; Aquinas Hobor; Wei-Ngan Chin (ICFEM, 2015)

On Power Splitting Games in Distributed Computation: The Case of Bitcoin Pooled Mining. - Loi Luu; Ratul Saha; Inian Parameshwaran; Prateek Saxena; Aquinas Hobor (IACR Cryptol. ePrint Arch., 2015)

Verifying Concurrent Graph Algorithms. - Azalea Raad; Aquinas Hobor; Jules Villard; Philippa Gardner (APLAS, 2016)

Decidability and Complexity of Tree Share Formulas. - Xuan Bach Le; Aquinas Hobor; Anthony W. Lin (FSTTCS, 2016)

Making Smart Contracts Smarter. - Loi Luu; Duc-Hiep Chu; Hrishi Olickel; Prateek Saxena; Aquinas Hobor (IACR Cryptol. ePrint Arch., 2016)

A Concurrent Perspective on Smart Contracts. - Ilya Sergey; Aquinas Hobor (Financial Cryptography Workshops, 2017)

A Certified Decision Procedure for Tree Shares. - Xuan Bach Le; Thanh-Toan Nguyen; Wei-Ngan Chin; Aquinas Hobor (ICFEM, 2017)

Finding The Greedy, Prodigal, and Suicidal Contracts at Scale. - Ivica Nikolic; Aashish Kolluri; Ilya Sergey; Prateek Saxena; Aquinas Hobor (ACSAC, 2018)

Complexity Analysis of Tree Share Structure. - Xuan Bach Le; Aquinas Hobor; Anthony W. Lin (APLAS, 2018)

Logical Reasoning for Disjoint Permissions. - Xuan Bach Le; Aquinas Hobor (ESOP, 2018)

Temporal Properties of Smart Contracts. - Ilya Sergey; Amrit Kumar 001; Aquinas Hobor (ISoLA (4), 2018)

Scilla: a Smart Contract Intermediate-Level LAnguage. - Ilya Sergey; Amrit Kumar 001; Aquinas Hobor (CoRR, 2018)

BesFS: Mechanized Proof of an Iago-Safe Filesystem for Enclaves. - Shweta Shinde; Shengyi Wang; Pinghai Yuan; Aquinas Hobor; Abhik Roychoudhury; Prateek Saxena (CoRR, 2018)

Pumping, with or Without Choice. - Aquinas Hobor; Elaine Li; Frank Stephan 001 (APLAS, 2019)

Exploiting the laws of order in smart contracts. - Aashish Kolluri; Ivica Nikolic; Ilya Sergey; Aquinas Hobor; Prateek Saxena (ISSTA, 2019)

Proof Pearl: Magic Wand as Frame. - Qinxiang Cao; Shengyi Wang; Aquinas Hobor; Andrew W. Appel (CoRR, 2019)

Certifying graph-manipulating C programs via localizations within data structures. - Shengyi Wang; Qinxiang Cao; Anshuman Mohan; Aquinas Hobor (Proc. ACM Program. Lang., 2019)

Reasoning over Permissions Regions in Concurrent Separation Logic. - James Brotherston; Diana Costa 001; Aquinas Hobor; John Wickerson (CAV (2), 2020)

A functional proof pearl: inverting the Ackermann hierarchy. - Linh Tran; Anshuman Mohan; Aquinas Hobor (CPP, 2020)

BesFS: A POSIX Filesystem for Enclaves with a Mechanized Safety Proof. - Shweta Shinde; Shengyi Wang; Pinghai Yuan; Aquinas Hobor; Abhik Roychoudhury; Prateek Saxena (USENIX Security Symposium, 2020)

Functional Correctness of C Implementations of Dijkstra's, Kruskal's, and Prim's Algorithms. - Anshuman Mohan; Wei Xiang Leow; Aquinas Hobor (CAV (2), 2021)

OverChain: Building a robust overlay with a blockchain. - Vijeth Aradhya; Seth Gilbert; Aquinas Hobor (CoRR, 2022)

Schooling to Exploit Foolish Contracts. - Tamer Abdelaziz; Aquinas Hobor (BCCA, 2023)

Smart Learning to Find Dumb Contracts. - Tamer Abdelaziz; Aquinas Hobor (USENIX Security Symposium, 2023)

Robust overlays meet blockchains: On handling high churn and catastrophic failures. - Vijeth Aradhya; Seth Gilbert; Aquinas Hobor (Theor. Comput. Sci., 2025)