Aquinas Hobor: Curriculum Vitae

(Also available as a PDF)

Education

Princeton University, Princeton, New Jersey
    PhD, Computer Science, 2008; thesis title: Oracle Semantics
    MA, Computer Science, 2005

The University of Chicago
, Chicago, Illinois
    BS, Honors, Mathematics, 2003
    BS, Honors, Computer Science, 2003
    Honors in the College, 2003

Honors & Awards

Lee Kuan Yew Postdoctoral Fellowship
    http://www.nus.edu.sg/dpr/funding/lky.html
    2008, Republic of Singapore

First Year Fellowship
    2003, Princeton University

ACM Programming Contest World Finalist
    2002, Association for Computing Machinery

Dean’s List
    1999-2003, The University of Chicago

Employment

National University of Singapore, Singapore
    Summer 2013 – Present: Assistant Professor
    Fall 2011 – Summer 2013: Lecturer
    Fall 2008 – Fall 2011: Lee Kuan Yew Postdoctoral Fellow

Princeton University
, Princeton, New Jersey
    Spring 2006 – Summer 2008: Research Assistant
    Spring 2005 – Fall 2005: Teaching Assistant
    Fall 2004: Research Assistant

Institut National de Recherche en Informatique et Automatique (INRIA), Rocquencourt, France
    Summer 2007: Research Intern

Microsoft Corporation, Redmond, Washington
    Summer 2005: Research Intern
    Summer 2001 & 2002: Software Development Intern

Lapides Asset Management, Greenwich, Connecticut
    Summer 2006: Financial Analyst Intern

William Blair & Company, Chicago, Illinois
    Summer 2003: Financial Analyst Intern

General Growth Properties, Chicago, Illinois
    Summer 2003: Investor Relations Intern

The University of Chicago, Chicago, Illinois
    Spring 2003 – Spring 2000: Teaching Assistant or Grader, 13 courses

FindMRO.com, Lake Forest, Illinois
    Summer 2000: Web site development

VIGRE Program, The University of Chicago, Chicago, Illinois
    Summer 2000: Teaching mathematics to high school students

Publications

Books

Program Logics for Certified Compilers
    Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer,
    Josiah Dodds, Gordon Stewart, Sandrine Blazy, Xavier Leroy
    Cambridge University Press, 2014.
    My chapters are on the Mechanized Semantic Library and Indirection Theory
    48 citations

Oracle Semantics
   
Aquinas Hobor
    Ph.D. Thesis, Princeton University, Department of Computer Science,
    October 2008 (TR-836-08).
   
26 citations

Refereed Conference Publications

Specifying Compatible Sharing in Data Structures
    Asankhaya Sharma, Aquinas Hobor, Wei-Ngan Chin
    17th International Conference on Formal Engineering Methods
    (ICFEM 2015), pp. 349-365, November 2015.
   
3 citations

On Power Splitting Games in Distributed Computation: The Case of Bitcoin Pooled Mining
    Loi Luu, Ratul Saha, Inian Parameshwaran, Prateek Saxena, Aquinas Hobor
    28th IEEE Computer Security Foundations Symposium (CSF 2015),
    pp. 397-411, July 2015.
   
10 citations

Certified Reasoning with Infinity
    Asankhaya Sharma, Shengyi Wang, Andreea Costea, Aquinas Hobor,
    Wei-Ngan Chin
    20th International Symposium on Formal Methods (FM 2015), pp. 496-513,
    June 2015.
   
1 citation

A Resource-Based Logic for Termination and Non-Termination Proofs
   
Ton Chanh Le, Cristian Gherghina, Aquinas Hobor, Wei-Ngan Chin
    16th International Conference on Formal Engineering Methods
    (ICFEM 2014), pp. 267-283, November 2014.
   
8 citations

The Ramifications of Sharing in Data Structures
    Aquinas Hobor, Jules Villard
    The 40th ACM SIGACT-SIGPLAN Symposium on Principles of
    Programming Languages (POPL 2013), January 2013
   
32 citations

Decision Procedures over Sophisticated Fractional Permissions
    Le Xuan Bach, Cristian Gherghina, Aquinas Hobor
    The 10th Asian Symposium on Programming Languages and
    Systems (APLAS 2012), December 2012.

    5 citations

Verifying Time Bounds for General Function Pointers

    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.
   
10 citations

Introducing Logic and Formal Methods with Coq
   
Martin Henz, Aquinas Hobor
    1st International Conference on Certified Programs and Proofs (CPP 2011),
    pp. 199-215, December 2011.
   
2 citations

Barriers in Concurrent Separation Logic
    Aquinas Hobor, Cristian Gherghina
    20th European Symposium of Programming (ESOP 2008), pp. 276-296,
    April 2011.
    Associated with the journal paper with similar name.
   
25 citations

A Theory of Indirection via Approximation
    Aquinas Hobor, Robert Dockins, Andrew W. Appel
    37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming
    Languages (POPL 2010), pp. 171-185, January 2010.

   
29 citations

A Fresh Look at Separation Algebras and Share Accounting
    Robert Dockins, Aquinas Hobor, Andrew W. Appel
    The 7th Asian Symposium on Programming Languages and Systems
    (APLAS 2009), pp. 161-177, December 2009.
    78 citations

Oracle Semantics for Concurrent Separation Logic
    Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli
    17th European Symposium of Programming (ESOP 2008), pp. 353-367,
    March/April 2008.
    130 citations

Refereed Journal Publications

Barriers in Concurrent Separation Logic: Now with Tool Support!
    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.

    Associated with the ESOP 2011 paper with similar name.
    14 citations

Invited

Developing and Mechanizing Semantic Models for Program Logics
    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
    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.
    6 citations

Multimodal Separation Logic for Reasoning About Operational Semantics
    Robert Dockins, Andrew W. Appel, Aquinas Hobor
    24th Conference on Mathematical Foundations of Programming Semantics
    (MFPS 2008), May 2008.  ENTCS Vol. 218, Oct. 22, 2008, pp. 5-20.
    8 citations

Refereed Workshop Publications

VisualizeSLE: A Visual Editor for Separation Logic Entailments
    Aquinas Hobor, Soe Lin Myat, Bimlesh Wadhwa
    Off the Beaten Track 2013 (OBT 2013).
   
Abstract & Video Demo.

VisualizeSLE: A Visual Editor for Separation Logic Entailments
    Aquinas Hobor, Soe Lin Myat, Bimlesh Wadhwa
    Poster session for APLAS 2012.
   
Poster & Poster Abstract.

Comparing Semantic and Syntactic Methods in Mechanized Proof Frameworks
    C. J. Bell, Robert Dockins, Aquinas Hobor, Andrew W. Appel, David Walker
    2nd International Workshop on Proof-Carrying Code (PCC 2008).  June 2008.
   
2 citations

Under Submission

Decidability and Complexity of Tree Share Formulas
    Xuan Bach Le, Aquinas Hobor, Anthony W. Lin
    Under submission, July 2016

The Ramifications of Mechanized Localizations within Data Structures
    Shengyi Wang, Qinxiang Cao, Asankhaya Sharma, Aquinas Hobor
    Under submission, July 2016

A Certified Decision Procedure for Sophisticated Fractional Permissions
    Xuan Bach Le, Aquinas Hobor
    Under submission, June 2016

Verifying Concurrent Graph Algorithms
    
Azalea Raad, Aquinas Hobor, Philippa Gardner, Jules Villard
    Under submission, June 2016

Making Smart Contracts Smarter
    Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, Aquinas Hobor
    Under submission, May 2016

Constructing Hereditary Worlds Within Worlds
    Robert Dockins, Aquinas Hobor
    Under submission, June 2013.

Unreviewed

The Ramifications of Sharing in Data Structures (extended version)
    Aquinas Hobor, Jules Villard
    Technical Report, 2012.
    Associated with the POPL13 paper with a similar name.

Improving the Compositionality of Separation Algebras
    Aquinas Hobor
    2011
    1 citation

Lecture notes on formal induction and Hoare logic
    Aquinas Hobor, 2010

A Theory of Termination via Indirection
    Robert Dockins, Aquinas Hobor
    Modelling, Controlling and Reasoning About State, Dagstuhl Seminar
    10341 Proceedings, 2010.

Oracle Semantics for Concurrent Separation Logic (Extended Version)
    Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli
    Princeton Univ., Department of Computer Science, June 2008, TR-825-08.
    2 citations

Aggregate Citation Information

Total Citations: 450; h-index: 10. Citation counts from Google Scholar, July 18, 2016.  Total includes 10 citations for Mechanized Semantic Library, below.

All my publications are available for download from my website at:
    http://www.comp.nus.edu.sg/~hobor/Publications/publications.html

Invited Talks

Oracle Semantics
    University of Paris VII, Paris, France, 2007
    University of Saarland, Saarbrucken, Germany, 2008
    Microsoft Research Cambridge, Cambridge, UK, 2008
    National University of Singapore, Singapore, 2008
    Microsoft Research India, Bangalore, India, 2008
    Microsoft Research Redmond, Redmond, USA, 2008

A Theory of Indirection via Approximation
    Queen Mary, University of London, UK, 2009
    University of Cambridge, Cambridge, UK, 2009

Barriers in Concurrent Separation Logic
    Microsoft Research India, Bangalore, India, 2010

A Theory of Termination via Indirection
    Microsoft Research India, Bangalore, India, 2010
    Dagstuhl 10341: Modelling, Controlling and Reasoning About State, 2010
    Queen Mary, University of London, London, UK, 2011

Developing and Mechanizing Semantic Models for Program Logics
 
  with Robert Dockins
    The 8th Asian Symposium on Programming Languages and Systems (APLAS
    2010), Shanghai, China, November/December 2010

Mechanized Semantic Library
    IT University of Copenhagen, Copenhagen, Denmark, 2011

The Ramifications of Sharing in Data Structures
    with Jules Villard
    Imperial College London, London, UK, 2012
    Microsoft Research Cambridge, Cambridge, UK, 2012
    Furthermore, Jules Villard has independently presented this work at:
      High Confidence Software and Systems, Annapolis, Maryland, USA, 2012
      Yale University, New Haven, Connecticut, USA, 2012
      Princeton University, Princeton, New Jersey, USA, 2012
      Wessex Theory Seminar, Queen Mary, London, UK, 2012

Software and Projects

Bare-Bones Verified Compiler
    A simple Coq-certified compiler developed for my students in CS 6282.
    http://www.comp.nus.edu.sg/~hobor/BBComp/
    Aquinas Hobor

Coq Soundness Proof for Barrier Logic
    Coq sources associated with my ESOP 2011 publication Barriers in
    Concurrent Separation Logic.
    http://www.comp.nus.edu.sg/~hobor/
barrier/
    Aquinas Hobor, Cristian Gherghina

HIP/SLEEK Barrier Verifier
    Prototype extension of HIP/SLEEK toolchain to verify concurrent programs
    with barriers as explained in my journal publication Barriers in Concurrent
    Separation Logic: Now With Tool Support!
    http://www.comp.nus.edu.sg/~cristian/projects/barriers/tool.html
    Cristian Gherghina, Aquinas Hobor

(10 citations) Mechanized Semantic Library
    Large collection of Coq-mechanized semantic techniques to aid
    development and mechanization of higher-order program logics.
    http://msl.cs.princeton.edu/
    Andrew W. Appel, Robert Dockins, Aquinas Hobor

Prototype Decision Procedure Over Sophisticated Fractional Permissions
    Prototype of our decision procedures.
    http://www.comp.nus.edu.sg/~cristian/projects/prover/
    Cristian Gherghina, Aquinas Hobor, Le Xuan Bach

Verified Software Toolchain
    Connecting machine-verified software analyzers to machine-verified
    compilers.
    http://vst.cs.princeton.edu/
    Andrew W. Appel et al.

VisualizeSLE
    Developing a visual editor for separation logic entailments.
    http://www.comp.nus.edu.sg/~hobor/vsl/

    Aquinas Hobor, Soe Lin Myat, Bimlesh Wadhwa

Academic Service

3rd Workshop on Bitcoin and Blockchain Research (BITCOIN 16)
    Program Committee
    http://fc16.ifca.ai/bitcoin/

13th Asian Symposium on Programming Languages and Systems (APLAS 2015)
    Program Committee
    http://pl.postech.ac.kr/aplas2015/

The 3rd International Conference on Certified Programs and Proofs (CPP 2013)
    Program Committee
    http://cpp2013.forge.nicta.com.au

The 2nd ACM SIGPLAN Workshop on Higher-Order Programming with Effects (HOPE 2013)

    Program committee
    http://hope2013.mpi-sws.org/

10th Asian Symposium on Programming Languages and Systems (APLAS 2012)

    Program committee
    http://aplas12.kuis.kyoto-u.ac.jp/

Formal Techniques for Java-like Programs (FTfJP 2012)

    Co-Chair (with Chin Wei Ngan)
    http://www.comp.nus.edu.sg/~ftfjp/

Teaching

Fundamentals of Programming
    Introduction to Algorithms and Data Structures
    Yale-NUS College
    Spring 2016, Spring 2015


Integrated Science 2/3
    Introduction to Computer Science in an integrated context (Core course)
    Yale-NUS College
    Fall 2015, Fall 2014


Quantitative Reasoning (YNC 1122)
    Innumeracy, Visualization, Biases, Logic, Probability, and Statistics
    (Core course)
    Yale-NUS College
    Spring 2014

Logic and Formal Systems
(CS 3234)
Foundation in Logic & AI (CS 5209)
    Introduction to formal methods in computer science, primarily covering
    propositional, predicate, modal, and Hoare logics.  This course is given
    in two similar versions: undergraduate (CS3234) and graduate (CS5209).

    I have been adding a substantial lab-based component to this course using
    the Coq theorem prover.  Please see my CPP 2011 paper (with Martin Henz)
    and my lecture notes on formal induction and Hoare logic.
    National University of Singapore

    CS3234, Spring 2016
    CS3234, Spring 2015
    CS3234, Spring 2014
    CS3234, Spring 2013 (with Chin Wei Ngan)
    CS3234, Spring 2012 (with Chin Wei Ngan)
    CS3234, Fall 2010 (with Martin Henz)
    CS5209, Spring 2010 (with Martin Henz)
    CS3234, Fall 2009 (with Martin Henz)
    CS5209, Spring 2009 (with P.S. Thiagarajan)

Parallel and Distributed Computing (CS 4231)
    Algorithms, Data Structures, and Formal Methods for Parallel Programming.
    National University of Singapore
    Spring 2013

Data Structures and Algorithms I (CS 1020)
    Introductory programming course using Java.
    National University of Singapore
    Spring 2012 (with Tan Sun Teck, Ling Tok Wang, and Tan Tuck Choy Aaron)

Topics in Computer Science III (CS 6282)
    Readings and research in formal methods.  Course projects included a
    verified bare-bones compiler, a concurrent separation logic for barriers,
    an investigation of alternate semantic encodes of higher-order Hoare
    tuples, and an investigation of alternate fractional share models.

    National University of Singapore
    Spring 2010

Students

PhD advisees

Shengyi Wang (PhD Candidate, Spring 2014-Present)
 
  The Ramifications of Mechanized Localizations within Data Structures
    (July 2016)
    Certified Reasoning with Infinity
    (FM 2015)

Le Xuan Bach
(PhD Candidate, Spring 2013-Present)
    Decidability and Complexity of Tree Share Formulas
    (July 2016)
    A Certified Decision Procedure for Sophisticated Fractional Permissions
    (June 2016)

Undergraduates/Masters/Non-advised PhDs

John Reid (Capstone*, Fall 2016-Spring 2017)
    In progress 

Anshuman Mohan (Capstone*, Fall 2016-Spring 2017)
    In progress
 
Leow Wei Xiang
(FYP*, Fall 2016-Spring 2017)
    In progress

Qinxiang Cao
(Intern, Summer 2015)
    The Ramifications of Mechanized Localizations within Data Structures
    (July 2016)

Jieqi Tong
(UROP*, Fall 2013-Spring 2014)
    Parallel algorithms in Haskell

Soe Lin Myat
(Fall 2012-Spring 2013)
    VisualizeSLE

Chris Chak (UROP*, Fall 2012-Spring 2013)
    Use of self-modifying code to build automata.

Le Xuan Bach (FYP*, Spring 2011-Fall 2011)
    Decision Procedures over Fractional Share Models for Separation Logic
    Later published as part of our APLAS 2012 paper Decision Procedures over
    Sophisticated Fractional Permissions.

Le Xuan Bach (UROP*, Spring 2010-Fall 2010)
    Mechanical Soundness Proof of Separation Logic in Sequential Language
    and Concurrent Language


Cristian Gherghina (CS 6282*, Spring 2010)
    Student project became our ESOP 2011 paper Barriers in Concurrent
    Separation Logic (and we subsequently collaborated on its associated
    journal version Barriers in Concurrent Separation Logic: Now With Tool
    Support!
)

*  UROP: Undergraduate Research Opportunity Project
    FYP: Final Year Project
    Capstone: Yale-NUS College final year project
    CS 6282: Topics in  Computer Science III (Reading & Research Course)

Grants

Program Verification for Concurrency, Compilers, and Self-Modifying Code
    Aquinas Hobor
    LKY PDF Grant,
August 2009, #T1 251RES0902
    National University of Singapore
    SGD 67,800 (about USD 55,600, at 0.82 USD to 1 SGD)

Citizenship

United States of America

web site by Lucy Day Hobor ~ 2008-2015