| 2023 | SSS | Robust Overlays Meet Blockchains - On Handling High Churn and Catastrophic Failures. | Vijeth Aradhya, Seth Gilbert, Aquinas Hobor |
| 2021 | CAV | Functional Correctness of C Implementations of Dijkstra's, Kruskal's, and Prim's Algorithms. | Anshuman Mohan, Wei Xiang Leow, Aquinas Hobor |
| 2020 | CAV | Reasoning over Permissions Regions in Concurrent Separation Logic. | James Brotherston, Diana Costa, Aquinas Hobor, John Wickerson |
| 2020 | CPP | A functional proof pearl: inverting the Ackermann hierarchy. | Linh Tran, Anshuman Mohan, Aquinas Hobor |
| 2019 | APLAS | Pumping, with or Without Choice. | Aquinas Hobor, Elaine Li, Frank Stephan |
| 2019 | ISSTA | Exploiting the laws of order in smart contracts. | Aashish Kolluri, Ivica Nikolic, Ilya Sergey, Aquinas Hobor, Prateek Saxena |
| 2018 | ACSAC | Finding The Greedy, Prodigal, and Suicidal Contracts at Scale. | Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek Saxena, Aquinas Hobor |
| 2018 | APLAS | Complexity Analysis of Tree Share Structure. | Xuan Bach Le, Aquinas Hobor, Anthony W. Lin |
| 2018 | ESOP | Logical Reasoning for Disjoint Permissions. | Xuan Bach Le, Aquinas Hobor |
| 2018 | ISoLA | Temporal Properties of Smart Contracts. | Ilya Sergey, Amrit Kumar, Aquinas Hobor |
| 2017 | FC | A Concurrent Perspective on Smart Contracts. | Ilya Sergey, Aquinas Hobor |
| 2017 | ICFEM | A Certified Decision Procedure for Tree Shares. | Xuan Bach Le, Thanh-Toan Nguyen, Wei-Ngan Chin, Aquinas Hobor |
| 2016 | APLAS | Verifying Concurrent Graph Algorithms. | Azalea Raad, Aquinas Hobor, Jules Villard, Philippa Gardner |
| 2016 | CCS | Making Smart Contracts Smarter. | Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, Aquinas Hobor |
| 2015 | FM | Certified Reasoning with Infinity. | Asankhaya Sharma, Shengyi Wang, Andreea Costea, Aquinas Hobor, Wei-Ngan Chin |
| 2015 | ICFEM | Specifying Compatible Sharing in Data Structures. | Asankhaya Sharma, Aquinas Hobor, Wei-Ngan Chin |
| 2014 | ICFEM | A Resource-Based Logic for Termination and Non-termination Proofs. | Ton Chanh Le, Cristian Gherghina, Aquinas Hobor, Wei-Ngan Chin |
| 2013 | POPL | The ramifications of sharing in data structures. | Aquinas Hobor, Jules Villard |
| 2012 | APLAS | Decision Procedures over Sophisticated Fractional Permissions. | Xuan Bach Le, Cristian Gherghina, Aquinas Hobor |
| 2011 | CPP | Teaching Experience: Logic and Formal Methods with Coq. | Martin Henz, Aquinas Hobor |
| 2011 | ESOP | Barriers in Concurrent Separation Logic. | Aquinas Hobor, Cristian Gherghina |
| 2010 | APLAS | A Logical Mix of Approximation and Separation. | Aquinas Hobor, Robert Dockins, Andrew W. Appel |
| 2010 | POPL | A theory of indirection via approximation. | Aquinas Hobor, Robert Dockins, Andrew W. Appel |
| 2009 | APLAS | A Fresh Look at Separation Algebras and Share Accounting. | Robert Dockins, Aquinas Hobor, Andrew W. Appel |
| 2008 | ESOP | Oracle Semantics for Concurrent Separation Logic. | Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli |