Aquinas Hobor: Home

I am an Assistant Professor of Computer Science with a joint appointment between National University of Singapore's School of Computing and Yale-NUS College.  I was a Lee Kuan Yew Postdoctoral Fellow after I defended my PhD thesis from the Department of Computer Science of Princeton University.

I do research in verification, semantic models, machine-checked proof, and computer security.  Particular areas of recent interest are verifying graph-manipulating programs, developing certified decision procedures, parallel programming, and Bitcoin.

I am looking for PhD students who are interested in formal methods, machine-checked proofs, etc.  If you are interested, please email me your CV.

News

I have been invited to be on the program committee for APLAS 2015!

New paper (November 2014):
  Dropping Your Cake and Eating it Too: Profiting in
  Bitcoin Pools by Withholding Blocks
  by Loi Luu, Ratul Saha, Inian Parameshwaran,
  Prateek Saxena, and Aquinas Hobor

New paper (October 2014):
  Certified Reasoning with Infinity
  by Asankhaya Sharma, Shengyi Wang,
  Andreea Costea, Aquinas Hobor, and Wei-Ngan Chin

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

Book (Cambridge University Press 2014):
  Program Logics for Certified Compilers
 
(hardcover) (e-book)
  by Andrew W. Appel, Robert Dockins,
  Aquinas Hobor, Lennart Beringer, Josiah Dodds,
  Gordon Stewart, Sandrine Blazy, and Xavier Leroy

New paper (November 2013)
  Specifying Compatible Sharing in Data Structures
  with Asankhaya Sharma and Wei-Ngan Chin

I have been invited to be on the program committee for CPP 2013!

I have been invited to be on the program committee for HOPE 2013!

New paper (June 2013):
  Constructing Hereditary Worlds Within Worlds
  with Robert Dockins

Abstract (OBT 2013):
  VisualizeSLE: A Visual Editor for Separation Logic
  Entailments (video demo)
  with Soe Lin Myat and Bimlesh Wadhwa

Poster (APLAS 2012):
  VisualizeSLE: A Visual Editor for Separation Logic
  Entailments (abstract)
  with Soe Lin Myat and Bimlesh Wadhwa

Publication (POPL 2013):
  The Ramifications of Sharing in Data Structures
  with Jules Villard
  See also this associated technical report.

Publication (APLAS 2012):
  Decision Procedures over Sophisticated Fractional
  Permissions
  with Le Xuan Bach, Cristian Gherghina

Publication (MFPS 2012):
  Verifying Time Bounds for General Function Pointers
  with Robert Dockins

I have been invited to be on the program committee for APLAS 2012!

Publication (LMCS):
  Barriers in Concurrent Separation Logic: Now with
  Tool Support!
  with Cristian Gherghina

I have been invited to become the Co-Chair (with Chin Wei Ngan) for FTfJP 2012Submit a paper!

New paper (July 2011):
  Improving the Compositionality of Separation
  Algebras

Publication (CPP 2011):
  Introducing Logic and Formal Methods with Coq
  with Martin Henz

Software release (12/8/2010): MSL v0.3
  with Robert Dockins and Andrew W. Appel

Publication (ESOP 2011):
  Barriers in Concurrent Separation Logic
  with Cristian Gherghina

Tutorial presentation (APLAS 2010, 11/28/10):
  Developing and Mechanizing Semantic Models for
  Program Logics
  with Robert Dockins
  (associated with A Logical Mix of Approximation and
  Separation)

Publication (Dagstuhl Seminar 10351):
  A Theory of Termination via Indirection
  with Robert Dockins

Publication (APLAS 2010, 11/28/10):
  A Logical Mix of Approximation and Separation
  with Robert Dockins and Andrew W. Appel
  (associated with Developing and Mechanizing
  Semantic Models for Program Logics)

Publication (POPL 2010, 1/21/10):
  A Theory of Indirection via Approximation
  with Robert Dockins and Andrew W. Appel

Publication (APLAS 2009, 12/15/09):
  A Fresh Look at Separation Algebras and Share
  Accounting
  with Robert Dockins and Andrew W. Appel

Aquinas Hobor

web site by Lucy Day Hobor ~ 2008-2014