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