Aquinas Hobor: Teaching
Current
Introduction to Computer Science (YSC 1212)
Fall 2018
Previous courses
Introduction to Computer Science (YSC 1212)
Spring 2018, Fall 2016
Fundamentals of Programming (YNC
2204),
Sprint 2016, Spring 2015
Logic and Formal Systems (CS 3234), Foundations in
Logic & AI (CS 5209)
CS3234, Spring 2018
CS3234, Spring 2017
CS3234, Spring 2016
CS3234, Spring 2015
CS3234, Spring 2014
CS3234, Spring 2013 (with Razvan Voicu)
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)
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)
Topics in Computer Science III (CS 6282)
Spring 2010
Students
PhD advisees
Shengyi Wang (Spring 2014-Present)
BesFS: Mechanized Proof of an
Iago-Safe Filesystem for Enclaves
The Ramifications of
Mechanized Localizations within Data Structures
Certified Reasoning with Infinity
Le Xuan Bach (Spring 2013-November 2017)
PhD thesis: Disjoint Fractional Permissions In
Verification: Applications,
Systems, and Theory
Complexity Analysis of Tree
Share Operations
Logical Reasoning for Disjoint Permissions
A Certified Decision Procedure for Tree Shares
Decidability and Complexity of Tree Share Formulas
A Certified Decision Procedure for Sophisticated
Fractional Permissions
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)
Temporal logic for smart contracts
Andrew Wooten (Capstone, Fall 2018-Spring
2019)
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
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.