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

Google Scholar
   
https://scholar.google.com/citations?user=-SbM8VcAAAAJ&hl=en

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

 

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.

Invited Publications

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.

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.

Thesis

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

Refereed Conference Publications

Functional Correctness of C Implementations of Dijkstra's, Kruskal's, and Prim's Algorithms
    Anshuman Mohan, Wei Xiang Leow, Aquinas Hobor
    33rd International Conference in Computer Aided Verification (CAV 2021),
     to appear, July 2021.

BesFS: A POSIX Filesystem for Enclaves with a Mechanized Safety Proof
   
Shweta Shinde, Shengyi Wang, Pinghai Yuan, Aquinas Hobor,
    Abhik Roychoudhury, Prateek Saxena
    20th USENIX Security Symposium (USENIX Security 2020), pp. 523-540,
    August 2020.

Reasoning over Permissions Regions in Concurrent Separation Logic
   
James Brotherston, Diana Costa, Aquinas Hobor, John Wickerson
    32nd International Conference in Computer Aided Verification (CAV 2020),
    pp. 203-224, July 2020.

A Functional Proof Pearl: Inverting the Ackermann Hierarchy
    Linh Tran, Anshuman Mohan, Aquinas Hobor
    9th ACM-SIGPLAN International Conference on Certified Programs and
    Proofs (CPP 2020), pp. 129-142, January 2020.

Pumping, With or Without Choice
   
Aquinas Hobor, Elaine Li, Frank Stephan
    17th Asian Symposium on Programming Languages and Systems
    (APLAS 2019), pp. 427-446, December 2019.

Certifying Graph-Manipulating C Programs via Localizations within Data Structures
   
Shengyi Wang, Qinxiang Cao, Anshuman Mohan, Aquinas Hobor
    PACMPL (OOPSLA 2019), pp. 171:1-171:30, October 2019.

Exploiting the Laws of Order in Smart Contracts
   
Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Aquinas Hobor, Prateek Saxena
   
28th International Symposium of Software Testing and Analysis
    (ISSTA 2019), pp. 363-373, July 2019.

Finding the Greedy, Prodigal, and Suicidal Contracts at Scale
    Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek Saxena, Aquinas Hobor
    34th Annual Computer Security Applications Conference (ACSAC 2018),
    pp. 653-663, December 2018.

Complexity Analysis of Tree Share Structure
    Xuan Bach Le, Aquinas Hobor, Anthony W. Lin
    16th Asian Symposium on Programming Languages and Systems
    (APLAS 2018), pp. 89-108, December 2018.

Temporal Properties of Smart Contracts
    Ilya Sergey, Amrit Kumar, Aquinas Hobor
    8th International Symposium On Leveraging Applications of Formal
    Methods, Verification and Validation (ISoLA 2018), pp. 323-338,
    November 2018, and 4th Workshop on New Ideas and Emerging Results
    (NIER'18), December 2018.

Logical Reasoning for Disjoint Permissions
    Xuan Bach Le, Aquinas Hobor
    27th European Symposium of Programming (ESOP 2018), pp. 385-414,
    April 2018.


A Certified Decision Procedure for Tree Shares
    Xuan Bach Le, Thanh Toan Nguyen, Wei Ngan Chin, Aquinas Hobor
    19th International Conference on Formal Engineering Methods
    (ICFEM 2017), pp. 226-242, November 2017
.

Decidability and Complexity of Tree Share Formulas
    Xuan Bach Le, Aquinas Hobor, Anthony W. Lin
    36th IARCS Annual Conference on Foundations of Software Technology and
    Theoretical Computer Science (FSTTCS 2016), pp. 19:1-19:14,
    December 2016.

Verifying Concurrent Graph Algorithms
    Azalea Raad, Aquinas Hobor, Philippa Gardner, Jules Villard
    14th Asian Symposium on Programming Languages and Systems
    (APLAS 2016), pp. 314-334, November 2016.

Making Smart Contracts Smarter
    Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, Aquinas Hobor
    23rd ACM Conference on Computer and Communications Security
    (CCS 2016), pp. 254-269, October 2016.

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.

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.

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.

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.

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

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


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.

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.

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.

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.


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.

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.

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.

Refereed Workshop Publications

Machine-Checked C Implementation of Dijkstra
    Anshuman Mohan, Aquinas Hobor
    Poster session of The 17th Asian Symposium on Programming Languages
    and Systems (APLAS 2019), December 2019.

A Verified Garbage Collector for Gallina

    Shengyi Wang, Anshuman Mohan, Qinxiang Cao, Aquinas Hobor
    5th Workshop on New Ideas and Emerging Results in Programming
    Languages and Systems (NIER'19), December 2019.

Mechanized Verification of Graph-Manipulating Programs

    Shengyi Wang, Qinxiang Cao, Aquinas Hobor
    Poster session of The 15th Asian Symposium on Programming Languages
    and Systems (APLAS 2017), November 2017.

A Concurrent Perspective on Smart Contracts

    Ilya Sergey, Aquinas Hobor
    First Workshop on Trusted Smart Contracts (WTSC 2017), April 2017.

Decidability and Complexity of Tree Share Formulas
    Le Xuan Bach, Aquinas Hobor, Anthony W. Lin
    Poster session of The 14th Asian Symposium on Programming Languages
    and Systems (APLAS 2016), November 2016.

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.

Under Submission

A Partition Resilient Overlay Network via Blockchain
    Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Aquinas Hobor, Prateek Saxena
    Under submission, 2021

Magic Wand as Frame
    Qinxiang Cao, Shengyi Wang, Aquinas Hobor, Andrew W. Appel
    Under submission, 2019

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

Unreviewed

BesFS: Mechanized Proof of an Iago-Safe Filesystem for Enclaves
    Shweta Shinde, Shengyi Wang, Pinghai Yuan, Aquinas Hobor,
    Abhik Roychoudhury, Prateek Saxena
    arXiv:1807.00477, July 2018.

Finding the Greedy, Prodigal, and Suicidal Contracts at Scale
    Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek Saxena, Aquinas Hobor
    arXiv:1802.06038v2, March 2018.
    Associated with the ACSAC 2018 paper of the same name.

SCILLA: a Smart Contract Intermediate-Level LAnguage
    Ilya Sergey, Amrit Kumar, Aquinas Hobor
    arXiv:1801.00687v1, January 2018.

On Power Splitting Games in Distributed Computation: The Case of Bitcoin Pooled Mining
    Loi Luu, Ratul Saha, Inian Parameshwaran, Prateek Saxena, Aquinas Hobor
    Associated with the CSF15 paper with the same name.

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

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.

Invited Talks

A Functional Proof Pearl: Inverting the Ackermann Hierarchy
    University College London, July 2019

Formal Methods in Software Development
    10th National Workshop on Recent Trends in Software Testing (RTST17),
    July 2017, Keynote

Disjoint Semirings for Fractional Permissions
    The Aarhus Concurrency Workshop on Concurrency Theory, May 2017
    Cambridge University, June 2017

Mechanized Verification for Graph Algorithms
    6th South of England Regional Programming Language Seminar (S-REPLS 6),
    May 2017

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

Grants

CRYSTAL Centre
    Co-PI, 2019-2021
    SGD 50,000 / year (about USD 108,000, at 0.72 USD to 1 SGD)

Verification of a Garbage Collector, Graph-Manipulating Programs and
    Cryptocurrency
    Aquinas Hobor
    June 2017, #IG16-LR103
    SGD 162,000 (about USD 120,000, at 0.74 USD to 1 SGD)

Semantic Models, Program Logics, and Tools for Verification
    Aquinas Hobor
   
September 2013
    SGD 60,000 (about USD 46,800, at 0.78 USD to 1 SGD)

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

Software and Projects

ShareInfer
    Inference tool associated with my ESOP 2018 publication Logical
    Reasoning for Disjoint Permissions.
 
   Le Xuan Bach, Aquinas Hobor

Coq Soundness Proof for Disjoint Permission Logic
    Coq sources associated with my ESOP 2018 publication Logical Reasoning
    for Disjoint Permissions.
 
   Le Xuan Bach, Aquinas Hobor

Certified Share Solver
    Coq sources associated with my ICFEM 2017 publication A Certified
    Decision Procedure for Tree Shares.
 
   Le Xuan Bach, Thanh Toan Nguyen, Wei Ngan Chin, Aquinas Hobor

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

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

20th Asian Symposium on Programming Languages and Systems (APLAS 2022)
    Program Committee

4th Workshop on Blockchain and Smart Contract Technologies (BSCT 2020)
    Program Committee

31st European Symposium on Programming (ESOP 2022)
    Program Committee

25th ACM SIGPLAN International Conference on Functional Programming (ICFP 2020)
    Moderator
    https://icfp20.sigplan.org/

3rd Workshop on Blockchain and Smart Contract Technologies (BSCT 2020)
    Program Committee
    https://bisconf.org/2020/bsct/

17th Asian Symposium on Programming Languages and Systems (APLAS 2019)
    Program Committee
    https://aplas2019.cs.ui.ac.id/

2nd Workshop on Blockchain and Smart Contract Technologies (BSCT 2019)
    Program Committee
    http://bis.ue.poznan.pl/bis2019/bsct/

8th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2019)
    Program Committee
    https://popl19.sigplan.org/track/CPP-2019

16th Asian Symposium on Programming Languages and Systems (APLAS 2018)
    Program Committee
    http://aplas2018.org/

1st IEEE Workshop on Blockchain Technologies and Applications (BTA 2018)
    Program Committee
    https://sites.google.com/view/bta18/

5th Workshop on Bitcoin and Blockchain Research (BITCOIN 2018)
    Program Committee
    https://fc18.ifca.ai/bitcoin/cfp.html

3rd Workshop on Bitcoin and Blockchain Research (BITCOIN 2016)
    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/

Commercial Service

Flamemaster Corporation
    Board of Directors
    A manufacturer of specialty sealants, adhesives, and coatings primarily
    serving the aerospace industry

Zilliqa Research
    Board of Directors
    Cryptocurrency developer

Teaching

Programming Methodology (CS 1010S)
    Introduction to programming with Python
    School of Computing
    Spring 2021

Introduction to Computer Science (YSC 1212)
    Introduction to algorithmic thinking and programming in OCaml
    Yale-NUS College
    Fall 2020, Fall 2019 (2 sections), Fall 2018, Spring 2018, Fall 2016

Introduction to Python (YSC 2221)
    Half-semester course teaching Python
    Yale-NUS College
    Fall 2020 (2 sections)

Data Structures and Algorithms (CS 2040)
    Introduction to data structures and algorithms in Java
    School of Computing
    Summer 2020

Advanced Topics in Software Engineering (CS 6880)
    Foundations of certified software
    School of Computing
    Fall 2018

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 added 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 2018, Spring 2017, Spring 2016, Spring 2015, Spring 2014
    CS3234, Spring 2013, Spring 2012 (with Chin Wei Ngan)
    CS3234, Fall 2010, Fall 2009 (with Martin Henz)
    CS5209, Spring 2010 (with Martin Henz)
    CS5209, Spring 2009 (with P.S. Thiagarajan)

Fundamentals of Programming (YSC 2204)
    Introduction to Algorithms and Data Structures in OCaml
    Yale-NUS College
    Spring 2016, Spring 2015


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


Machine-checked Proof (YIR 2311)
    Propositional and predicate logic in the Coq proof assistant
    Fall 2014

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

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

Tamer AbdElaziz (PhD Candidate, 2019-present)

Wei Xiang Leow
(PhD Candidate, 2020-2021)
    Functional Correctness of C Implementations of Dijkstra's, Kruskal's, and
    Prim's Algorithms (CAV 2021, to appear)

Shengyi Wang
(PhD, 2014-2020; next position: postdoc at Princeton)
    Mechanized Verification of Graph-Manipulating Programs (PhD thesis)
    BesFS: A POSIX Filesystem for Enclaves with a Mechanized Safety Proof
    (USENIX Security 2020)
    Certifying Graph-Manipulating C Programs via Localizations within Data
    Structures (OOPSLA 2019)
    Certified Reasoning with Infinity (FM 2015)

Le Xuan Bach
(PhD, 2013-2017; next position: postdoc at Oxford)
    Disjoint Fractional Permissions in Verification: Applications, Systems and
    Theory (PhD thesis)
    Complexity Analysis of Tree Share Operations (APLAS 2018)
    Logical Reasoning for Disjoint Permissions (ESOP 2018)
    A Certified Decision Procedure for Tree Shares (ICFEM 2017)
    Decidability and Complexity of Tree Share Formulas (FSTTCS 2016)

Research Assistants (RAs)

Anshuman Mohan (2017-2020; next position: PhD Candidate at Cornell)
    Functional Correctness of C Implementations of Dijkstra's, Kruskal's, and
    Prim's Algorithms (CAV 2021, to appear)
    A Functional Proof Pearl: Inverting the Ackermann Hierarchy (CPP 2020)
    Certifying Graph-Manipulating C Programs via Localizations within Data
    Structures (OOPSLA 2019)

Linh Tran
(2019; next position: PhD Candidate at Yale mathematics)
    A Functional Proof Pearl: Inverting the Ackermann Hierarchy (CPP 2020)

Undergraduates/Masters/Non-advised PhDs

Andrew Wooten (Capstone*, Fall 2018-Spring 2019)
    Analysis of Splay Trees

Elaine Fang Li (Capstone*, Fall 2018-Spring 2019)
    Formalizing Block Pumpable Language Theory
    Later published as part of our APLAS 2019 paper Pumping, with or Without
    Choice

How Si Wei
(UROP*, Fall 2018-Spring 2019)
    Formalization of Real Analysis

Anshuman Mohan
(Capstone*, Fall 2016-Spring 2017)
    Certification of a Garbage Collector for a Purely Functional Language
 
Leow Wei Xiang
(FYP*, Fall 2016-Spring 2017)
    Formalization of Set Theory in Coq

Hrishi Olickel
(Fall 2015-Spring 2016)
    Making Smart Contracts Smarter (CCS 2016)


Qinxiang Cao
(Intern, Summer 2015)
    Certifying Graph-Manipulating C Programs via Localizations within Data
    Structures (OOPSLA 2019)

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 Decision Procedures over Sophisticated Fractional
    Permissions (APLAS 2012).

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

Ali Razeen (CS CS 6282*, Spring 2010)



Cristian Gherghina (CS 6282*, Spring 2010)
    Later published as part of Barriers in Concurrent Separation Logic (ESOP
    2011) and we subsequently collaborated on its associated
    journal version Barriers in Concurrent Separation Logic: Now With Tool
    Support!)

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

Citizenship

United States of America

web site design by Lucy Day - 2008–2021