Aquinas Hobor: Teaching


Previous courses

Fundamentals of Programming,
  Sprint 2016, Spring 2015

Logic and Formal Systems (CS 3234), Foundations in Logic & AI (CS5209)

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


PhD advisees

Shengyi Wang (Spring 2014-Present)
  The Ramifications of Mechanized Localizations within Data Structures
  Certified Reasoning with Infinity

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

Undergraduates/Masters/Non-supervised 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

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

Soe Lin Myat (Fall 2012-Spring 2013)

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
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 by Lucy Day Hobor ~ 2008-2015