Aquinas Hobor: Publications
(Google Scholar, BIB : all)
Book
Program Logics for Certified Compilers (hardcover,
e-book)
Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer,
Josiah Dodds, Gordon Stewart, Sandrine Blazy, Xavier Leroy
Cambridge University Press 2014.
Oracle Semantics (PDF,
PPT : Thesis defense,
BIB)
Aquinas Hobor
Ph.D. Thesis, Princeton TR-836-08, October 2008.
Conference
BesFS: A POSIX Filesystem for Enclaves with a Mechanized
Safety Proof (PDF, slides:
, code:
GitHub)
Shweta Shinde, Shengyi Wang, Pinghai Yuan, Aquinas Hobor,
Abhik Roychoudhury, Prateek Saxena
20th USENIX Security Symposium (USENIX Security 2020), pp.,
August 2020.
A
Functional Proof Pearl: Inverting the Ackermann Hierarchy (PDF,
slides: PDF by
Linh Tran, code:
GitHub)
Linh Tran, Anshuman Mohan, Aquinas Hobor
9th ACM-SIGPLAN International Conference on Certified Programs and
Proofs (CPP 2020), pp. 129-142, January 2020.
See also the associated
technical report
for more detail.
Pumping, With or Without Choice (PDF,
slides: PDF by
Elaine Li, code:
GitHub)
Aquinas Hobor, Elaine Li, Frank Stephan
17th Asian Symposium on Programming Languages and Systems
(APLAS 2019), pp. 427-446, December 2019.
Certifying Graph-Manipulating C Programs via Localizations within Data Structures (PDF,
slides: PDF by
Shengyi Wang)
Shengyi Wang, Qinxiang Cao, Anshuman Mohan, Aquinas Hobor
PACMPL (OOPSLA 2019), pp. 171:1-171:30, October 2019.
See also a
poster by Shengyi Wang and another
poster by Anshuman
Mohan.
Exploiting the Laws of Order in Smart Contracts (PDF,
PPT: by Aashish
Kolluri)
Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Aquinas
Hobor, Prateek Saxena
28th International Symposium of Software Testing
and Analysis (ISSTA 2019), pp. 363-373, July 2019.
Finding the Greedy,
Prodigal, and Suicidal Contracts at Scale (PDF,
PPT: by Aashish
Kolluri)
Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek
Saxena, Aquinas Hobor
34th Annual Computer Security Applications Conference (ACSAC
2018), pp. 653-663, December 2018.
Complexity Analysis of Tree Share Structure (PDF,
slides: PDF by Xuan Bach Le)
Xuan Bach Le, Aquinas Hobor, Anthony W. Lin
16th Asian Symposium on Programming Languages and Systems
(APLAS 2018), pp. 89-108, December 2018.
Temporal Properties of Smart Contracts (PDF)
Ilya Sergey, Amrit Kumar, Aquinas Hobor
8th International Symposium On Leveraging
Applications of Formal Methods, Verification and Validation (ISoLA
2018), pp. 323-338, November 2018.
Logical Reasoning for Disjoint Permissions
(PDF, slides:
PDF by Xuan Bach Le)
Xuan Bach Le, Aquinas
Hobor
27th European Symposium of Programming (ESOP 2018), pp.
385-414, April 2018.
See also the associated Coq
proofs and
ShareInfer tool.
A Certified Decision Procedure for Tree Shares
(PDF, slides:
PDF by Xuan
Bach Le)
Xuan Bach Le, Thanh Toan Nguyen, Wei Ngan Chin, Aquinas
Hobor
19th International Conference on Formal
Engineering Methods (ICFEM 2017), pp. 226-242, November 2017.
See also the associated certified
tool.
Decidability and Complexity of
Tree Share Formulas (PDF,
slides: PDF by Xuan Bach Le)
Xuan Bach Le, Aquinas Hobor, Anthony W. Lin
36th IARCS Annual Conference on Foundations
of Software Technology and Theoretical Computer Science (FSTTCS 2016),
pp. 19:1-19:14, December 2016.
Verifying Concurrent Graph Algorithms (PDF,
slides: PDF by Azalea Raad)
Azalea Raad, Aquinas Hobor, Jules Villard, Philippa
Gardner
14th Asian Symposium on Programming
Languages and Systems (APLAS 2016), pp. 314-334, November 2016.
Making Smart Contracts Smarter (PDF,
PPT: by Hrishi Olickel)
Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, Aquinas Hobor
23rd ACM Conference on Computer and
Communications Security (CCS 2016), pp. 254-269, October 2016.
Specifying Compatible Sharing
in Data Structures (PDF,
PPT: by Asankhaya Sharma)
Asankhaya Sharma, Aquinas Hobor, Wei-Ngan
Chin
17th International Conference on Formal Engineering Methods
(ICFEM 2015), pp. 349-365, November 2015.
On Power Splitting Games in Distributed Computation:
The Case of Bitcoin Pooled Mining (PDF,
PPT : by Loi
Luu)
Loi Luu, Ratul Saha, Inian Parameshwaran, Prateek
Saxena, Aquinas Hobor
28th IEEE Computer Security Foundations Symposium (CSF
2015),
pp. 397-411, July 2015.
See also this associated technical
report.
Certified Reasoning with Infinity (PDF;
slides: PDF, by Shengyi
Wang)
Asankhaya Sharma, Shengyi Wang, Andreea Costea, Aquinas
Hobor,
Wei-Ngan
Chin
20th International Symposium on Formal Methods (FM 2015),
pp. 496-513, June 2015.
A Resource-Based Logic for
Termination and Non-Termination Proofs (PDF,
PPT : by Ton Chanh Le)
Ton Chanh Le, Cristian Gherghina, Aquinas Hobor, Wei-Ngan
Chin
16th International Conference on Formal Engineering Methods
(ICFEM 2014), pp. 267-283, November 2014.
The Ramifications of Sharing
in Data Structures (PDF,
slides: PDF, by
Jules Villard)
Aquinas Hobor, Jules Villard
The 40th ACM SIGACT-SIGPLAN Symposium on
Principles of Programming Languages (POPL 2013), pp. 523-536, January 2013.
See also this associated technical report.
Decision Procedures over
Sophisticated Fractional Permissions (PDF,
slides: PDF)
Le Xuan Bach, Cristian Gherghina, Aquinas Hobor
The 10th Asian Symposium on Programming
Languages and Systems (APLAS 2012), pp. 368-385, December 2012.
Verifying Time Bounds for General
Function Pointers (PDF,
PPT,
BIB)
Robert Dockins, Aquinas Hobor
Twenty-Eighth Conference on the Mathematical Foundations of
Programming Semantics (MFPS 2012), June 2012. ENTCS Vol.
XX, 2012, pp. 132-148.
See also this associated unreviewed Dagstuhl
paper.
Teaching Experience: Logic and Formal Methods with Coq
(PDF,
PPT,
BIB)
Martin Henz, Aquinas Hobor
1st International Conference on Certified Programs and
Proofs (CPP 2011), pp. 199-215, December 2011.
See also some lecture notes here
and additional course material
here.
Barriers in Concurrent Separation Logic (PDF,
PPT : by C. Gherghina,
BIB)
Aquinas Hobor, Cristian Gherghina
20th European Symposium of Programming (ESOP 2011), pp.
276-296, April 2011.
See also this associated journal
paper.
A Theory of Indirection via Approximation (PDF,
BIB)
Aquinas Hobor, Robert Dockins, Andrew W. Appel
37th ACM SIGACT-SIGPLAN Symposium on Principles of
Programming Languages (POPL 2010), pp. 171-185, January 2010.
A Fresh Look at Separation Algebras and Share
Accounting (PDF,
BIB)
Robert Dockins, Aquinas Hobor, Andrew W. Appel
The 7th Asian Symposium on Programming Languages and Systems
(APLAS 2009), pp. 161-177, December
2009.
Oracle Semantics for Concurrent Separation Logic
(PDF,
PPT,
BIB)
Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli
17th European Symposium of Programming (ESOP 2008), pp.
353-367, April 2008.
See also the associated technical report
for more detail.
Invited
Formal Methods in Software Development
(PPT)
Aquinas Hobor
10th National Workshop on Recent Trends in Software Testing
(RTST17), July 2017.
Keynote talk.
Disjoint Semirings for Fractional Permissions (PPT)
The Aarhus Concurrency Workshop on Concurrency
Theory, May 2017.
Also presented at Cambridge University, June 2017.
A preview of the work later published at ESOP 2018.
Mechanized Verification for Graph Algorithms (PDF)
Aquinas Hobor
6th South of England Regional Programming Language
Seminar (S-REPLS 6), May 2017.
Developing and Mechanizing Semantic Models for Program Logics
(PDF:
presentation, PDF:
for printing)
Aquinas Hobor, Robert Dockins
The 8th Asian Symposium on Programming Languages
and Systems (APLAS 2010), November/December 2010.
A tutorial associated with the following publication.
A Logical Mix of Approximation and Separation
(PDF,
BIB)
Aquinas Hobor, Robert Dockins, Andrew W. Appel
The 8th Asian Symposium on Programming Languages
and Systems (APLAS 2010), pp. 439-454, November/December 2010.
A paper associated with the previous tutorial presentation.
Multimodal Separation Logic for Reasoning About
Operational Semantics (PDF,
BIB)
Robert Dockins, Andrew W. Appel, Aquinas Hobor
Twenty-Fourth Conference on Mathematical Foundations of
Programming Semantics (MFPS 2008), May 2008. ENTCS Vol.
218, Oct. 22, 2008, pp. 5-20.
Journal
Barriers in Concurrent Separation Logic: Now With Tool Support!
(PDF,
BIB)
Aquinas Hobor, Cristian Gherghina
Selected Papers of the 20th European Symposium on
Programming (ESOP 2011), April 2012. Logical Methods in
Computer Science, Vol. 8, pp 1-36.
See also this associated ESOP 2011
paper.
Workshop, etc.
A Certified Version of Dijkstra's Shortest-Path
(PDF: poster)
Shengyi Wang, Anshuman Mohan, Qinxiang Cao, Aquinas Hobor
Poster session of The 17th Asian Symposium on
Programming Languages and Systems (APLAS 2019), December 2019.
See also the associated
paper.
A Verified Garbage Collector for Gallina (PDF:
slides)
Shengyi Wang, Anshuman Mohan, Qinxiang Cao, Aquinas Hobor
APLAS NIER, December 2019.
Certifying Graph-Manipulating C Programs
(PDF: poster)
Shengyi Wang, Qinxiang Cao, Anshuman Mohan, Aquinas Hobor
Poster session OOPSLA 2019, October 2019.
See also the associated conference
paper.
Mechanized Verification of
Graph-Manipulating Programs
(PDF: poster)
Shengyi Wang, Qinxiang Cao, Aquinas Hobor
Poster session of The 15th Asian Symposium on
Programming Languages and Systems (APLAS 2017), November 2017.
See also the associated conference
paper.
A Concurrent Perspective on
Smart Contracts
(PDF)
Ilya Sergey,
Aquinas Hobor
First Workshop on Trusted Smart Contracts (WTSC 2017), April 2017.
Decidability and Complexity of Tree Share Formulas
(PDF: poster)
Le Xuan Bach,
Aquinas Hobor, Anthony W. Lin
Poster session of The 14th Asian Symposium on
Programming Languages and Systems (APLAS 2016), November 2016.
VisualizeSLE: A Visual Editor for Separation Logic
Entailments
(PDF:
abstract, YouTube:
video demo)
Aquinas Hobor, Soe Lin Myat, Bimlesh Wadhwa
Off the Beaten Track (OBT 2013), January 2013.
VisualizeSLE: A Visual Editor for Separation Logic
Entailments
(PDF: poster, PDF:
abstract)
Aquinas Hobor, Soe Lin Myat, Bimlesh Wadhwa
Poster session of The 10th Asian Symposium on
Programming Languages and Systems (APLAS 2012).
Comparing Semantic and Syntactic Methods in
Mechanized Proof Frameworks
(PDF,
PPT : by C. J. Bell,
BIB)
C. J. Bell, Robert Dockins, Aquinas Hobor,
Andrew W. Appel, David Walker
Second International Workshop on Proof-Carrying Code (PCC 2008),
June 2008.
Under submission
Reasoning over Permissions Regions in Concurrent Separation
Logic (PDF)
James Brotherston, Diana Costa, Aquinas Hobor, John
Wickerson
2020
A Machine-Checked C Implementation of Dijkstra's Shortest Path
Algorithm (PDF)
Anshuman Mohan, Shengyi Wang, Aquinas Hobor
2020
See also the associated
poster.
Magic Wand as Frame
(PDF)
Qinxiang Cao, Shengyi Wang, Aquinas Hobor, Andrew W.
Appel
2018
Constructing Hereditary Worlds Within Worlds (PDF)
Robert Dockins, Aquinas Hobor
2012
Unreviewed
A Functional Proof Pearl:
Inverting the Ackermann Hierarchy Extended Version (PDF)
Linh Tran, Anshuman Mohan,
Aquinas Hobor
January 2020.
See also the associated conference
paper.
BesFS: Mechanized Proof of an
Iago-Safe Filesystem for Enclaves (PDF)
Shweta Shinde, Shengyi Wang, Pinghai Yuan, Aquinas Hobor,
Abhik Roychoudhury, Prateek Saxena
arXiv:1807.00477, July 2018.
See also the associated conference paper.
Finding the Greedy,
Prodigal, and Suicidal Contracts at Scale (PDF)
Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek
Saxena, Aquinas Hobor
arXiv:1802.06038v2, March 2018.
See also the associated conference
paper.
SCILLA: a Smart Contract
Intermediate-Level LAnguage (PDF)
Ilya Sergey, Amrit Kumar, Aquinas Hobor
arXiv:1801.00687v1, January 2018.
On Power Splitting Games in Distributed Computation:
The Case of Bitcoin Pooled Mining (PDF)
Loi Luu, Ratul Saha, Inian Parameshwaran, Prateek
Saxena, Aquinas Hobor
See also the associated conference
paper.
The Ramifications of Sharing in
Data Structures (extended version) (PDF)
Aquinas Hobor, Jules Villard
2012
See also the associated conference
paper.
Improving the Compositionality of Separation Algebras
(PDF,
BIB)
Aquinas Hobor
2011
Lecture notes on formal induction
(PDF)
and Hoare logic (PDF)
Aquinas Hobor
2010
Lecture notes from when I co-taught CS3234 with Martin Henz.
This material may be developed into a book. Additional
material from that course may be found
here.
See also the associated conference paper.
A Theory of Termination via Indirection
(PDF,
PPT,
BIB)
Robert Dockins, Aquinas Hobor
Modelling, Controlling and Reasoning About State, Dagstuhl Seminar 10341 Proceedings, 2010.
See also the associated conference paper.
Oracle Semantics for Concurrent Separation Logic
(Extended Version) (PDF,
PPT : Job Talk,
BIB)
Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli
Princeton TR-825-08, June 2008.
See also the associated conference
paper.
Software and Projects
ShareInfer
Le Xuan Bach, Aquinas Hobor
Certified
Share Solver
Le Xuan Bach, Aquinas Hobor
Coq Soundness
Proof for Disjoint Permission Logic
Le Xuan Bach, Aquinas Hobor
Bare-Bones Verified
Compiler
Aquinas Hobor
Coq Soundness Proof
for Barrier Logic
Aquinas Hobor, Cristian Gherghina
HIP/SLEEK Barrier Verifier
Cristian Gherghina, Aquinas Hobor
Mechanized
Semantic Library
Andrew W. Appel, Robert Dockins, Aquinas Hobor
Prototype Decision Procedure Over Sophisticated Fractional
Permissions
Cristian Gherghina, Aquinas Hobor, Le Xuan Bach
Verified Software
Toolchain
Andrew W. Appel et al.
VisualizeSLE
Aquinas Hobor, Soe Lin Myat, Bimlesh Wadhwa
Professional Services
3rd Workshop on Blockchain and Smart Contract
Technologies
(BSCT 2020)
17th Asian Symposium on Programming Languages and Systems
(APLAS 2019)
Program Committee
2nd Workshop on Blockchain and Smart Contract Technologies
(BSCT 2019)
8th ACM SIGPLAN Conference on Certified Programs and
Proofs
(CPP
2019)
Program Committee
16th Asian Symposium on Programming Languages and Systems
(APLAS 2018)
Program Committee
1st IEEE Workshop on Blockchain Technologies and Applications
(BTA 2018)
Program Committee
5th Workshop on Bitcoin and Blockchain Research
(BITCOIN 2018)
Program Committee
3rd Workshop on Bitcoin and Blockchain Research
(BITCOIN 2016)
Program Committee
13th Asian Symposium on Programming Languages and
Systems (APLAS 2015)
Program Committee
The 3rd International Conference on Certified Programs and
Proofs (CPP
2013)
Program Committee
The 2nd ACM SIGPLAN Workshop on Higher-Order Programming with
Effects (HOPE
2013)
Program Committee
10th Asian Symposium on Programming Languages and
Systems (APLAS 2012)
Program Committee
Formal Techniques for Java-like Programs (FTfJP
2012)
Co-Chair (with
Chin Wei Ngan)
Co-authors
Andrew W. Appel,
C. J. Bell,
Lennart Beringer,
Sandrine Blazy,
James
Brotherston,
Qinxiang
Cao, Wei-Ngan Chin,
Diane Costa,
Andreea Costea,
Robert Dockins,
Josiah Dodds,
Philippa Gardner,
Cristian
Gherghina, Martin Henz,
Aashish Kolluri,
Amrit
Kumar, Ton-Chanh Le,
Le Xuan Bach,
Xavier Leroy,
Elaine Li,
Anthony W. Lin,
Loi Luu,
Anshuman Mohan,
Soe Lin Myat,
Francesco Zappa Nardelli,
Thanh Toan Nguyen,
Ivica Nikolic,
Inian Parameshwaran,
Azalea Raad,
Abhik Roychoudhury,
Ratul Saha,
Prateek Saxena,
Ilya Sergey,
Asankhaya Sharma,
Shweta Shinde,
Gordon Stewart,
Linh Tran,
Jules Villard,
David Walker,
Bimlesh Wadhwa,
Shengyi Wang,
Pinghai Yuan