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