Aquinas Hobor: Curriculum Vitae

(Also available as a PDF or as a Word document.)

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
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
Dean’s Scholarship
1999, Rensselaer Polytechnic Institute

Employment

National University of Singapore, Singapore
    Fall 2011 – present 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

Jackson Software, Glencoe, Illinois
    Summer 1996 Testing software for teachers

Publications

A Specification Logic for Termination Reasoning
    Ton-Chanh Le, Cristian Gherghina, Aquinas Hobor, Wei-Ngan Chin
    Under submission, 2012.

Barriers in Concurrent Separation Logic: Now with Tool Support!
    Aquinas Hobor, Cristian Gherghina
    Under submission, 2011.

Verifying Time Bounds for General Function Pointers
    Robert Dockins, Aquinas Hobor
    Under submission, 2011.

Improving the Compositionality of Separation Algebras
    Aquinas Hobor
    2011

Introducing Logic and Formal Methods with Coq
    Martin Henz, Aquinas Hobor
    1st International Conference on Certified Programs and Proofs (CPP 2011),
    199-215, 2011.

Barriers in Concurrent Separation Logic
    Aquinas Hobor, Cristian Gherghina
    20th European Symposium of Programming (ESOP 2008), pp. 276-296,
    April 2011.

Lecture notes on formal induction and Hoare logic
    Aquinas Hobor, 2010

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.

A Theory of Termination via Indirection
    Robert Dockins, Aquinas Hobor
    Modelling, Controlling and Reasoning About State, Dagstuhl Seminar
    10341 Proceedings, 2010.

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
    Aquinas Hobor
    Ph.D. Thesis, Princeton University, Department of Computer Science,
    October 2008 (TR-836-08).

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.

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.

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.

Oracle Semantics for Concurrent Separation Logic
    Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli
    17th European Symposium of Programming (ESOP 2008), pp. 353-367.

Professional Services

Formal Techniques for Java-like Programs (FTfJP) 2012
Co-Chair (with Chin Wei Ngan)

Teaching

Data Structures and Algorithms I (CS 1020)
    Introductory undergraduate course using Java
    Co-taught with Tan Sun Teck, Ling Tok Wang, and Tan Tuck Choy Aaron
    Spring 2012, National University of Singapore

Logic and Formal Systems (CS 3234)
    Introductory undergraduate course in formal methods
    Co-taught with Chin Wei Ngan
    Spring 2012, National University of Singapore

Logic and Formal Systems (CS 3234)
    Introductory undergraduate course in formal methods
    Co-taught with Martin Henz
    Fall 2010, National University of Singapore

Topics in Computer Science III (CS 6282)
    Readings and research in formal methods
    Spring 2010, National University of Singapore

Foundation in Logic & AI (CS 5209)
    Introductory graduate course in formal logic (no AI covered)
    Co-taught with Martin Henz
    Spring 2010, National University of Singapore

Logic and Formal Systems (CS 3234)
    Introductory undergraduate course in formal methods
    Co-taught with Martin Henz
    Fall 2009, National University of Singapore

Foundation in Logic & AI (CS 5209)
    Introductory graduate course in formal logic (no AI covered)
    Co-taught with P.S. Thiagarajan
    Spring 2009, National University of Singapore

Grants

Program Verification for Concurrency, Compilers, and Self-Modifying Code
    Aquinas Hobor
    LKY PDF Grant, August 2009, #T1 251RES0902
    National University of Singapore

References

Available on request