Louise Dennis: Publications

2017

Louise Dennis, Elisa Cucco and Michael Fisher. A General Architecture for Flexible Autonomous Systems. Workshop on Architectures for Generality and Autonomy (AGA 2017), 2017. BibTex

Elisa Cucco, Michael Fisher, Louise Dennis, Clare Dixon, Matt Webster, Bastian Broecker, Richard Williams, Joe Collenette, Katie Atkinson and Karl Tuyls. Towards Robots for Social Engagement. Workshop on Human-Robot Engagement in the Home, Workplace and Public Spaces (WHRE 2017), 2017. BibTex

Maryam Kamali, Louise A. Dennis, Owen McAree, Michael Fisher and Sandor M. Veres. Formal verification of autonomous vehicle platooning. Science of Computer Programming, 2017 (in press). DOI: 10.1016/j.scico.2017.05.006. Pre-print available at ArXiv pre-prints 1602.01718, 2016. BibTex

Vicky Charisi, Louise Dennis, Michael Fisher, Robert Lieck, Andreas Matthias, Marija Slavkovik, Janina Sombetzki, Alan F. T. Winfield, Roman Yampolskiy. Towards Autonomous Moral Systems. ArXiv e-prints, 1703.04741, 2017. BibTex

Louise A. Dennis. Gwendolen Semantics: 2017. University of Liverpool, Computer Science, Technical Report ULCS-17-001. BibTex

2016

Louise A. Dennis, Marija Slavkovik and Michael Fisher. "How Did They Know?" - Model-Checking for Analysis of Information Leakage in Social Networks. Coordination, Organizations, Institutions and Norms in Agent Systems XII. 2016. LNAI 10315, pages 42-59. BibTex

Louise A. Dennis, Jonathan M. Aitken, Joe Collenette, Elisa Cucco, Maryam Kamali, Owen McAree, Affan Shaukat, Katie Atkinson, Yang Gao, Sandor Veres, and Michael Fisher. Agent-based Autonomous Systems and Abstraction Engines: Theory meets Practice. Towards Autonomous Robotic Systems, 17th Annual Conference (TAROS 2016), 2016. Springer LNCS 9716, pages 75-86. BibTex.

Louise A. Dennis, Michael Fisher, Nicholas K. Lincoln, Alexei Lisitsa, Sandor M. Veres. Practical Verification of Decision-Making in Agent-Based Autonomous Systems (available Open Access). Automated Software Engineering 23(3), 305-359, 2016. DOI: 10.1007/s10515-014-0168-9. PDF. The results mentioned in the paper can be reproduced using this Virtual Machine archived at recomputation.org. BibTex.

2015

Louise A. Dennis, Michael Fisher, Marija Slavkovik, and Matt Webster. Formal Verification of Ethical Choices in Autonomous Systems Robotics and Autonomous Systems. DOI:10.1016/j.robot.2015.11.012. BibTex

M. Birna van Riemsdijk, Louise A. Dennis, Michael Fisher, Koen V. Hindriks. A Semantic Framework for Socially Adaptive Agents: Towards strong norm compliance. AAMAS 2015: 423-432 BibTex

Marija Slavkovik, Louise A. Dennis, and Michael Fisher. An Abstract Formal Basis for Digital Crowds. Distributed and Parallel Databases. DOI: 10.1007/s10619-014-7161-y. BibTex

Louise A. Dennis, Michael Fisher, and Matt Webster. Two-stage agent program verification. Journal of Logic and Computation. Published online February 16, 2015. DOI: 10.1093/logcom/exv002. BibTex. This is an extension of Using Agent JPF to Build Models for Other Model Checkers. BibTex

Louise A. Dennis, Michael Fisher, and Alan Winfield. Towards Verifiably Ethical Robot Behaviour. Proceedings of the AAAI Workshop on Artificial Intelligence and Ethics (1st International Workshop on AI and Ethics). BibTex

2014

Louise A. Dennis. ROS-AIL Integration. University of Liverpool, Computer Science, Technical Report ULCS-14-004. BibTex

Louise Dennis, Michael Fisher, Sandor Veres and Nick Lincoln. Safe Autonomous Space Software. Space Safety Magazine. February 2014.

Louise A. Dennis and Michael Fisher. Actions with Durations and Failures in BDI Languages. Proceedings of the 21st European Conference on Artificial Intelligence (ECAI 2014), Frontiers in Artificial Intelligence and Applications, volume 263, pp.995-996. IOS Press. A longer version appears as University of Liverpool, Computer Science Technical Report ULCS-14-003. BibTex (ECAI Paper). BibTex (Tecnical Report)

Louise A. Dennis, Michael Fisher, Jonathan M. Aitken, Sandor M. Veres, Yang Gao, Affan Shaukat, Guy Burroughes. Reconfigurable Autonomy. Künstliche Intelligenz (2014) 28:199–207. BibTex

2013

Matteo Baldoni, Louise A. Dennis, Viviana Mascardi and Wamberto Vasconcelos (eds), Declarative Agent Languages and Technologies X, 10th International Workshop, DALT 2012, Valencia, Spain, June 4, 2012, Revised Selected and Invited Papers, LNCS Volume 7784, 2013, DOI: 10.1007/978-3-642-37890-4.

Michael Fisher, Louise A. Dennis, Matthew P. Webster. Verifying Autonomous Systems. Communications of the ACM 56(9): 85-93 (2013). BibTex

M. Birna van Riemsdijk, Louise A. Dennis, Michael Fisher, Koen V. Hindriks. Agent Reasoning for Norm Compliance: A Semantic Approach. AAMAS 2013: 499-506. BibTex

Louise A. Dennis, Michael Fisher, Matthew P. Webster. Using Agent JPF to Build Models for Other Model Checkers.. Computational Logic in Multi-Agent Systems: 14th International Workshop, CLIMA XIV, Corunna, Spain, September 16-18, 2013, Proceedings: 273-289. Springer LNCS 8143. This is now superseded by Two-stage agent program verification. BibTex

Louise Dennis, Michael Fisher, Marija Slavkovik, Matt Webster. Ethical Choice in Unforeseen Circumstances. Towards Autonomous Robotic Systems, 14th Annual Conference (TAROS 2013), 2013. Springer LNCS 8069, pp. 433-445. BibTeX

Richard Stocker, Maarten Sierhuis, Louise Dennis, Clare Dixon, Michael Fisher. A Formal Semantics for Brahms. ULCS Technical Report ULCS-13-006

N. K. Lincoln, S. M. Veres, L. A. Dennis, M. Fisher and A. Lisitsa. Autonomous Asteroid Exploration by Rational Agents. Computational Intelligence Magazine, 8(4), pp. 25 - 38. IEEE, 2013. BibTeX

2012

Louise A. Dennis, Olivier Boissier and Rafael H. Bordini (eds), Programming Multi-Agent Systems: 9th International Workshop, ProMAS 2011, Taipei, Taiwan, May 3, 2011, Revised Selected Papers, LNCS Volume 7217, 2012, DOI: 10.1007/978-3-642-31915-0.

Richard Stocker, Louise A. Dennis, Clare Dixon and Michael Fisher. Verifying Brahms Human-Robot Teamwork Models. Logics in Artificial Intelligence - 13th European Conference, JELIA 2012, Toulouse, France, September 26-28, 2012. pp. 385-397. BibTex

2011

Louise A. Dennis, Michael Fisher, Matthew P. Webster and Rafael H. Bordini. Model checking agent programming languages, Automated Software Engineering, 2011. BibTex

Richard Stocker, Maarten Sierhuis, Louise. A. Dennis, Clare Dixon, Michael Fisher. A Formal Semantics for Brahms. Computational Logic in Multi-Agent Systems - 12th International Workshop, CLIMA XII, Barcelona, Spain, July 17-18, 2011. pp. 259-274. BibTex

L. A. Dennis. Plan-indexing for State-Based Plans. Proceedings of Declarative Agent Languages and Technologies (DALT 11), 2011. Springer LNCS 7169. pp 3-15. BibTex

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), Page 57-105. BibTex

2010

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

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

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

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

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. Springer LNAI 6619. pp 96-111. BibTex

2009

Myrto Arapinis, Muffy Calder, Louise A. Dennis, Michael Fisher, Philip D. Gray, Savas Konor, Alice Miller, Eike Ritter, Mark Ryan, Sven Schewe, Chris Unsworth, Rehana Yasmin. Towards the Verification of Pervasive Systems. ECEASST 22 (2009). BibTex

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

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

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

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

2008

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

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

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

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

2007

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, pp. 71-88. BibTex

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

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

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

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

2006

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

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

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

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

2005

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

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

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

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

2004

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

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

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

2003

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

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

2002

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. LNCS 2410. Springer. 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. LNAI 2385. Springer. 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

2001

L. A. Dennis and A. Smaill, Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domainin 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. BibTeX

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

2000

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

G. Collins and L. A. Dennis, System Description: Embedding Verification into Microsoft Excelin D. McAllester (Ed.): Proceedings of 17th International COnference on Automated Deduction, CADE-17, pp. 497-501. LNAI 1831. Springer. BibTeX.

L. A. Dennis, G. Collins, M. Norrish, R. Boulton, K. Slind, G. Robinson, M. Gordon, and T. Melham, The PROSPER Toolkit in S. Graf and M. Schwartzback (Eds.): Proceedings of Tools and Algorithms for the Construction and Analysis of Systems, 6th International Conference, TACAS 2000, pp. 78-92. LNCS 1785, Springer-Verlag. Springer-Verlag own the copyright to the paper. BibTeX.

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

1999

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

1997

L. A. Dennis, A. Bundy, and I. Green, Using a Generalisation Critic to find Bisimulations for Coinductive Proofs. in W. McCune (Ed.): Proceedings of 14th International Conference on Automated Deduction, CADE-14, 1997, pp 276-290. Also available as Edinburgh DAI Research Report, 834. 1997. BibTeX.

1994

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