Aquinas Hobor: Publications

(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

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)
Aquinas Hobor, Jules Villard
The 40th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 2013), January 2013.
See also this associated technical report.

Decision Procedures over Sophisticated Fractional Permissions (PDF)
Le Xuan Bach, Cristian Gherghina, Aquinas Hobor
The 10th Asian Symposium on Programming Languages and Systems (APLAS 2012), 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

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.

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

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

The Ramifications of Mechanized Localizations within Data Structures (PDF)
Shengyi Wang, Qinxiang Cao, Asankhaya Sharma, Aquinas Hobor
2016

A Certified Decision Procedure for Sophisticated Fractional Permissions (PDF)
Xuan Bach Le, Aquinas Hobor
2016

Verifying Concurrent Graph Algorithms (PDF)
Azalea Raad, Aquinas Hobor, Philippa Gardner, Jules Villard
2016

Making Smart Contracts Smarter (PDF)
Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, Aquinas Hobor
2016

Constructing Hereditary Worlds Within Worlds
(PDF)
Robert Dockins, Aquinas Hobor
2012

Unreviewed

On Power Splitting Games in Distributed Computation: The Case of Bitcoin Pooled Mining (PDF)
Loi Luu, Ratul Saha, Inian Parameshwaran, Prateek Saxena, Aquinas Hobor
28th IEEE Computer Security Foundations Symposium (CSF 2015), to appear, July 2015.
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

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 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, Wei-Ngan Chin,
Andreea Costea, Robert Dockins, Josiah Dodds, Philippa Gardner,
Cristian Gherghina, Martin Henz, Ton-Chanh Le, Le Xuan Bach, Xavier Leroy,
Loi Luu, Soe Lin Myat, Francesco Zappa Nardelli, Inian Parameshwaran,
Azalea Raad, Ratul Saha, Prateek Saxena, Asankhaya Sharma, Gordon Stewart,
Jules Villard, David Walker, Bimlesh Wadhwa, Shengyi Wang

web site by Lucy Day Hobor ~ 2008-2015