Hasan Amjad

CURRENT ADDRESS
University of Cambridge Computer Laboratory
15 JJ Thomson Avenue
Cambridge CB3 0FD
United Kingdom
Tel.: +44 (01223) 763602
e-mail : ha227 at cam dot ac dot uk

DATE OF BIRTH 25th January, 1975

NATIONALITY British & Pakistani

EMPLOYMENT

Nov. 2008 to date Analyst, Cantab Capital Partners LLP, Cambridge, UK
Aug. 2007 to date Visiting Fellow, Computer Laboratory, University of Cambridge, UK
Aug. 2007 to Nov 2008 Research Associate, School of Computing, Middlesex University, UK
Oct. 2003 to Jul. 2007 Research Assistant/Associate, Computer Laboratory, University of Cambridge, UK
June 2001 to Aug. 2001 Summer Intern, Compaq Cambridge Research Labs, USA
Nov.1999 to Aug. 2000 3D Graphics Developer, Align Technology Inc., Pakistan


ADMINISTRATIVE

2008 PC member, Theorem Proving in Higher Order Logics (TPHOLs)
2007- Member, SMT-LIB working group on proof format standardisation


EDUCATION

Oct. 2000 to Sep. 2004 Ph.D. Computer Science
  Automated Reasoning Group, Computer Laboratory, University of Cambridge, UK
Oct. 1998 to Oct. 1999 M.Sc. Mathematics and the Foundations of Computer Science
  Mathematical Institute, University of Oxford, UK
Aug. 1994 to May 1997 B.Sc. (Hons.) Computer Science
  Dept. of Computer Science, Lahore University of Management Sciences, Pakistan

AWARDS

2003 Trinity College (Cambridge) Graduate Studentship
2000 Trinity College (Cambridge) External Research Studentship (3 years)
  Overseas Research Scholar Award (3 years)
  Commonwealth Scholarship (Honorary)
  Commonwealth Fellow
  Merton College (Oxford) Harmsworth-Domus Graduate Scholarship (Declined)
1999 Worcester College (Oxford) Cash Prize for Academic Performance
  Distinction in M.Sc. MFOCS programme (Oxford University, top candidate)
1996 Dean's Honours List

RESEARCH

Oct. 2004 to date Integration of SAT/SMT solvers and interactive theorem provers; propositional proof compression; analysis of concurrent heap-manipulating programs.
Oct. 2000 to Sep. 2004 For Ph.D., developed a self-verifying model checker in the HOL theorem prover. This work was supervised by Professor M. J. C. Gordon FRS.
Oct. 1998 to Sept. 1999 For M.Sc., constructed a categorical model of classical linear logic using Hoare's CSP. This work was supervised by Dr. C-H. L. Ong.

TEACHING

Oct. 2004 to date Research Assistant/Associate
  Computer Laboratory, University of Cambridge, UK
  In addition to supervisions, acted as moderator for second-year Discrete Maths problem solving seminars ( 15 students per session).
  Taught Theory and Semantics Mini-Course titled Formal Verification Techniques.
Oct. 2000 to Sep. 2004 Research Student
  Computer Laboratory, University of Cambridge, UK
  Conducted undergraduate supervisions for the following courses: Concurrency, Natural Language Processing, Denotational Semantics, Theory of Computation and Quantum Computing.
July 1997 to July 1998 Teaching Assistant in Computer Science
  Lahore University of Management Sciences, Pakistan
  Conducted undergraduate tutorials for the following courses: Calculus, Statistics, Probability, Operations Research, Automata, Complexity Theory and Compilers (50-100 students per tutorial). Also helped set and mark exams for these courses.

Hasan 2008-11-06