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, certified decision procedures, parallel programming, and cryptocurrencies.

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 am on the program committee for CPP 2019!

I am on the program committee for BSCT 2018!

Paper (May 2018)
  BesFS: Mechanized Proof of an Iago-Safe
  Filesystem for Enclaves
  with Shweta Shinde, Shengyi Wang, Pinghai Yuan,
  Abhik Roychoudhury, and Prateek Saxena

Paper (May 2018)
  Exploiting the Laws of Order in Smart Contracts
  with Ivica Nikolic, Aashish Kolluri, Ilya Sergey,
  and Prateek Saxena

I am on the program committee for APLAS 2018!

Publication (ESOP 2018):
  Logical Reasoning over Disjoint Permissions
  with Xuan Bach Le

Paper (March 2018)
  Finding the Greedy, Prodigal, and Suicidal Contracts
  at Scale
  with Ivica Nikolic, Aashish Kolluri, Ilya Sergey,
  and Prateek Saxena

Paper (January 2018)
  SCILLA: a Smart Contract Intermediate-Level
  LAnguage
  with Ilya Sergey and Amrit Kumar

Student (December 2017)
  Xuan Bach Le has defended his thesis!

Poster (APLAS 2017)
  Mechanized Verification of Graph-Manipulating
  Programs
  with Shengyi Wang and Qinxiang Cao

Grant (June 2017)
  Verification of a Garbage Collector, Graph-
  Manipulating Programs and Cryptocurrency

I am on the program committee for BTA18!

I am on the program committee for the BITCOIN 18!

Publication (ICFEM 2017):
  A Certified Decision Procedure for Tree Shares
  with Xuan Bach Le, Thanh Toan Nguyen, and
  Wei Ngan Chin

Keynote (RTST 2017):
  Formal Methods in Software Development

Publication (WTSC 2017):
  A Concurrent Perspective on Smart Contracts
  with Ilya Sergey

Publication (FSTTCS 2016):
  Decidability and Complexity of Tree Share Formulas
  with Xuan Bach Le and Anthony W. Lin

Publication (APLAS 2016):
  Verifying Concurrent Graph Algorithms
  with Azalea Raad, Jules Villard, and
  Philippa Gardner

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

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

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-2018