Dennis BibTeX References




@article{dennis_see_2020,
	Abstract = {Considering the popular framing of an artificial intelligence as a rational agent that always seeks to maximise its expected utility, referred to as its goal, one of the features attributed to such rational agents is that they will never select an action which will change their goal. Therefore, if such an agent is to be friendly towards humanity, one argument goes, we must understand how to specify this friendliness in terms of a utility function. Wolfhart Totschnig (Fully Autonomous AI, Science and Engineering Ethics, 2020), argues in contrast that a fully autonomous agent will have the ability to change its utility function and will do so guided by its values. This commentary examines computational accounts of goals, values and decision-making. It rejects the idea that a rational agent will never select an action that changes its goal but also argues that an artificial intelligence is unlikely to be purely rational in terms of always acting to maximise a utility function. It nevertheless also challenges the idea that an agent which does not change its goal cannot be considered fully autonomous. It does agree that values are an important component of decision-making and explores a number of reasons why.},
	Author = {Dennis, Louise A. },
	Da = {2020/08/04},
	Date-Added = {2020-08-06 13:39:55 +0100},
	Date-Modified = {2020-08-06 13:39:55 +0100},
	Doi = {10.1007/s11948-020-00244-y},
	Id = {Dennis2020},
	Isbn = {1471-5546},
	Journal = {Science and Engineering Ethics},
	Title = {Computational Goals, Values and Decision-Making},
	Ty = {JOUR},
	Url = {https://doi.org/10.1007/s11948-020-00244-y},
	Year = {2020},
	Bdsk-Url-1 = {https://doi.org/10.1007/s11948-020-00244-y}}

      
      

      @misc{cardoso_ime,
      author = {Rafael C. Cardoso aand Daniel Ene and Tom Evans and Louise A. Dennis},
      title = {Ethical Governor Systems viewed as a Multi-Agent Problem},
  editor       = {Vivek Nallur},
  booktitle        = {Second Workshop on Implementing Machine Ethics},
  month        = jun,
  year         = 2020,
  publisher    = {Zenodo},
  doi          = {10.5281/zenodo.3938851},
  url          = {https://doi.org/10.5281/zenodo.3938851}
}


           

      @misc{alves_ime,
      author = {Gleifer Vaz Alves and Louise Dennis and Michael Fisher},
      title = {First Steps towards an Ethical Agent for checking decision and behaviour for an Autonomous Vehicle on the Rules of the Road},
  editor       = {Vivek Nallur},
  booktitle        = {Second Workshop on Implementing Machine Ethics},
  month        = jun,
  year         = 2020,
  publisher    = {Zenodo},
  doi          = {10.5281/zenodo.3938851},
  url          = {https://doi.org/10.5281/zenodo.3938851}
}


      
      @inproceedings{Stringer20,
      author="Peter W. Stringer and Rafael C. Cardoso and Xiaowei Huang and Louise A. Dennis",
      title="Verifiable and Adapatble BDI Reasoning",
      booktitle="Agents and Robots for reliable Engineered Autonomy (AREA)",
      year=2020}

      

@article{dennis_ieee20,
author={Louise A. Dennis and Michael Fisher},
title ={Verifiable Self-Aware Agent-Based Autonomous Systems},
journal={Proceedings of the IEEE special issue on Self-Aware Autonomous Systems},
doi="10.1109/JPROC.2020.2991262",
pages={1--16},
year=2020}



      @incproceedings{Cardoso20,
      author="Rafael C. Cardoso and Angelo Ferrando and Louise A. Dennis and Michael Fisher",
      title="An Interface for Programming Verifiable Autonomous Agents in ROS",
      booktitle="17th European Conference on Multi-Agent Systems (EUMAS 2020)",
      year=2020
      }

            
      @incproceedings{Dennis20,
      author="Louise A. Dennis and Marija Slavkovik",
      title="Model-checking Information Diffusion in Social Networks with PRISM",
      booktitle="17th European Conference on Multi-Agent Systems (EUMAS 2020)",
      year=2020
      }

      
      
      @inproceedings{Webster20,
      author="Matt Webster and Louise A. Dennis and Clare Dixon and Michael Fisher and Richard Stocker and Maarten Sierhuis.",
      title="Formal Verification of Astronaut-Rover Teams for Planetary Surface Operations.",
      booktitle="IEEE Aerospace Conference (AeroConf) 2020.",
      year=2020
      }
      
      
      @Inbook{Alves2020,
author="Alves, Gleifer Vaz
and Dennis, Louise
and Fernandes, Lucas
and Fisher, Michael",
editor="Leitner, Andrea
and Watzenig, Daniel
and Ibanez-Guzman, Javier",
title="Reliable Decision-Making in Autonomous Vehicles",
bookTitle="Validation and Verification of Automated Systems: Results of the ENABLE-S3 Project",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="105--117",
abstract="The use of Autonomous Vehicles (AVs) on our streets is soon to be a reality; increasingly, interacting with such AVs will be part of our daily routine. However, we will certainly need to assure the reliable behaviour of an AV, especially when some unexpected scenarios (e.g. harsh environments, obstacles, emergencies) are taken into account. In this article we use an intelligent agent approach to capture the high-level decision-making process within an AV and then use formal verification techniques to automatically, and strongly, analyse the required behaviours. Specifically, we use the MCAPL framework, wherein our core agent is implemented using the GWENDOLEN agent programming language, and to which we can apply model checking via the AJPF model checker. By performing such formal verification on our agent, we are able to prove that the AV's decision-making process, embedded within the GWENDOLEN agent plans, matches our requirements. As examples, we will verify (formal) properties in order to determine whether the agent behaves in a reliable manner through three different levels of emergency displayed in a simple urban traffic environment.",
isbn="978-3-030-14628-3",
doi="10.1007/978-3-030-14628-3_10",
url="https://doi.org/10.1007/978-3-030-14628-3_10"
}
      

@inproceedings{alves19,
   author="Gleifer Alves and Louise A. Dennis and Michael Fisher",
   title="A Model Checking Agent-Based Architecture for Representing the Rules of the Road on Autonomous Vehicles.",
   booktitle="Formal Methods for Autonomous Systems",
   year=2019
}


@misc{farrell2019modular,
    title={Modular Verification of Autonomous Space Robotics},
    author={Marie Farrell and Rafael C. Cardoso and Louise A. Dennis and Clare Dixon and Michael Fisher and Georgios Kourtis and Alexei Lisitsa and Matt Luckcuck and Matt Webster},
    year={2019},
    eprint={1908.10738},
    archivePrefix={arXiv},
    primaryClass={cs.SE}
}

      
@InProceedings{10.1007/978-3-030-30446-1_25,
author="Farrell, Marie
and Bradbury, Matthew
and Fisher, Michael
and Dennis, Louise A.
and Dixon, Clare
and Yuan, Hu
and Maple, Carsten",
editor="{\"O}lveczky, Peter Csaba
and Sala{\"u}n, Gwen",
title="Using Threat Analysis Techniques to Guide Formal Verification: A Case Study of Cooperative Awareness Messages",
booktitle="Software Engineering and Formal Methods",
year="2019",
publisher="Springer International Publishing",
address="Cham",
pages="471--490",
abstract="Autonomous robotic systems such as Connected and Autonomous Vehicle (CAV) systems are both safety-and security-critical, since a breach in system security may impact safety. Generally, safety and security concerns for such systems are treated separately during the development process. In this paper, we consider an algorithm for sending Cooperative Awareness Messages (CAMs) between vehicles in a CAV system and the use of CAMs in preventing vehicle collisions. We employ threat analysis techniques that are commonly used in the cyber security domain to guide our formal verification. This allows us to focus our formal methods on those security properties that are particularly important and to consider both safety and security in tandem. Our analysis centres on identifying STRIDE security properties and we illustrate how these can be formalised, and subsequently verified, using a combination of formal tools for distinct aspects, namely Promela/SPIN and Dafny.",
isbn="978-3-030-30446-1"
}
      
      
@article{Luckcuck2019,
title = {{Formal Specification and Verification of Autonomous Robotic Systems: A Survey}},
author = {Luckcuck, Matt and Farrell, Marie and Dennis, Louise A. and Dixon, Clare and Fisher, Michael},
doi = {10.1145/3342355},
eprint = {1807.00048},
issn = {03600300},
journal = {ACM Comput. Surv.},
month = {sep},
number = {5},
pages = {1--41},
url = {https://arxiv.org/abs/1807.00048 http://dl.acm.org/citation.cfm?doid=3362097.3342355},
volume = {52},
year = {2019}
}


@InProceedings{koeman_emas19,
author="Koeman, Vincent J.
and Dennis, Louise A.
and Webster, Matt
and Fisher, Michael
and Hindriks, Koen",
editor="Dennis, Louise A.
and Bordini, Rafael H.
and Lesp{\'e}rance, Yves",
title="The ``Why Did You Do That?'' Button: Answering Why-Questions for End Users of Robotic Systems",
booktitle="Engineering Multi-Agent Systems",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="152--172",
abstract="The issue of explainability for autonomous systems is becoming increasingly prominent. Several researchers and organisations have advocated the provision of a ``Why did you do that?'' button which allows a user to interrogate a robot about its choices and actions. We take previous work on debugging cognitive agent programs and apply it to the question of supplying explanations to end users in the form of answers to why-questions. These previous approaches are based on the generation of a trace of events in the execution of the program and then answering why-questions using the trace. We implemented this framework in the agent infrastructure layer and, in particular, the Gwendolen programming language it supports -- extending it in the process to handle the generation of applicable plans and multiple intentions. In order to make the answers to why-questions comprehensible to end users we advocate a two step process in which first a representation of an explanation is created and this is subsequently converted into natural language in a way which abstracts away from some events in the trace and employs application specific predicate dictionaries in order to translate the first-order logic presentation of concepts within the cognitive agent program in natural language. A prototype implementation of these ideas is provided.",
isbn="978-3-030-51417-4"
}


      @InProceedings{cardoso_emas19,
   author = {Rafael C. Cardoso and Louise A. Dennis and Michael Fisher},
    title = {Plan Library Reconfigurability in BDI Agents},
booktitle = {Proceedings of the 7th International Workshop in Engineering Multi-Agent Systems},
year = 2019,
address = {Montreal, Canada},
url={http://cgi.csc.liv.ac.uk/~lad/emas2019/accepted/EMAS2019_paper_24.pdf}author="Cardoso, Rafael C.
and Dennis, Louise A.
and Fisher, Michael",
editor="Dennis, Louise A.
and Bordini, Rafael H.
and Lesp{\'e}rance, Yves",
title="Plan Library Reconfigurability in BDI Agents",
booktitle="Engineering Multi-Agent Systems",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="195--212",
abstract="One of the major advantages of modular architectures in robotic systems is the ability to add or replace nodes, without needing to rearrange the whole system. In this type of system, autonomous agents can aid in the decision making and high-level control of the robot. For example, a robot may have a module for each of the effectors and sensors that it has and an agent with a plan library containing high-level plans to aid in the decision making within these modules. However, when autonomously replacing a node it can be difficult to reconfigure plans in the agent's plan library while retaining correctness. In this paper, we exploit the formal concept of capabilities in Belief-Desire-Intention agents and describe how agents can reason about these capabilities in order to reconfigure their plan library while retaining overall correctness constraints. To validate our approach, we show the implementation of our framework and an experiment using a practical example in the Mars rover scenario.",
isbn="978-3-030-51417-4"
}



@article{bremner19,
author={Paul Bremner and Louise A. Dennis and Michael Fisher and Alan F. Winfield},
title ={On Proactive, Transparent and Verifiable Ethical Reasoning for Robots},
journal={Proceedings of the IEEE special issue on Machine Ethics: The Design and Governance of Ethical AI and Autonomous Systems},
volume=107,
issue=3,
pages={541--561},
year=2019}
      

@article{dennis18iib,
author={Louise A. Dennis and Marija Slavkovik},
title ={Machines That Know Right And Cannot Do Wrong: The Theory and Practice of Machine Ethics},
journal={IEEE Intelligent Informatics Bulletin},
volume=19,
number=1,
year=2018}


@TechReport{dennis18rais,
  author = 	 {Louise A. Dennis},
  title = 	 {Reconfigurable Autonomy: Architecture and Configuration Language},
  institution =  {University of Liverpool, Department of Computer Science},
  year = 	 2018,
  number =	 {ULCS-18-002}
}
      

@InProceedings{10.1007/978-3-030-03769-7_15,
author="Ferrando, Angelo
and Dennis, Louise A. 
and Ancona, Davide
and Fisher, Michael
and Mascardi, Viviana",
editor="Colombo, Christian
and Leucker, Martin",
title="Verifying and Validating Autonomous Systems: Towards an Integrated Approach",
booktitle="Runtime Verification",
year="2018",
publisher="Springer International Publishing",
address="Cham",
pages="263--281",
abstract="When applying formal verification to a system that interacts with the real world we must use a model of the environment. This model represents an abstraction of the actual environment, but is necessarily incomplete and hence presents an issue for system verification. If the actual environment matches the model, then the verification is correct; however, if the environment falls outside the abstraction captured by the model, then we cannot guarantee that the system is well-behaved. A solution to this problem consists in exploiting the model of the environment for statically verifying the system's behaviour and, if the verification succeeds, using it also for validating the model against the real environment via runtime verification. The paper discusses this approach and demonstrates its feasibility by presenting its implementation on top of a framework integrating the Agent Java PathFinder model checker. Trace expressions are used to model the environment for both static formal verification and runtime verification.",
isbn="978-3-030-03769-7"
}


      
@InProceedings{fisher_wosocer18,
   author = {Michael Fisher and Emily C. Collins and Louise A. Dennis and Matthew Luckcuck and Matthew P. Webster and Mike Jump and Vincent Page and Charles Patchet and Fateme Dinmohammadi and David Flynn and Valentin Robu and Xingu Zhao},
    title = {Verifiable Self-Certifying Autonomous Systems},
booktitle = {8th IEEE International Workshop on Software Certification (WoSoCer)},
year = 2018
      }


      
@InProceedings{bentzen_vavas18,
   author = {Martin Mose Bentzen and Felix Lindner and Louise Dennis and  Michael Fisher},
    title = {Moral Permissability of Actions in Smart Home Systems},
booktitle = {Workshop on Robots, Morality, and Trust through the Verification Lens},
year = 2018
      }

      
      
@InProceedings{alves_vavas18,
   author = {Gleifer Alves and Louise Dennis and Michael Fisher},
    title = "{Formalisation of the Rules of the Road for embedding into an Autonomous Vehicle Agent}",
booktitle = {Workshop on Verification and Validation of Autonomous Systems},
year = 2018
}


      
@InProceedings{10.1007/978-3-030-25693-7_8,
author="Winikoff, Michael
and Dennis, Louise
and Fisher, Michael",
editor="Weyns, Danny
and Mascardi, Viviana
and Ricci, Alessandro",
title="Slicing Agent Programs for More Efficient Verification",
booktitle="Engineering Multi-Agent Systems",
year="2019",
publisher="Springer International Publishing",
address="Cham",
pages="139--157",
abstract="Agent programs are increasingly used as the core high-level decision-making components within a range of autonomous systems and, as the deployment of such systems in safety-critical scenarios develops, the need for strong and trustworthy verification becomes acute. Formal verification techniques such as model-checking provide this high level of assurance yet they are typically both complex and slow to deploy. In this chapter we introduce, develop and evaluate a program slicing technique that significantly improves the efficiency of such verification, hence providing more effective routes to the assurance of safety, reliability, and ethics in autonomous systems.",
isbn="978-3-030-25693-7"
}

    
      @InProceedings{ferrando_aamas18,
   author = {Angelo Ferrando and Louise A. Dennis and Davide Ancona and Michael Fisher and Viviana Mascardi}.
    title = "{Recognising Assumption Violations in Autonomous Systems Verificaion}",
booktitle = {Proceedings of the 2018 International Conference on Autonomous Agents and Multiagent Systems},
year = 2018,
address = {Stockholm, Sweden},
pages={1933-1936}
}



@Article{dennis18:mcapl,
  author="Louise A Dennis",
  title="The MCAPL Framework including the Agent Infrastructure Layer and Agent Java Pathfinder",
  journal = "The Journal of Open Source Software",
  year = 2018,
  volume=3,
  number=24}


@InProceedings{dennis_isaim18,
   author = {Louise A. Dennis and Michael Fisher},
    title = "{Practical Challenges in Explicit Ethical Machine Reasoning}",
booktitle = {International Symposium on Artificial Intelligence and Mathematics},
year = 2018,
address = {Fort Lauderdale, USA},
url={http://isaim2018.cs.virginia.edu/papers/ISAIM2018_Ethics_Dennis_Fischer.pdf},
note={Also available as ArXiv pre-print 1801.01422}
}


@InProceedings{dignum18,
author = 	 {Virginia Dignum and Matteo Baldoni and Cristina Baroglio and Maurizio Caon and  Raja Chatila and Louise Dennis and Gonzalo G\'{e}nova and Malte Klie{\ss} and Maite Lopez-Sanchez and Roberto Micalizio and Juan Pav\'{o}n and Marija Slavkovik and Matthijs Smakman and Marlies van Steenbergen and  Stefano Tedeschi and Leon van der Torre and Serena Villata and Tristan de Wildt and Galit Haim},
title = 	 {Ethics by Design: necessity or curse?},
booktitle = {AAAI/ACM Conference on Artificial Intelligence, Ethics and Society},
year = 	 2018,
address = 	 {New Orleans, USA}}

      
@InProceedings{bjorgen18,
author = 	 {Edvard P. Bj{\o}rgen and Simen Madsen and Therese S. Bj{\o}rknes and  Fredrik V. Heims{\ae}ter and Robin H{\aa}vik and Morten Linderud and Per-Niklas Longberg and Louise A. Dennis and Marija Slavkovik},
title = 	 {Cake, death, and trolleys: dilemmas as benchmarks of ethical decision-making},
booktitle = {AAAI/ACM Conference on Artificial Intelligence, Ethics and Society},
year = 	 2018,
address = 	 {New Orleans, USA}}

      

@Article{aitken17:_auton_nuclear_waste_manag,
  author = 	 {Jonathan M. Aitken and Affan Shaukat and Elisa Cucco and Louise A. Dennis and Sandor M. Veres and Yang Gao and Michael Fisher and Jeffrey A. Kuo and Thomas Robinson and Paul E. Mort},
  title = 	 {Autonomous Nuclear Waste Management},
  journal = 	 {IEEE Intelligent Systems},
  year = 	 2017,
  note = 	 {In Press}}
      


@Inbook{Dennis2017,
author="Dennis, Louise A.
and Slavkovik, Marija
and Fisher, Michael",
editor="Cranefield, Stephen
and Mahmoud, Samhar
and Padget, Julian
and Rocha, Ana Paula",
title="``How Did They Know?''---Model-Checking for Analysis of Information Leakage in Social Networks",
bookTitle="Coordination, Organizations, Institutions, and Norms in Agent Systems XII: COIN 2016 International Workshops, COIN@AAMAS, Singapore, Singapore, May 9, 2016, COIN@ECAI, The Hague, The Netherlands, August 30, 2016, Revised Selected Papers",
year="2017",
publisher="Springer International Publishing",
address="Cham",
pages="42--59",
abstract="We examine the use of model-checking in the analysis of information leakage in social networks. We take previous work on the formal analysis of digital crowds and show how a variation on the formalism can naturally model the interaction of people and groups of followers in intersecting social networks. We then show how probabilistic models of the forwarding and reposting behaviour of individuals can be used to analyse the risk that information will leak to unwanted parties. We illustrate our approach by analysing several simple examples.",
isbn="978-3-319-66595-5",
doi="10.1007/978-3-319-66595-5_3",
url="https://doi.org/10.1007/978-3-319-66595-5_3"
}


@InProceedings{dennis17:_gener_archit_flexib_auton_system,
author = 	 {Louise Dennis and Elisa Cucco and Michael Fisher},
title = 	 {A General Architecture for Flexible Autonomous Systems},
booktitle = {Workshop on Architectures for Generality and Autonomy (AGA 2017)},
year = 	 2017,
address = 	 {Melbourne, Australia},
note = 	 {Available at http://cadia.ru.is/workshops/aga2017/}}


@InProceedings{cucco17:_towar_robot_social_engag,
  author = 	 {Elisa Cucco and Michael Fisher and Louise Dennis and Clare Dixon and Matt Webster and Bastian Broecker and Richard Williams and Joe Collenette and Katie Atkinson and Karl Tuyls},
  title = 	 {Towards Robots for Social Engagement},
  booktitle = {Workshop on Human-Robot Engagement in the Home, Workplace and Public Spaces (WHRE 2017)},
  year = 	 2017,
  note = 	 {Published at http://ijcaihumanrobotengagement.webnode.com}}



@article{Kamali2017,
title = "Formal verification of autonomous vehicle platooning ",
journal = "Science of Computer Programming ",
volume = "148",
number = "",
pages = "88--106",
year = "2017",
note = "",
issn = "0167-6423",
doi = "https://doi.org/10.1016/j.scico.2017.05.006",
url = "http://www.sciencedirect.com/science/article/pii/S0167642317301168",
author = "Maryam Kamali and Louise A. Dennis and Owen McAree and Michael Fisher and Sandor M. Veres",
keywords = "Vehicle platooning",
keywords = "Agent programming",
keywords = "Model checking "
}



@article{DBLP:journals/corr/KamaliDMFV16,
  author    = {Maryam Kamali and
               Louise A. Dennis and
               Owen McAree and
               Michael Fisher and
               Sandor M. Veres},
  title     = {Formal Verification of Autonomous Vehicle Platooning},
  journal   = {CoRR},
  volume    = {abs/1602.01718},
  year      = {2016},
  url       = {http://arxiv.org/abs/1602.01718},
  timestamp = {Tue, 01 Mar 2016 17:47:25 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/KamaliDMFV16},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}


@ARTICLE{2017arXiv170304741C,
   author = {{Charisi}, V. and {Dennis}, L. and {Fisher}, M. and {Lieck}, R. and 
	{Matthias}, A. and {Slavkovik}, M. and {Sombetzki}, J. and {Winfield}, A.~F.~T. and 
	{Yampolskiy}, R.},
    title = "{Towards Moral Autonomous Systems}",
  journal = {ArXiv e-prints},
archivePrefix = "arXiv",
   eprint = {1703.04741},
 primaryClass = "cs.AI",
 keywords = {Computer Science - Artificial Intelligence},
     year = 2017,
    month = mar,
   adsurl = {http://adsabs.harvard.edu/abs/2017arXiv170304741C},
  adsnote = {Provided by the SAO/NASA Astrophysics Data System}
}


@TechReport{dennis17gwen,
  author = 	 {Louise A. Dennis},
  title = 	 {Gwendolen Semantics: 2017},
  institution =  {University of Liverpool, Department of Computer Science},
  year = 	 2017,
  number =	 {ULCS-17-001}
}


@Inbook{Dennis2016,
author="Dennis, Louise A.
and Aitken, Jonathan M.
and Collenette, Joe
and Cucco, Elisa
and Kamali, Maryam
and McAree, Owen
and Shaukat, Affan
and Atkinson, Katie
and Gao, Yang 
and Veres, Sandor M.
and Fisher, Michael",
editor="Alboul, Lyuba
and Damian, Dana
and Aitken, M. Jonathan",
title="Agent-Based Autonomous Systems and Abstraction Engines: Theory Meets Practice",
bookTitle="Towards Autonomous Robotic Systems: 17th Annual Conference, TAROS 2016, Sheffield, UK, June 26--July 1, 2016, Proceedings",
year="2016",
publisher="Springer International Publishing",
address="Cham",
pages="75--86",
isbn="978-3-319-40379-3",
doi="10.1007/978-3-319-40379-3_8",
url="http://dx.doi.org/10.1007/978-3-319-40379-3_8"
}


@ARTICLE{6632950, 
author={Lincoln, N.K. and Veres, S.M. and Dennis, L.A. and Fisher, M. and Lisitsa, A.}, 
journal={Computational Intelligence Magazine, IEEE}, 
title={Autonomous Asteroid Exploration by Rational Agents}, 
year={2013}, 
volume={8}, 
number={4}, 
pages={25-38}, 
keywords={asteroids;formal verification;natural language processing;object-oriented programming;software agents;agent reasoning;autonomous asteroid exploration;autonomous space missions;belief-desire-intention architectures;formal verifiability;natural language definitions;novel anthropomorphic agent architecture;rational agents;real-time decision-making;skill descriptions;software agent architectures;Asteroids;Computer architecture;Real-time systems;Software agents;Software architecture;Space vehicles}, 
doi={10.1109/MCI.2013.2279559}, 
ISSN={1556-603X}, 
month={Nov},}


@article{Dennis2015,
title = "Formal verification of ethical choices in autonomous systems ",
journal = "Robotics and Autonomous Systems ",
volume = "",
number = "",
pages = " - ",
year = "2015",
note = "",
issn = "0921-8890",
doi = "http://dx.doi.org/10.1016/j.robot.2015.11.012",
url = "http://www.sciencedirect.com/science/article/pii/S0921889015003000",
author = "Louise Dennis and Michael Fisher and Marija Slavkovik and Matt Webster",
keywords = "Autonomous systems",
keywords = "Ethics",
keywords = "BDI programs",
keywords = "Formal verification "
}


@inproceedings{vanRiemsdijk:2015:SFS:2772879.2772935,
 author = {van Riemsdijk, M. Birna and Dennis, Louise and Fisher, Michael and Hindriks, Koen V.},
 title = {A Semantic Framework for Socially Adaptive Agents: Towards Strong Norm Compliance},
 booktitle = {Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems},
 series = {AAMAS '15},
 year = {2015},
 isbn = {978-1-4503-3413-6},
 location = {Istanbul, Turkey},
 pages = {423--432},
 numpages = {10},
 url = {http://dl.acm.org/citation.cfm?id=2772879.2772935},
 acmid = {2772935},
 publisher = {International Foundation for Autonomous Agents and Multiagent Systems},
 address = {Richland, SC},
 keywords = {agent programming languages, executable temporal logic, formal semantics, norm compliance, norm-aware agents},
} 


@InProceedings{dennis15:_towar_verif_ethic_robot_behav,
	author = 			 {Louise A. Dennis and Michael Fisher and Alan F. T. Winfield},
	title = 			 {Towards Verifiably Ethical Robot Behaviour},
	booktitle = {AAAI Workshop on AI and Ethics (1st International Conference on AI and Ethics)},
	year = 		 2015,
	month = 		 {January},
	address = 	 {Austin, TX}}



@article{slavkovik15,
year=2015,
issn={0926-8782},
journal={Distributed and Parallel Databases},
volume=33,
number=1,
doi={10.1007/s10619-014-7161-y},
title={An abstract formal basis for digital crowds},
url={http://dx.doi.org/10.1007/s10619-014-7161-y},
publisher={Springer US},
keywords={Logical foundations; Crowd specification; Formal verification; Predictability},
author={Slavkovik, Marija and Dennis, LouiseA. and Fisher, Michael},
pages={3-31},
language={English}
}


@article{Dennis16022015,
author = {Dennis, Louise A. and Fisher, Michael and Webster, Matt}, 
title = {Two-stage agent program verification},
year = {2018}, 
doi = {10.1093/logcom/exv002}, 
volume=28,
issue=3,
pages={499-523},
abstract ={We describe an extension to the AJPF agent program model-checker so that it may be used to generate models for input into other, non-agent, model-checkers. We motivate this adaptation, arguing that it potentially improves the efficiency of the model-checking process and provides access to richer property specification languages. We illustrate the approach by describing the export of AJPF program models to both the SPIN and Prism model-checkers. We also investigate, experimentally, the effect the process has on the overall efficiency of model-checking.}, 
URL = {http://logcom.oxfordjournals.org/content/early/2015/02/16/logcom.exv002.abstract}, 
eprint = {http://logcom.oxfordjournals.org/content/early/2015/02/16/logcom.exv002.full.pdf+html}, 
journal = {Journal of Logic and Computation} 
}


@TechReport{dennis14ros,
  author = 	 {Louise A. Dennis},
  title = 	 {{ROS}-{AIL} Integration},
  institution =  {University of Liverpool, Department of Computer Science},
  year = 	 2014,
  number =	 {ULCS-14-004}
}


@article{dennis_ase14,
year={2016},
issn={0928-8910},
journal={Automated Software Engineering},
doi={10.1007/s10515-014-0168-9},
title={Practical verification of decision-making in agent-based autonomous systems},
url={http://dx.doi.org/10.1007/s10515-014-0168-9},
publisher={Springer US},
keywords={Hybrid systems; Model checking; Agent architectures},
author={Dennis, Louise A. and Fisher, Michael and Lincoln, Nicholas K. and Lisitsa, Alexei and Veres, Sandor M.},
volume=23,
number=3,
pages={305-359},
language={English}
}



@incollection{
year={2014},
isbn={978-3-662-43644-8},
booktitle={Towards Autonomous Robotic Systems},
series={Lecture Notes in Computer Science},
editor={Natraj, Ashutosh and Cameron, Stephen and Melhuish, Chris and Witkowski, Mark},
doi={10.1007/978-3-662-43645-5_45},
title={Ethical Choice in Unforeseen Circumstances},
url={http://dx.doi.org/10.1007/978-3-662-43645-5_45},
publisher={Springer Berlin Heidelberg},
author={Dennis, Louise and Fisher, Michael and Slavkovik, Marija and Webster, Matt},
pages={433-445},
language={English}
}



@InProceedings{dennis14:_action_durat_failur_bdi_languag,
  author = 	 {Louise A. Dennis and Michael Fisher},
  title = 	 {Actions with Durations and Failures in BDI Languages},
  booktitle = {21st European Conference on Artificial Intelligence (ECAI 2014)},
  year = 	 2014,
  editor = 	 {Torsten Schaub},
  series = {Frontiers in Artificial Intelligence and Applications},
  volume = 263,
  pages = {995--996},
  publisher = {IOS Press}}


@TechReport{dennis14,
  author = 	 {Louise A. Dennis and Michael Fisher},
  title = 	 {Actions with Durations and Failures in BDI Languages},
  institution =  {University of Liverpool, Department of Computer Science},
  year = 	 2014,
  number =	 {ULCS-14-003}
}


@article{
year={2014},
issn={0933-1875},
journal={KI - Künstliche Intelligenz},
volume={28},
number={3},
doi={10.1007/s13218-014-0308-1},
title={Reconfigurable Autonomy},
url={http://dx.doi.org/10.1007/s13218-014-0308-1},
publisher={Springer Berlin Heidelberg},
keywords={Hybrid systems; Autonomous vehicles; Intelligent agents; Robotics},
author={Dennis, Louise A. and Fisher, Michael and Aitken, Jonathan M. and Veres, Sandor M. and Gao, Yang and Shaukat, Affan and Burroughes, Guy},
pages={199-207},
language={English}
}


@inproceedings{DBLP:conf/clima/DennisFW13,
  author    = {Louise A. Dennis and
               Michael Fisher and
               Matthew P. Webster},
  title     = {Using Agent JPF to Build Models for Other Model Checkers},
  editor    = {Jo{\~a}o Leite and
               Tran Cao Son and
               Paolo Torroni and
               Leon van der Torre and
               Stefan Woltran},
  booktitle     = {Computational Logic in Multi-Agent Systems - 14th International
               Workshop, CLIMA XIV, Corunna, Spain, September 16-18, 2013.
               Proceedings},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {8143},
  year      = {2013},
  pages     = {273-289},
  ee        = {http://dx.doi.org/10.1007/978-3-642-40624-9_17},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@inproceedings{DBLP:conf/atal/RiemsdijkDFH13,
  author    = {M. Birna van Riemsdijk and
               Louise A. Dennis and
               Michael Fisher and
               Koen V. Hindriks},
  title     = {Agent reasoning for norm compliance: a semantic approach},
  editor    = {Maria L. Gini and
               Onn Shehory and
               Takayuki Ito and
               Catholijn M. Jonker},
  booktitle     = {International conference on Autonomous Agents and Multi-Agent
               Systems, AAMAS '13, Saint Paul, MN, USA, May 6-10, 2013},
  year      = {2013},
  pages     = {499-506},
  ee        = {http://dl.acm.org/citation.cfm?id=2485000},
  isbn      = {978-1-4503-1993-5},
  publisher = {IFAAMAS},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{DBLP:journals/cacm/FisherDW13,
  author    = {Michael Fisher and
               Louise A. Dennis and
               Matthew P. Webster},
  title     = {Verifying autonomous systems},
  journal   = {Commun. ACM},
  volume    = {56},
  number    = {9},
  year      = {2013},
  pages     = {84-93},
  ee        = {http://doi.acm.org/10.1145/2494558},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@article{DBLP:journals/eceasst/ArapinisCDFGKMRRSUY09,
  author    = {Myrto Arapinis and
               Muffy Calder and
               Louise A. Dennis and
               Michael Fisher and
               Philip D. Gray and
               Savas Konur and
               Alice Miller and
               Eike Ritter and
               Mark Ryan and
               Sven Schewe and
               Chris Unsworth and
               Rehana Yasmin},
  title     = {Towards the Verification of Pervasive Systems},
  journal   = {ECEASST},
  volume    = {22},
  year      = {2009},
  ee        = {http://eceasst.cs.tu-berlin.de/index.php/eceasst/article/view/315},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{DBLP:conf/clima/StockerSDDF11,
  author    = {Richard Stocker and
               Maarten Sierhuis and
               Louise A. Dennis and
               Clare Dixon and
               Michael Fisher},
  title     = {A Formal Semantics for Brahms},
  year      = {2011},
  pages     = {259-274},
  ee        = {http://dx.doi.org/10.1007/978-3-642-22359-4_18},
  editor    = {Jo{\~a}o Leite and
               Paolo Torroni and
               Thomas {\AA}gotnes and
               Guido Boella and
               Leon van der Torre},
  booktitle     = {Computational Logic in Multi-Agent Systems - 12th International
               Workshop, CLIMA XII, Barcelona, Spain, July 17-18, 2011.
               Proceedings},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {6814},
  year      = {2011},
  isbn      = {978-3-642-22358-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{DBLP:conf/jelia/StockerDDF12,
  author    = {Richard Stocker and
               Louise A. Dennis and
               Clare Dixon and
               Michael Fisher},
  title     = {Verifying Brahms Human-Robot Teamwork Models},
  year      = {2012},
  pages     = {385-397},
  ee        = {http://dx.doi.org/10.1007/978-3-642-33353-8_30},
  editor    = {Luis Fari{\~n}as del Cerro and
               Andreas Herzig and
               J{\'e}r{\^o}me Mengin},
  booktitle     = {Logics in Artificial Intelligence - 13th European Conference,
               JELIA 2012, Toulouse, France, September 26-28, 2012. Proceedings},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {7519},
  year      = {2012},
  isbn      = {978-3-642-33352-1},
  ee        = {http://dx.doi.org/10.1007/978-3-642-33353-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@incollection{
year={2012},
isbn={978-3-642-29112-8},
booktitle={Declarative Agent Languages and Technologies IX},
volume={7169},
series={Lecture Notes in Computer Science},
editor={Sakama, Chiaki and Sardina, Sebastian and Vasconcelos, Wamberto and Winikoff, Michael},
doi={10.1007/978-3-642-29113-5_2},
Title={Plan Indexing for State-Based Plans},
url={http://dx.doi.org/10.1007/978-3-642-29113-5_2},
publisher={Springer Berlin Heidelberg},
author={Dennis, Louise A.},
pages={3-15}
}


@inproceedings{LVDFL10:ALCOSP,
   author=" Lincoln, N. and  Veres, S. M. and Dennis, L. A. and Fisher, M. and
           and Lisitsa, A.",
   title="{An Agent Based Framework for
  Adaptive Control and Decision Making of Autonomous Vehicles}",
   booktitle="Proc. IFAC Workshop on Adaptation and Learning in Control
  and Signal Processing (ALCOSP)",
   year=2010
}


@inproceedings{DALT10:abstraction,
  author="Dennis, L. A. and Fisher, M. and
           Lincoln, N. and Lisitsa, A. and Veres, S. M.",
  title="{Declarative Abstractions for Agent Based Hybrid Control Systems}",
  booktitle="Proc. 8th International Workshop on Declarative Agent Languages and Technologies (DALT)",
   series="{LNCS}",
   publisher="Springer",
   volume=6619,
   pages="96--111",
year=2010
}


@article{springerlink:10.1007/s10515-011-0088-x,
   author = {Dennis, Louise and Fisher, Michael and Webster, Matthew and Bordini, Rafael},
   affiliation = {Department of Computer Science, University of Liverpool, Liverpool, L69 3BX UK},
   title = {Model checking agent programming languages},
   journal = {Automated Software Engineering},
   publisher = {Springer Netherlands},
   issn = {0928-8910},
   keyword = {Computer Science},
   pages = {1-59},
   url = {http://dx.doi.org/10.1007/s10515-011-0088-x},
   note = {10.1007/s10515-011-0088-x},
   year = {2011}
}


@InCollection{r.10:_direc_agent_model_check,
  author = 	 {R. H. Bordini, L. A. Dennis, B. Farwer and M. Fisher},
  title = 	 {Directions for Agent Model Checking},
  booktitle = 	 {Specification and Verification of Multi-agent Systems},
  pages =	 {103--123},
  publisher =	 {Springer US},
  year =	 2010,
  editor =	 {M. Dastani, K. V. Hindriks, J.-J. C. Meyer},
  chapter =	 4,
  url= {http://dx.doi.org/10.1007/978-1-4419-6984-2}
}


@article {springerlink:10.1007/s10817-010-9177-y,
   author = {Dennis, Louise and Green, Ian and Smaill, Alan},
   affiliation = {University of Liverpool School of Computer Science Liverpool L69 3BX UK},
   title = {The Use of Embeddings to Provide a Clean Separation of Term and Annotation for Higher Order Rippling},
   journal = {Journal of Automated Reasoning},
   volume = {47},
   issue = {1},
   publisher = {Springer Netherlands},
   issn = {0168-7433},
   keyword = {Computer Science},
   pages = {57-105},
   url = {http://dx.doi.org/10.1007/s10817-010-9177-y},
   note = {10.1007/s10817-010-9177-y},
   year = {2011}
}


@InProceedings{louise10:_reduc_code_compl_hybrid_auton_contr_system,
  author = 	 {Louise A. Dennis, Michael Fisher, Nicholas K. Lincoln, Alexei Lisitsa, and Sandor M. Veres},
  title = 	 {Reducing Code Complexity in Hybrid Autonomous Control Systems},
  booktitle = 	 {The 10th International Symposium on Artificial Intelligence, Robotics and Automation in Space (iSAIRAS 2010)},
  year =	 2010,
  editor =	 {Takashi Kubota}
}



@article{DBLP:journals/expert/DennisFLLV10,
  author    = {Louise A. Dennis and
               Michael Fisher and
               Alexei Lisitsa and
               Nicholas Lincoln and
               Sandor M. Veres},
  title     = {Satellite Control Using Rational Agent Programming},
  journal   = {IEEE Intelligent Systems},
  volume    = {25},
  number    = {3},
  year      = {2010},
  pages     = {92-97},
  ee        = {http://dx.doi.org/10.1109/MIS.2010.88},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{DBLP:conf/clima/DennisTM09,
  author    = {Louise A. Dennis and
               Nick A. M. Tinnemeier and
               John-Jules Ch. Meyer},
  title     = {Model Checking Normative Agent Organisations},
  editor    = {J{\"u}rgen Dix and
               Michael Fisher and
               Peter Nov{\'a}k},
  booktitle     = {Computational Logic in Multi-Agent Systems - 10th International
               Workshop, CLIMA X, Hamburg, Germany, September 9-10, 2009,
               Revised Selected and Invited Papers},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = 6214,
  isbn      = {978-3-642-16866-6},
  year      = 2009,
  pages     = {64-82},
  ee        = {http://dx.doi.org/10.1007/978-3-642-16867-3_4},
  crossref  = {DBLP:conf/clima/2009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@inproceedings{DBLP:journals/corr/abs-1003-0617,
  author    = {Louise A. Dennis and
               Michael Fisher and
               Nicholas Lincoln and
               Alexei Lisitsa and
               Sandor M. Veres},
  title     = {Agent Based Approaches to Engineering Autonomous Space Software},
  editor    = {Manuela L. Bujorianu and
               Michael Fisher},
  booktitle     = {Proceedings FM-09 Workshop on Formal Methods for Aerospace},
  series    = {EPTCS},
  volume    = 20,
  year      = 2009,
  pages     = {63-67},
  ee        = {http://dx.doi.org/10.4204/EPTCS.20.6},
}


@INPROCEEDINGS{BDFF08:ASE,
  author = {R. H. Bordini and L. A. Dennis and B. Farwer and M. Fisher},
  title = {{Automated Verification of Multi-Agent Programs}},
  booktitle = {Proc. 23rd IEEE/ACM International Conference on Automated Software
	Engineering (ASE)},
  year = {2008},
  publisher=2008,
  pages = {69--78}
}


@TechReport{fisher09,
  author = 	 {Michael Fisher and Louise Dennis and Anthony Hepple},
  title = 	 {Modular Multi-Agent Design},
  institution =  {University of Liverpool, Department of Computer Science},
  year = 	 2009,
  number =	 {ULCS-09-002}
}


@TechReport{webster09,
  author = 	 {Matt Webster and Louise Dennis and Michael Fisher},
  title = 	 {Model Checking Auctions, Coalitions and Trust},
  institution =  {University of Liverpool, Department of Computer Science},
  year = 	 2009,
  number =	 {ULCS-09-004}
}


@InProceedings{dennis08:_gwend,
  author = 	 {Louise A. Dennis and Berndt Farwer},
  title = 	 {Gwendolen: A BDI Language for Verifiable Agents},
  booktitle = 	 {Logic and the Simulation of Interaction and Reasoning},
  year =	 2008,
  editor =	 {Benedikt L{\"o}we},
  address =	 {Aberdeen},
  publisher =	 {AISB},
  note =	 {AISB'08 Workshop}
}


@InProceedings{dennis08:_progr_verif_heter_agent_system,
  author = 	 {Louise A. Dennis and Michael Fisher},
  title = 	 {Programming Verifiable Heterogeneous Agent Systems},
  booktitle = 	 {Sixth International Workshop on Programming in Multi-Agent Systems (ProMAS'08)},
  year =	 2008,
  address =	 {Estoril, Portugal},
  pages =        {27-42},
  editor =       {Koen Hindriks and Alexander Pokahr and Sebastian Sardina},
  month =	 {May},
}


@InProceedings{dennis08:_progr_verif_heter_agent_system,
  author = 	 {Louise A. Dennis and Michael Fisher},
  title = 	 {Programming Verifiable Heterogeneous Agent Systems},
  editor =	 {Koen Hindriks and Alexander Pokahr and Sebastian Sardina},
  booktitle = 	 {Sixth International Workshop on Programming in Multi-Agent Systems (ProMAS'08)},
  year =	 2008,
  pages =        {27-42},
  address =	 {Estoril, Portugal},
  month =	 {May},
}


@InProceedings{farwer07:_trans,
  author = 	 {B. Farwer and L. Dennis},
  title = 	 {Translating into an intermediate agent layer: A prototype in Maude},
  booktitle = 	 {Proceedings of Concurrency, Specification and Programming (CS\&P 2007)},
  year =	 2007,
  address =	 {Lagow, Poland}
}


@InProceedings{hepple07:_common_basis_agent_organ_bdi_languag,
  author = 	 {Anthony Hepple and Louise A. Dennis and Michael Fisher},
  title = 	 {A Common Basis for Agent Organisation in BDI Languages},
  booktitle = 	 {Languages, Methodologies and Development Tools for Multi-Agent Systems (LADS'07)},
  year =	 2007,
  series =	 {Lecture Notes in Artificial Intelligence},
  publisher =	 {Springer},
}



@InProceedings{dennis07:_found_flexib_multi_agent_progr,
  author = 	 {Louise A. Dennis and Michael Fisher and Antony Hepple},
  title = 	 {Foundations of Flexible Multi-Agent Programming},
  booktitle = 	 {Eighth Workshop on Computational Logic in
      Multi-Agent Systems (CLIMA-VIII)},
  year =	 2007
}



@InProceedings{dennis07:_common_seman_basis_bdi_languag,
  author = 	 {Louise A. Dennis and Rafael H. Bordini and Berndt
	  Farwer and Michael Fisher and Michael Wooldridge},
  M3 = {10.1007/978-3-540-79043-3{\_}8},
  Pages = {124--139},
  Title = {A Common Semantic Basis for BDI Languages},
  Url = {http://dx.doi.org/10.1007/978-3-540-79043-3_8},
  Year = {2008},
  Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-540-79043-3_8}
  booktitle = 	 {Fifth International Workshop on Programming in Multi-Agent Systems (ProMAS'07)},
  series =	 {Lecture Notes in Artificial Intelligence},
  publisher =	 {Springer},
  volume = {4908}
}


@TechReport{dennis07:_chall_probl_induc_theor_prover,
  author = 	 {Louise A. Dennis and Jeremy Gow and Carsten Sch{\"u}rmann},
  title = 	 {Challenge Problems for Inductive Theorem Provers v1.0},
  institution =  {University of Liverpool, Department of Computer Science},
  year = 	 2007,
  number =	 {ULCS-07-004}
}



@InCollection{attfield06,
  author = 	 {Thomas D. Attfield and Monica C. Duarte and Lin Li and Ho-Ying Mak and Adam M. Neal and Lewis M. Toft and Zixuan Wang and Louise A. Dennis},
  title = 	 {26.11 Induction Challenge OMDoc Manager (ICOM)},
  booktitle = 	 {{OMD}oc --
      An Open Markup Format for Mathematical Documents [version 1.2]},
  pages =	 {278--280},
  publisher =	 {Springer},
  year =	 2006,
  editor =	 {Michael Kohlhase},
  volume =	 4180,
  series =	 {Lecture Notes in Artificial Intelligence},
  chapter =	 {26 Applications and Project},
  note =	 {AI Systems Subseries}
}


@InProceedings{dennis06:_progr_slicin_middl_out_reason,
  author = 	 {Louise A. Dennis},
  title = 	 {Program Slicing and Middle-Out Reasoning for Error
          Location and Repair},
  booktitle = 	 {Disproving: Non-Theorems, Non-Validity and Non-Provability},
  year =	 2006
}


@Article{dennis07:_enhan_theor_prover_inter_progr_slice_infor,
  author = 	 {Louise A. Dennis},
  title = 	 {Enhancing Theorem Prover Interfaces with Program Slice Information},
  journal = 	 {Electronic Notes in Theoretical Computer Science (ENTCS)},
  year = 	 2007,
  volume =	 174,
  number =	 2,
  pages =	 {19--33},
  month =	 {May},
  note =	 {Proceedings of the 7th Workshop on User Interfaces for Theorem Provers (UITP 2006)}
}


@InProceedings{dennis05:_compar_proof_plann_system,
  author =       {L. A. Dennis and M. Jamnik and M. Pollet},
  title =        {On the Comparison of Proof Planning Systems: {L}ambda{C}lam, {O}meg
a and {I}sa{P}lanner},
  booktitle =    {12th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2005},
  year =         2006,
  series =       {ENTCS},
  volume = 151,
  issue = 1,
  papges = {93--110}
}




@InProceedings{dennis06:_proof_debug_repair,
  author =       {L. A. Dennis and R. Monroy and P. Nogueira},
  title =        {Proof-directed Debugging and Repair},
  booktitle =    {Seventh Symposium on Trends in Functional Programming 2006},
  pages =        {131--140},
  year =         2006,
  editor =       {H. Nilsson and M. van Eekelen}
}


@inproceedings{Dennis:plagiarism04,
  author="L. A. Dennis",
  editor="A. P. Smith and F. Duggan",
  pages="57--64",
  title="Student Attitudes to Plagiarism and Collusion within Computer
Science",
  booktitle="Plagiarism: Prevention, Practice and Policy Conference
28--30 June 2004",
  publisher="Northumbria University Press",
  year=2005}


@inproceedings{Dennis:tphols05,
  author="L. A. Dennis and P. Nogueira",
  editor="J. Hurd and E. Smith and A. Darbari",
  pages="45--58",
  title="What can be Learned from Failed Proofs of Non-Theorems?",
  booktitle="Theorem Proving in Higher Order Logics (TPHOLs 2005):
Emerging Trends Proceedings",
  note="Technical Report PRG-RP-05-2, Oxford University Computer Laboratory",
  year=2005}


@inproceedings{Dennis:ijcai05,
  author="L. A. Dennis",
  editor="L. P. Kaelbling and A. Saffiotti",
  pages="1558--1559",
  title="An Architecture for Proof Planning Systems",
  booktitle="Nineteenth International Joint Conference on Artificial
Intelligence, IJCAI-05",
  publisher="IJCAI Inc.",
  year=2005}


@technicalreport{Dennisetal05,
  author="L. A. Dennis and I. Green and A. Smaill",
  title="Embeddings as a Higher-Order Representation of Annotations
for Rippling",
  number="Computer Science Technical Report No. NOTTCS-WP-SUB-0503230955-5470", 
  institution="University of Nottingham",
  year=2005,
  notes="Submitted to Journal of Automated Reasoning"}


@article{Sellers:janat04,
  author="W. I. Sellers and L. A. Dennis and W.-J. Wang and R. H. Crompton",
  title="Evaluating alternative gait strategies using evolutionary robotics",
  year="2004",
  journal="Journal of Anatomy",
  volume=204,
  pages="343--351"}
  
  


@InProceedings{AdamsDennis:strata03,
  author="A. A. Adams and L. A. Denns",
  title="Rippling in PVS",
  editor="M. Archer and B. Di Vito and C. Munoz",
  booktitle="Proceedings of Design and Application of
	Strategies/Tactics in Higher Order Logics (STRATA 2003)",
  year=2003,
  pages="84--91",
  publisher="NASA Technical Report CP-2003-212448"}  


@InProceedings{Dennis:disproving04,
  author="L. A. Dennis",
  title="The Use of Proof Planning Critics to Diagnose Errors in the
	Base Cases of Recursive Programs",
  year="2004",
  editor="W. Ahrendt and P. Baumgartner and H. de Nivelle",
  pages="47--58",
  booktitle="IJCAR 2004 Workshop on Disproving: Non-Theorems,
	Non-Validity, Non-Provability"}



@article{Dennis:sttt03,
  author="L. A. Dennis and G. Collins and M. Norrish and R. J. Boulton and K. Slind and T. F. Melham",
  title = "The {\sc PROSPER} toolkit",
  year=2003,
  journal="International Journal on Software Tools for Technology Transfer",
  volume=4,
  number = 2,
  year = 2003,
  pages="189--210"}


@article{Sellers:jeb03,
  author="W. I. Sellers and L. A. Dennis and R. H. Crompton",
  title = "Predicting the metabolic energy costs of bipedalism using evolutionary robotics",
  year=2003,
  journal="Journal of Experimental Biology",
  volume=206,
  pages="1127--1136"}


@InProceedings{Zimmer:calculemus02,
  author="J. Zimmer and L. A. Dennis",
  title="Inductive Theorem Proving and Computer Algebra in the Mathweb
	Software Bus",
  year="2002",
  editor="J. Calmet and  B. Belaid and O. Caprotti and  L. Henocque
	and V. Sorge (Eds.)",
  pages="319--331",
  series="LNAI",
  booktitle="Artificial Intelligence, Automated Reasoning and Symbolic
	Computation, Calculemus 2002",
  number="2385",
  publisher="Springer-Verlag"}



@InProceedings{Dennis:tphols02,
  author="L. A. Dennis and A. Bundy",
  title="A Comparison of two Proof Critics: Power vs. Robustness",
  booktitle="Theorem Proving in Higher Order Logics, 15th
	International Conference, TPHOLs 2002",
  year="2002",
  editor="V. A Carreno and C. A. Munoz and S. Tahar",
  pages="182--197",
  series="LNCS",
  number="2410",
  publisher="Springer-Verlag"}


@article{Dennis:amai00,
  author =       "Dennis, L. and Bundy, A. and Green, I.",
  title =        "Making a productive use of failure to generate
                  witness for coinduction from divergent proof
                  attempts",
  journal =      "Annals of Mathematics and Artificial Intelligence",
  volume =       29,
  pages =        "99--138",
  year =         2000,
  note =         "also paper no. RR0004 in the Informatics Report
                  Series"
}



@InProceedings{Colton:AIM02,
  author="S. Colton and L. Dennis",
  title="The NumbersWithNames Program",
  booktitle="AI&M 3-2002, Seventh
International Symposium on Artificial Intelligence and Mathematics",
  month="January 2-4", 
  year="2002", 
  location="Fort Lauderdale, Florida.",
  notes="Available from http://rutcor.rutgers.edu/~amai/aimath02/"}


@InProceedings{Dennis:TPHOLs01,
  author="L. A. Dennis and A. Smaill",
  title="Ordinal Arithimetic: A Case Study for Rippling in a Higher Order Domain",
  booktitle="Theorem Proving in Higher Order Logics: 14th Internional Conference, TPHOLs 2001",
  pages="185--200",
  series="Lecture Notes in Computer Science",
  number=2152,
  year=2001,
  publisher="Springer-Verlag",
  editor="R. J. Boulton and P. B. Jackson",
  month="September",
  location="Edinburgh, Scotland, UK"}


@techreport{Stevenson:TPHOLs00,
   author="A. Stevenson and L. A. Dennis", 
   title="Integrating {SVC} and {HOL} with the {\sc Prosper} Toolkit",
   booktitle="Theorem Proving in Higher Order Logics (TPHOLs2000), Supplemental Proceedings", 
   year=2000,
   pages="199--206",
   instituion="Oregon Graduate Institue",
   number="CSE00-009"}



@InProceedings{Dennis:CADE97,
  author =	 "L. A. Dennis and A. Bundy and I. Green",
  title =	 "Using a generalisation critic to find bisimulations
                  for coinductive proofs",
  booktitle =	 "Automated Deduction (CADE-14)",
  pages =	 "276--290",
  series = "Lecture Notes in Artificial Intelligence",
  number = 1249,
  year = 1997,
  publisher = "Springer-Verlag",
  editor = "W. McCune"
}


@inproceedings{Dennis:TACAS00,
  author = {L. A. Dennis and G. Collins and M. Norrish and R. Boulton and K. Slind and G. Robinson and M. Gordon and T. Melham},
  title = {The PROSPER Toolkit},
  booktitle = {Tools and Algorithms for Constructing Systems (TACAS 2000)},
  editor = {Graf, S. and Schwartbach, M.},
  series = {Lecture Notes in Computer Science},
  number = 1785,
  year = 2000,
  pages = {78--92},
  publisher = {Springer-Verlag}}


@InProceedings{Collins:CADE00,
  author =	 "G. Collins and L. A. Dennis",
  title =	 "System Description: Embedding Verification into Microsoft Excel",
  booktitle =	 "Automated Deduction (CADE-17)",
  pages =	 "497--501",
  series = "Lecture Notes in Artificial Intelligence",
  number = 1831,
  year = 2000,
  publisher = "Springer-Verlag",
  editor = "D. McAllester"
}


@PhDThesis(Dennis:Thesis,
   author = "Dennis, L. A.",
   title = "Proof Planning Coinduction",
   school = "Edinburgh University",
   year = 1998)


@MScThesis(Dennis:MSc,
  author="L. A. Dennis",
 title="An Exploration of Semantic Resolution",
  year=1994,
  institution="Department of Artificial Intelligence, University of Edinburgh")


Last modified: Tue Jun 7 13:21:38 BST 2011