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

New paper (July 2016):
  Decidability and Complexity of Tree Share Formulas
  with Xuan Bach Le and Anthony W. Lin

New paper (July 2016):
  The Ramifications of Mechanized Localizations
  within Data Structures
  with Shengyi Wang, Qinxiang Cao, and
  Asankhaya Sharma

New paper (June 2016):
  A Certified Decision Procedure for Sophisticated
  Fractional Permissions
  with Xuan Bach Le

New paper (June 2016):
  Verifying Concurrent Graph Algorithms
  with Azalea Raad, Jules Villard, and
  Philippa Gardner

New paper (May 2016):
  Making Smart Contracts Smarter
  with Loi Luu, Duc-Hiep Chu, Hrishi Olickel, and
  Prateek Saxena

I am on the program committee for the BITCOIN 16!

Publication (ICFEM 2015)
  Specifying Compatible Sharing in Data Structures
  with Asankhaya Sharma and Wei-Ngan Chin

Publication (CSF 2015):
  On Power Splitting Games in Distributed
  Computation: The Case of Bitcoin Pooled Mining
  with Loi Luu, Ratul Saha, Inian Parameshwaran,
  and Prateek Saxena

Publication (FM 2015):
  Certified Reasoning with Infinity
  with Asankhaya Sharma, Shengyi Wang,
  Andreea Costea, and Wei-Ngan Chin

I am on the program committee for APLAS 2015!

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

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

I am 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 am on the program committee for APLAS 2012!

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

I am 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-2015