Jia Meng
Personal Information
| Work Address | RSISE, Building 115, The Australian National University, Canberra, ACT 0200, Australia |
| Date of Birth | November 1979 |
| Nationality | Chinese |
| Marital Status | Single |
| Tel | +61 (2)6125 1768 |
| jia.meng at anu.edu.au |
Education
| 2002 - 2005 | Computer Laboratory, University of Cambridge, Churchill College Ph.D. in Computational Logic: The Integration of Higher Order Interactive Proof with First Order Automatic Theorem Proving |
| 1999 - 2002 | New Hall College, University of Cambridge First Class B.A. Hons Degree in Computer Science |
| 1997 - 1999 | Cambridge Tutors College, Croydon, U.K. A-Levels: Mathematics A, Physics A, Economics A |
Achievements and Prizes
| 2002 - 2005 | Awarded Scholarships from Computer Laboratory, University of Cambridge and Cambridge Overseas Trust for reading Ph.D. |
| 2002 | First Class (4th ranked in University) in CST PartII exams. |
| 2002 | New Hall Scholarship in recognition of excellent tripos result. |
| 2001 | First Class (1st ranked in University) in CST PartIB exams. |
| 2001 | Awarded Addison Wesley Prize (also known as Pearson Education Prize) for excellence in Computer Science. |
| 2001 | New Hall Scholarship in recognition of excellent tripos result. |
| 2000 | Achieved First Class in CST PartIA exams. |
| 2000 | New Hall Scholarship in recognition of excellent tripos result. |
| 1999 | MacCarthy Award for excellent A-Level exams results from Cambridge Tutors College. |
| 1997 - 1999 | Full Scholarship from Cambridge Tutors College for reading A-Levels. |
Research Interests
Interested in all areas of formal methods, including building theorem provers and using formal verification to design systems, hardware and protocols etc.
Also interested in programming language principles (semantics, types etc.) and artificial intelligence.
Work Experience
Logic and Computation Program,
National ICT Australia 22/8/2005 - present
Researcher.
Autonomy plc.2/9/2002 - 26/9/2002
Cambridge Business Park, Cowley Road, Cambridge CB4 0WZ
Summer intern as a software engineer.
Micromuse Ltd. 20/6/2001 - 14/8/2001
Disraeli House, 90 Putney Bridge Road, London SW18 1DA
Summer intern on web design.
Teaching Experience
| 2002 - 2005 | Supervisor for Computer Science students at the University of Cambridge for the courses: Logic and Proof, Numerical Analysis 1, Semantics of Programming Languages, Artificial Intelligence 1, Foundations of Functional Programming, Specification and Verification 1, Types. |
Language Skill
Mandarin as first language.
Fluent in both English and Cantonese.
Basic French (received CULP certificate from Cambridge University Language Centre).
Publications
1. Jia Meng. Integration of Interactive and Automatic Provers. In Manuel Carro and Jesus Correas (editors), Second CologNet Workshop on Implementation Technology for Computational Logic Systems, FME2003, September 2003.
2. Jia Meng and Lawrence C. Paulson. Experiments On Supporting Interactive Proof Using Resolution.In: David Basin and Michaël Rusinowitch (editors), IJCAR 2004: Second International Joint Conference on Automated Reasoning (Springer LNCS, 2004), 372-384.
3. Jia Meng, Claire Quigley and Lawrence C. Paulson. Automation for Interactive Proof: First Prototype. Information and Computation 204 10 (2006), 1575-1596.
4. Hans de Nivelle and Jia Meng. Geometric Resolution: A Proof Procedure Based on Finite Model Search. In U. Furbach and N. Shankar (editors), IJCAR 2006: Third International Joint Conference on Automated Reasoning (Springer LNAI, Vol 4130, 2006), 303-317.
5. Jia Meng and Lawrence C. Paulson. Lightweight Relevance Filtering for Machine-Generated Resolution Problems. In: Geoff Sutcliffe, Renate Schmidt and Stephan Schulz (editors), ESCoR: Empirically Successful Computerized Reasoning (CEUR Workshop Proceedings, Vol. 192, 2006), 53-69.
6. Jia Meng and Lawrence C. Paulson. Translating Higher-Order Problems to First-Order Clauses. In: Geoff Sutcliffe, Renate Schmidt and Stephan Schulz (editors), ESCoR: Empirically Successful Computerized Reasoning (CEUR Workshop Proceedings, Vol. 192, 2006), 70-80.
7. Jia Meng and Lawrence C. Paulson. Lightweight Relevance Filtering for Machine-Generated Resolution Problems. Journal of Applied Logic, in press.
8. Jia Meng, Lawrence C. Paulson and Gerwin Klein. A Termination Checker for Isabelle Hoare Logic. In: Bernhard Beckert (editor), 4th International Verification Workshop, VERIFY'07 (CEUR Workshop Proceedings, Vol. 259, 2007), 104-118.
9. Jia Meng and Lawrence C. Paulson. Translating higher-order problems to first-order clauses. Journal of Automated Reasoning, in press.
Referees
| Prof. Lawrence C. Paulson Computer Laboratory JJ Thomson Avenue Cambridge CB3 0FD U.K. Larry.Paulson at cl.cam.ac.uk |
Prof. Michael J. C. Gordon Computer Laboratory JJ Thomson Avenue Cambridge CB3 0FD U.K. Mike.Gordon at cl.cam.ac.uk |
Prof. Jean M. Bacon Computer Laboratory JJ Thomson Avenue Cambridge CB3 0FD U.K. Jean.Bacon at cl.cam.ac.uk |