Aquinas Hobor: Publications
(BIB : all)
Under submission
A Specification Logic for
Termination Reasoning (PDF)
Ton-Chanh Le, Cristian Gherghina, Aquinas Hobor, Wei-Ngan
Chin
2012
Barriers in Concurrent
Separation Logic: Now With Tool Support! (PDF)
Aquinas Hobor, Cristian Gherghina
2011
See also this associated ESOP 2011
paper.
Verifying Time Bounds for General
Function Pointers (PDF,
BIB)
Robert Dockins, Aquinas Hobor
2011
See also this associated unreviewed Dagstuhl
paper.
Invited
Developing and Mechanizing Semantic Models for Program Logics
(PPT)
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.
Peer-reviewed
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,
BIB)
Aquinas Hobor, Cristian Gherghina
20th European Symposium of Programming (ESOP 2011), pp.
276-296, April 2011.
See also this associated journal
submission.
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.
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.
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.
Ph.D. Thesis
Oracle Semantics (PDF,
PPT : Thesis defense,
BIB)
Aquinas Hobor
Ph.D. Thesis, Princeton TR-836-08, October 2008.
Unreviewed
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 this associated 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.
Co-authors
Andrew W. Appel,
C. J. Bell,
Wei-Ngan Chin,
Robert Dockins,
Cristian
Gherghina, Martin Henz,
Ton-Chanh Le,
Francesco Zappa Nardelli,
David Walker