Aquinas Hobor: Teaching

Current

Programming Methodology (CS 1010S)
  Spring 2021

Previous courses

Introduction to Computer Science (YSC 1212)
  Fall 2020, Fall 2019 (2 sections), Fall 2018, Spring 2018, Fall 2016

Introduction to Python (YSC 2221)
  Fall 2020 (2 sections)

Data Structures and Algorithms (CS 2040)
  Summer 2020

Advanced Topics in Software Engineering (CS 6880)
  Fall 2018

Fundamentals of Programming (YSC 2204)
  Spring 2016, Spring 2015

Logic and Formal Systems (CS 3234)
  Spring 2014, Spring 2015, Spring 2016, Spring 2017, Spring 2018
  Spring 2013 (with Razvan Voicu)
  Spring 2012 (with Chin Wei Ngan)
  Fall 2010, Fall 2009 (with Martin Henz)

Machine-checked Proof (YIR 2311)

  Fall 2014

Integrated Science 2 (YCC 2133)
  Fall 2015, Fall 2014

Quantitative Reasoning (YCC 1122)
  Spring 2014 (with Christopher Asplund, Jon Berrick et al.)

Parallel and Distributed Computing (CS 4231)
 
Spring 2013

Data Structures and Algorithms I (CS 1020)
  Spring 2012 (with Tan Sun Teck, Ling Tok Wang, and Tan Tuck Choy Aaron)

Foundations in Logic & AI (CS 5209)
  CS5209, Spring 2010 (with Martin Henz)
  CS5209, Spring 2009 (with P. S. Thiagarajan)

Topics in Computer Science III (CS 6282)
  Spring 2010

Students and Employees

PhD advisees

Wei Xiang Leow (PhD Candidate, 2020-present)
    Functional Correctness of C Implementations of Dijkstra's, Kruskal's, and
    Prim's Algorithms (under submission)

Tamer AbdElaziz
(PhD Candidate, 2019-present)

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

Le Xuan Bach
(2013-2017; next position: postdoc at Oxford)
  PhD thesis: Disjoint Fractional Permissions In Verification: Applications,
    Systems, and Theory
  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)
  Decision Procedures over Sophisticated Fractional Permissions (APLAS 2012)

RAs

Anshuman Mohan (2017-2020; next position: PhD student at Cornell)
  Functional Correctness of C Implementations of Dijkstra's, Kruskal's, and
    Prim's Algorithms (under submission)
  Machine-Checked C Implementation of Dijkstra (APLAS 2019 poster)
  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 student at Yale mathematics)
  A Functional Proof Pearl: Inverting the Ackermann Hierarchy (CPP 2020)

Undergraduates/Masters/Non-supervised PhDs

How Si Wei (UROP, Fall 2018-Spring 2019)
  Formalization of real analysis of one variable

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

Andrew Wooten (Capstone, Fall 2018-Spring 2019)
  Nested Splay Trees 

Anshuman Mohan (Capstone, Fall 2016-Spring 2017)
  Certification of a Garbage Collector for a Purely Functional Language
  Later grew into part of our OOPSLA 2019 paper Certifying Graph-Manipulating
 
C Programs via Localizations within Data Structures

Leow Wei Xiang (FYP, Fall 2016-Spring 2017)
  Formalization of set theory in Coq

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

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

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, Fall 2011-Spring 2012)
  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)
  Barriers in Concurrent Separation Logic (and we subsequently collaborated
  on its associated journal version Barriers in Concurrent Separation Logic:
  Now With Tool Support!)

Teaching-related Publications

Teaching Experience: Logic and Formal Methods with Coq (PDF, PPT, BIB)
Martin Henz, Aquinas Hobor
1st International Conference on Certified Programs and Proofs (CPP 2011), pp. 199-215, December 2011.
See also the following lecture notes and some additional course material here.

Lecture notes on formal induction (PDF) and Hoare logic (PDF)
Aquinas Hobor
2010
Lecture notes from when I co-taught CS3234 with Martin Henz.  This material may be developed into a book.  Additional material from that course may be found here.  See also the associated conference paper.

web site design by Lucy Day - 2008–2021