L. A. Dennis: CV

Name: Louise Dennis
Nationality: British
email: lad@csc.liv.ac.uk
Address:
Department of Computer Science
Room 117
Ashton Building
University of Liverpool
United Kingdom

Summary

I'm currently working as a Post-Doctoral Researcher in the Logic and Computation group at the University of Liverpool. I am an investigator on an EPSRC funded platform grant (The Integration and Interaction of Multiple Mathematical Reasoning Processes) held at the University of Edinburgh. I have a PhD in Artificial Intelligence and an MSc in Knowledge Based Systems.

My background is in artificial intelligence and more specifically in automated reasoning. Over the years I have worked primarily on the development of automated reasoning and theorem proving tools, most notably the lambda-clam proof planning system and the PROSPER Toolkit for integrating an interactive theorem prover (HOL) with automated reasoning tools (such as SAT solvers) and Case/CAD tools.

I am Secretary (and webmaster) of the Society for the Study of Artificial Intelligence and the Simulation of Behaviour. I am also on the organising committee of the Automated Reasoning Workshop and will be chair of the 2006 Automated Reasoning Workshop.

Qualifications

PGCHE (completed 2005)
Postgraduate Certificate in Higher Education. University of Nottingham. Group Project: Automated Assessment for Large Groups, Individual Project: Student Attitudes to Plagiarism and Collusion in Computer Science, Teaching Portfolio available online at http://www.csc.liv.ac.uk/~lad/portfolio.
PhD (1994 - 1998)
Department of Artificial Intelligence, Edinburgh University, Proof Planning Coinduction. Supervisors: Prof. Alan Bundy, Dr. Ian Green.
MSc Knowledge Based Systems (1993-1994)
Department of Artificial Intelligence, University of Edinburgh, An Exploration of Sematic Resolution.
BA Hons (2:1) (1989-1992)
Mathematics and Philosophy, Oxford University.

Career

2006-2009
Department of Computer Science, University of Liverpool.
Research Associate on Model Checking Agent Programming Languages
2001-2006
School of Computer Science and Information Technology, University of Nottingham.
Lecturer.
2000-2001
Division of Informatics, University of Edinburgh.
Research Fellow on EPSRC grant GR/M45030, The Computational Modelling of Mathematical Reasoning.
1998-1999
Department of Computing Science, University of Glasgow.
Research Associate on PROSPER (Proof and Specification assisted Design Environments). ESPRIT Framework IV LTR 26241.
1997-1998
Department of Computer Science, University of Nottingham.
Teaching Assistant.
1993
European Molecular Biology Laboratory (EMBL), Heidelberg.
6 month Research Assistant/Traineeship in Biocomputing.

Research

Publications

Refereed Journal Papers

Louise A. Dennis, Michael Fisher, Matthew P. Webster and Rafael H. Bordini. Model checking agent programming languages}, Automated Software Engineering, http://dx.doi.org/10.1007/s10515-011-0088-x, 2011.

L. A. Dennis, I. Green and A. Smaill, The Use of Embeddings to Provide a Clean Separation of Term and Annotation for Higher Order Rippling. Journal of Automated Reasoning: Volume 47, Issue 1 (2011), 57-105.

W. I. Sellers, L. A. Dennis, W.-J. Wang and R. H. Crompton, Evaluating alternative gait strategies using evolutionary robotics, Journal of Anatomy, 204, pp. 343-351, 2004.

W. I. Sellers, L. A. Dennis and R. H. Crompton, Predicting the metabolic energy costs of bipedalism using evolutionary robotics, Journal of Experimental Biology, 206, 1127-1136, 2003.

L. A. Dennis, G. Collins, M. Norrish, R. Boulton, K. Slind and T. Melham, The PROSPER Toolkit. Int J Software Tools for Technology Transfer, 4(2), pp. 189-210, 2003.

L. A. Dennis, A. Bundy, and I. Green, The Productive Use of Failure to Generate Witnesses From Divergent Proof Attempts for Coinduction. Annals of Mathematics and Artificial Intelligence 29:99-138, 2000.

J. A. Dennis and L. A. Dennis, Neutron dose effect relationships at low doses. Radiation and Environmental Biophysics, 27:91-101, 1988.

Conference Proceedings - refereed

Louise A. Dennis, Michael Fisher, Nicholas K. Lincoln, Alexei Lisitsa, and Sandor M. Veres. Declarative Abstractions for Agent Based Hybrid Control Systems. Proceedings of Declarative Agent Languages and Technologies (DALT 10), 2010.

Louise A. Dennis, Michael Fisher, Nicholas K. Lincoln, Alexei Lisitsa, and Sandor M. Veres. Reducing Code Complexity in Hybrid Autonomous Control Systems. The 10th International Symposium on Artificial Intelligence, Robotics and Automation in Space (iSAIRAS 2010).

Louise A. Dennis, Michael Fisher, Nicholas Lincoln, Alexei Lisitsa, Sandor M. Veres. Agent Based Approaches to Engineering Autonomous Space Software. Proceedings FM-09 Workshop on Formal Methods for Aerospace, Eindhoven, 3rd November 2009 pp. 63-68. EPTCS 20, The Computing Research Repository.

L. A. Dennis, N. Tinnemeier and J.-J. Meyer. Model Checking Normative Agent Organisations. Proceedings 10th Workshop on Computational Logic in Multi-Agent Systems (CLIMA-X), 2009. Jürgen Dix, Michael Fisher and Peter Novák (eds), pp. 64-82. LNCS 6214. Springer.

Nicholas Lincoln , Sandor Veres , Louise Dennis , Michael Fisher and Alexei Lisitsa. An Agent Based Framework for Adaptive Control and Decision Making of Autonomous Vehicles. Adaptation and Learning in Control and Signal Processing (ALCOSP 2010), 2010.

R. H. Bordini, L. A. Dennis, B. Farwer and M. Fisher. Automated Verification of Multi-Agent Programs. Proceedings of Automated Software Engineering (ASE 2008), 2008. IEEE.

L. A. Dennis, B. Farwer, R. H. Bordini and M. Fisher. A Flexible Framework for Verifying Agent Programs (Short Paper). Proceedings of the 7th International Conference on Autonomous Agents and Multi-agent Systems (AAMAS 2008), Padgham, Parkes, Müller and Parsons (eds.), May, 12-16., 2008, Estoril, Portugal, pp. 1303-1306.

L. A. Dennis and M. Fisher. Programming Verifiable Heterogeneous Agent Systems. Programming Multi-Agent Sstems (ProMAS08). K. Hindriks, A. Pokahr and S. Sardina (eds.), 2008. pp. 27-42.

L. A. Dennis and B. Farwer. Gwendolen: A BDI Language for Verifiable Agents. Logic and the Simulation of Interaction and Reasoning. B. Löwe (ed). AISB'08 Workshop, Aberdeen, 2008.

A. Hepple, L. A. Dennis and M. Fisher. A Common Basis for Agent Organisation in BDI Languages. Languages, methodologies and Development tools for Multi-Agent Systems (LADS'007), 2007. Lecture Notes in Artificial Intelligence, 5118.

L. A. Dennis, M. Fisher and A. Hepple. Foundations of Flexible Multi-Agent Programming. Eighth Workshop on Computational Logic in Multi-Agent Systems (CLIMA-VIII), 2007.

B. Farwer and L. Dennis. Translating into an intermediate agent layer: A prototype in Maude. Proceedings of Concurrency, Specification and Programming CS&P'2007, Lagow, Poland, 2007.

L. A. Dennis, R. H. Bordini, B. Farwer, M. Fisher and M. Wooldridge. A Common Semantic Basis for BDI Languages. Fifth International Workshop on Programming in Multi-Agent Systems (ProMAS'07). 2008. Lecture Notes in Artificial Intelligence 4908.

L. A. Dennis, Enhancing Theorem Prover Interfaces with Program Slice Information. User Interaces for Theorem Provers 2006, Seattle, Washington, 2006. Workshop associated with IJCAR 2006. Published in Electronic Notes in Computer Science, Volume 174, Issue 2, 2007.

L. A. Dennis, Program Slicing and Middle-Out Reasoning for Error Location and Repair. IJCAR 2006 workshop on Disproving: Non-Theorems, Non-Validity and Non-Provability, Seattle, Washington, 2006.

L. A. Dennis, M. Jamnik and M. Pollet. On the Comparison of Proof Planning Systems: Lambda-Clam, Omega and IsaPlanner. 12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus 2005), Electronic Notes in Computer Science (ENTCS) 151. pp. 93-110, 2006.

L. A. Dennis, An Architecture for Proof Planning Systems, in L. P. Kaelbling and A. Saffoitti (Eds): Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, IJCAI-05, IJCAI, Inc. pp. 1558-1559, 2005.

L. A. Dennis, The Use of Proof Planning Critics to Diagnose Errors in the Base Cases of Recursive Programs, in W. Ahrendt and P. Baumgartner and H. de Nivelle (Eds): IJCAR 2004 Workshop on Disproving: Non-Theorems, Non-Validity, Non-Provability. pp. 47-58. 2004.

L. A. Dennis, Student attitudes to plagiarism and collusion within computer science, in A. P. Smith and F. Duggan (Eds): Plagiarism: Prevention, Practice and Policy Conference 2004. Northumbria University Press, 2005. pp. 57-64.BibTex

A. A. Adams and L. A. Dennis, Rippling in PVS, in M. Archer, B. Di Vito and C. Munoz (Eds.): Proceedings of Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), Rome, Italy, September 8, 2003. pp. 84 - 91. Published as NASA Technical Report CP-2003-212448.

L. A. Dennis and A. Bundy, A Comparison of two Proof Critics: Power vs. Robustness, in V. A Carreno, C. A. Munoz, S. Tahar (Eds.): Proceedings of Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002. pp 182-198. Volume 2410 in the LNCS series by Springer-Verlag. BibTex

J. Zimmer and L. A. Dennis, Inductive Theorem Proving and Computer Algebra in the Mathweb Software Bus in J. Calmet, B. Belaid, O. Caprotti, L. Henocque and V. Sorge (Eds.): Artificial Intelligence, Automated Reasoning and Symbolic Computation (Calculemus 02), Marseille, France, 2002. pp. 319-331. Volume 2385 in the LNAI series by Springer-Verlag. BibTex

S. Colton and L. Dennis, The NumbersWithNames Program. AI&M 3-2002, Seventh International Symposium on Artificial Intelligence and Mathematics, January 2-4, 2002, Fort Lauderdale, Florida. Available from http://rutcor.rutgers.edu/~amai/aimath02/. BibTex

L. A. Dennis and A. Smaill, Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain. R. J. Boulton and P. B. Jackson (eds). 14th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2001. pp. 185-200 LNCS 2152.

G. Collins and L. A. Dennis, System Description: Embedding Verification into Microsoft Excel. Proceeedings of CADE17, pp. 497-501. LNAI 1831. Springer-Verlag. Springer-Verlag own the copyright to this paper.

L. A. Dennis, G. Collins, M. Norrish, R. Boulton, K. Slind, G. Robinson, M. Gordon, and T. Melham, The PROSPER Toolkit. Proceedings of TACAS 2000, pp. 78-92. LNCS 1785, Springer-Verlag. Springer-Verlag own the copyright to the paper.

L. A. Dennis, A. Bundy, and I. Green, Using a Generalisation Critic to find Bisimulations for Coinductive Proofs. Proceedings CADE-14, 1997, pp 276-290. Also available as Edinburgh DAI Research Report, 834.

Chapters (Sections) in book

R. H. Bordini, L. A. Dennis, B. Farwer and M. Fisher, Directions for Agent Model Checking. Chapter 4 in M. Dastani, K. V. Hindriks, J.-J. C. Meyer (eds), Specification and Verification of Multi-agent Systems, pp. 103-123. Springer US, 2010. BibTex

T. D. Attfield, M. C. Duarte, L. Li, H.-Y. Mak, A. N. Neal, L. M. Toft, Z. Wang and L. A. Dennis, Induction Challenge OMDoc Manager (ICOM). Chapter 26 Applications and Projects, Section 11 in M. Kohlhase, OMDoc - An Open Markup Format for Mathematical Documents [version 1.2], Lecture Notes in Artificial Intelligence 4180, AI Systems Sub-Series. Springer, 2006. BibTex

Conference Proceedings - not refereed

L. A. Dennis, R. Monroy and P. Nogueira. Proof-directed Debugging and Repair in H. Nilsson and M. van Eekelen (eds). Seventh Symposium on Trends in Functional Programming, pp. 131-140. 2006.

L. A. Dennis and P. Nogueira. What can be Learned from Failed Proofs of Non-Theorems? in J. Hurd, E. Smith and A. Darbari (eds). Theorem Proving in Higher Order Logics (TPHOLs 2005): Emerging Trends Proceedings, pp. 45-58. Technical Report PRG-RP-05-2, Oxford University Computer Laboratory, 2005.

A. Stevenson and L. A. Dennis, Integrating SVC and HOL with the PROSPER Toolkit. TPHOLs2000, Supplemental Proceedings, pp. 199-206. OGI Technical Report CSE 00-009.

Others

Louise Dennis, Michael Fisher, Alexei Lisitsa, Nicholas Lincoln, Sandor Veres. Satellite Control Using Rational Agent Programming. IEEE Intelligent Systems 25 (3), pp. 92-97, IEEE Computer Society, 2010.

M. Webster, L. Dennis and M. Fisher. Model Checking Auctions, Coalitions and Trust. Technical Report ULCS-09-004, University of Liverpool, Department of Computer Science. 2009. Available from http://www.csc.liv.ac.uk/research/techreports/.

M. Fisher, L. Dennis and A. Hepple. Modular Multi-Agent Design. Technical Report ULCS-09-002, University of Liverpool, Department of Computer Science. 2009. Available from http://www.csc.liv.ac.uk/research/techreports/.

L. A. Dennis, J. Gow and C. Schurmann. Challenge Problems for Inductive Theorem Provers v1.0. Technical Report ULCS-07-004, University of Liverpool, Department of Computer Science. 2007. Available from http://www.csc.liv.ac.uk/research/techreports/.

L. A. Dennis, I. Green and A. Smaill, Embeddings as a Higher-Order Representation of Annotations for Rippling, Computer Science Technical Report No. NOTTCS-WP-2005-1, University of Nottingham. 2005. Under revision for the Journal of Automated Reasoning.

J. Richardson, L. A. Dennis, J. Gow and M. Jackson. User/Programmer Manual for the LambdaClam Proof planner, v. 2.0.0. Publicly available (with software) from the Lambda-CLam Home Page.

L. A. Dennis, G. Collins and M. Norrish, The PROSPER Toolkit, Deliverable D3.5, PROSPER project. Publicly available (with software) from the PROSPER web site.

L. A. Dennis and T. Melham, PROSPER Technology Roadmap, Deliverable D6.4, Prosper project. Publically available from the PROSPER web site.

L. A. Dennis Proof Planning Coinduction. Unpublished PhD thesis. Department of Artificial Intelligence, University of Edinburgh. 1999.

L. A. Dennis, An Exploration of Semantic Resolution. Unpublished MSc thesis, Department of Artificial Intelligence, University of Edinburgh. 1994.

Grants

Nottingham New Lecturers' Fund Grant NLF - 3051
Classifying programming Errors and how they cause Correctness Proofs to Fail.
EPSRC Platform Grant Gr/SO1771/01
The Integration and Interaction of Multiple Mathematical Reasoning Processes. This grant is held in Edinburgh with Prof. Alan Bundy as the principal investigator.
EPSRC Grant Gr/M45030
The Computational Modelling of Mathematical Reasoning. This grant was held in Edinburgh with Prof. Alan Bundy as the principal investigator.

Teaching Experience

Lecturing

2003 - , Mathematics for Computer Science 2
A first year module covering discrete mathematics. The work involved adapting the existing lectures, setting and marking exercises and examinations.
2002 - , Software Methods and Tools
A first year module in UNIX, perl and a tool-based approach to Software Engineering. The work involved adapting the existing lectures, setting and marking practicals and examinations.
2002, Mechanised Reasoning and Theorem Proving
A Short course for the Midland Graduate School in Theoretical Computer Science.
2002, An Introduction to UNIX
A One day course for IT workers from Peurgeot
2002, Developments in Digital Business
A third year module aimed primarily at students on the Digitial Business degree course. This module was offered for the first time in 2002 and so I created the module from scratch based on a small syllabus description. Half the module consisted of guest lectures given by people working in Digital Business. The other half consisted of a series of lectures by myself on current topics in Digital Business. I also created and marked the course works and exam.
1999, Advanced Artificial Intelligence.
A third year module. I inherited this course in a form that had not been revised for several years. The work involved substantial revision of the existing material, the addition of new material, setting and marking coursework and the exam and co-oridinating the visit of a guest lecturer from Caen via the ERASMUS scheme.

Supervision

PhD Students

Matthew Walton, Programming Languages for Proof Planning Systems (2005-2006)
University of Nottingham. Supervision handed over when I moved.
Graham Steel, Non-theorem Refutation and Cryptographic Security Protocols (Graduated 2004).
University of Edinburgh, second supervisor.

MSc Students

Fiona McNeill, On the Use of Dependency Tracking in Theorem Proving, 2000.
University of Edinburgh, second supervisor.

Selected Final Year Undergraduates

Thomas Attfield, Improving OMDoc Manager, 2002-2003
University of Nottingham
Richard Everett, A Route Finding System for Europe, 2002-2003
University of Nottingham
Sirisha Gollapudi and Stuart Lewis, A Patient Database for the Paediatric Hospital in Sarajevo, Bosnia, 2002 - 2003
University of Nottingham
Jasdeep Kalsi, Packaging a Remote Distance E-Learning Resource for the For-Profit University
University of Nottingham
C. Robey, An Expert System for the Production of Athletics Training Schedules, 2002 - 2003
University of Nottingham
D. Gill, The "Cognitive Dimensions" framework is capable of evaluating the usability of an online store and provides results consistent or equal to those of more traditional HCI approaches., 2001-2002
University of Nottingham
P. Mills, An AI Implementation of the Game of Go, 2002
University of Nottingham, transfered from previous supervisor
R. Speight, London Underground Route Finder for Wireless Devices, 2001-2002
University of Nottingham
S. van Beelarts von Blokland, Electric Model Elimination, 1999-00.
University of Edinburgh, second supervisor.
A. Stevenson, An SVC Plugin for HOL, 1999-00.
Glasgow University, second supervisor. Led to publication.
K. R. Kanagasabai, A Children's Tutoring System, 1997-98.
Nottingham University.

Second Year Group Projects

Whitebox, 2004-2005.
Nottingham University.
Foraging Agents, 2002-2003.
Nottingham University.
An Example of Distributed Computing, Happy@Home, 2002-2003
Nottingham University.
An OMDOC Entry system, 2001-2002.
Nottingham University.
Logic Tutor, 1997-98.
Nottingham University, A FOL proof checker
Computer Salesman, 1997-98.
Nottingham University, An Expert System for Computer Configuration
Philosophiza, 1997-98.
Nottingham University, An Eliza based Philosopher

Pastoral Care

At Nottingham I am personal tutor for a group of students in each year of study. This involves writing references, advising on module choice and liaising between the department, the disabilities officer and counsellors.

Formal Training

I have a Postgraduate Certificate in Higher Education (PGCHE). For this I had to produce a Teaching Portfolio.

Competence

Conferences, Workshops, Invited Talks and Visits (not covered in publications)

University of Birmingham 2002,Planning the Whisky Problem
Invited talk
University of Liverpool 2002, Planning the Whisky Problem
Invited talk
Reading University 2002, Proof Planning and the lambdaCLAM System
Invited talk.
University of Liverpool 2001, Using a Generalisation Critic to find Bisimulations for Coinductive Proof
Invited talk.
Glasgow Caledonian 2000, Embedding Verification into Microsoft Excel
Invited talk on the PROSPER project, focusing in particular on a case study embedding verification into Microsoft Excel.
CADE-17 Workshop on the Automation of Proof by Mathematical Induction, Panel on Proof Planning.
Saarbrücken. June 2000.
Week-long visit to the OMEGA group at Saarbrücken, including a presentation on the lambda-clam proof planning system.
CIAO (Clam-INKA-OMRS).
Attended this annual workshop on proof planning and related topics since 1993 and have presented work at every one since 1994 (except 2003).
Automated Reasoning Workshop.
I regularly attend this British based workshop and presented a poster at the 1999 workshop.
Glasgow 1997. Proof Planning Coinduction
Invited talk on my PhD work, presented to the Glasgow Formal Methods Group Seminar series.

Membership of Professional Organisations

The British Computer Society
The Society for the Study of Artificial Intelligence and the Simulation of Behaviour
Association for Automated Reasoning
British Logic Colloquium

Administrative Experience

2006
Automated Reasoning Workshop Organiser
2006 -
Member of the Automated Reasoning Workshop Organising Committee
2005 - 2006
Course Organiser Computer Science with Artificial Intelligence
2005 - 2006
Course Organiser Computer Science with Formal Methods
2005
University of Nottingham. Committee member on two committees which designed three new degrees to be offered by the School and redesigned the curriculum of the existing single honours Computer Science degree.
2005 - 2006
Head of Marketing Undergraduate Degrees, School of Computer Science and IT, University of Nottingham
2005 - 2006
Admissions Officer, School of Computer Science and IT, University of Nottingham
2005
CIAO Workshop Chair
2004 -
Secretary and Webmaster of the Society for the the Study of Artificial Intelligence and the Simulation of Behaviour
2003 -
AISB Quarterly Newsletter, Member of the Editorial Board
2001 -
Society for the Study of Artificial Intelligence and the Simulation of Behaviour, Committee Member
2001 - 2006
Nottingham Teaching Committee Member
2001 - 2005
Course Organiser for GN51 Joint Honours Computer Science and Management Studies.
International Conference on Theorem Proving in Higher-Order Logic 2001
Local Arrangements Chair
Banff 2000 Workshop in Honour of Graham Birtwhistle, Ullapool Scotland.
Assisted with planning and organisation.
PROSPER Review Meeting 1999
Assisted with planning and organisation. In particular the coordination of the production of volumes of deliverables and booking accommodation.
Member of the Implementation, Empirical and Web Taskforces in the MRG, 2000 - 2001.
The Implementation Taskforce is in charge of the development of LambdaClam. The Empirical taskforce maps out strategies for case studies, new areas of study and benchmark suites. The Web Taskforce coordinated the presentation and content of the research groups' web pages.
Refereeing papers.
I have reviewed papers both for journals and conferences.
Summers 1990 - 1992
Academic Assistant at Open University Mathematics Summer Schools. General administrative duties and some teaching.
Formal Training
I have attended a CRAC management training course.

External Recognition

Louise Dennis
Last modified: Tue Jun 7 13:24:07 BST 2011