pubs.bib

@InProceedings{Cardoso20d,
author="Cardoso, Rafael C.
and Ferrando, Angelo
and Papacchini, Fabio",
title="LFC: Combining Autonomous Agents and Automated Planning in the Multi-Agent Programming Contest",
booktitle="The Multi-Agent Programming Contest 2019",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="31--58",
isbn="978-3-030-59299-8",
note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}
}

@InProceedings{10.1007/978-3-030-54994-7_16,
author="Alves, Gleifer Vaz
and Dennis, Louise
and Fisher, Michael",
editor="Sekerinski, Emil
and Moreira, Nelma
and Oliveira, Jos{\'e} N.
and Ratiu, Daniel
and Guidotti, Riccardo
and Farrell, Marie
and Luckcuck, Matt
and Marmsoler, Diego
and Campos, Jos{\'e}
and Astarte, Troy
and Gonnord, Laure
and Cerone, Antonio
and Couto, Luis
and Dongol, Brijesh
and Kutrib, Martin
and Monteiro, Pedro
and Delmas, David",
title="Formalisation and Implementation of Road Junction Rules on an Autonomous Vehicle Modelled as an Agent",
booktitle="Formal Methods. FM 2019 International Workshops",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="217--232",
abstract="The design of autonomous vehicles includes obstacle detection and avoidance, route planning, speed control, etc. However, there is a lack of an explicitely representation of the rules of the road on an autonomous vehicle. Additionally, it is necessary to understand the behaviour of an autonomous vehicle in order to check whether or not it works according to the rules of the road. Here, we propose an agent-based architecture to embed the rules of the road into an agent representing the behaviour of an autonomous vehicle. We use temporal logic to formally represent the rules of the road in a way it should be possible to capture when and how a given rule of the road can be applied. Our contributions include: i. suggestion of changes in the rules of the road; ii. representation of rules in a suitable way for an autonomous vehicle agent; iii. dealing with indeterminate terms in the Highway Code.",
isbn="978-3-030-54994-7",
note = {[<span class="va">Verifiable Autonomy</span>]}
}

@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}}
  
@inproceedings{cardosoime,
  author = {Rafael C. Cardoso and 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},
  note = {[<span class="rain">RAIN</span>]}
}

@inproceedings{alvesime,
  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{Stringer20a,
  author    = {Stringer, P. and Cardoso, R. C. and Huang, X. and Dennis, L. A.},
  title     = {Adaptable and Verifiable BDI Reasoning},
  booktitle = {Workshop on Agents and Robots for reliable Engineered Autonomy (AREA)},
  year      = {2020},
  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}
}

@unpublished{Cardoso20c,
  author    = {Cardoso, R. C. and Farrell, M. and Kourtis, G. and Webster, M. and Dennis, L. A. and Dixon, C. and Fisher, M. and Lisitsa, A.},
  title     = {Verification and Validation for Space Robotics},
  year      = {2020},
  note = {Poster presented at the Opportunities and Challenges in Space Robotics Workshop held with ICRA 2020. [<span class="fs">FAIR-SPACE</span>]}
}

@inproceedings{Ferrando20a,
  author    = {Ferrando, A. and Cardoso, R. C. and Fisher, M. and Ancona, D. and Franceschini, L. and Mascardi, V.},
  title     = {ROSMonitoring: a Runtime Verification Framework for ROS},
  booktitle = {Towards Autonomous Robotic Systems Conference (TAROS)},
  year      = {2020},
  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}
}

@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},
  pages={1011-1026},
  doi={10.1109/JPROC.2020.2991262},
  note = {[<span class="va">Verifiable Autonomy</span>, <span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]},
year=2020}

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

@inproceedings{Cardoso20b,
  author    = {Cardoso, R. C. and Ferrando, A. and Dennis, L. A. and Fisher, M.},
  title     = {An Interface for Programming Verifiable Autonomous Agents in ROS},
  booktitle = {European Conference on Multi-Agent Systems (EUMAS)},
  year      = {2020},
  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}
}

@inproceedings{Cardoso20a,
  author    = {Cardoso, R. C. and Farrell, M. and Luckcuck, M. and Ferrando, A. and Fisher, M.},
  title     = {Heterogeneous Verification of an Autonomous Curiosity Rover},
  booktitle = {NASA Formal Methods Symposium (NFM)},
  year      = {2020},
  note = {[<span class="fs">FAIR-SPACE</span>]}
}

@incollection{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"
}

@article{Linker2019b,
  author    = {Mario Gleirscher and
               Anne E. Haxthausen and
               Martin Leucker and
               Sven Linker},
  title     = {Analysis of Autonomous Mobile Collectives in Complex Physical Environments
               (Dagstuhl Seminar 19432)},
  journal   = {Dagstuhl Reports},
  volume    = {9},
  number    = {10},
  pages     = {95--116},
  year      = {2019},
  url       = {https://doi.org/10.4230/DagRep.9.10.95},
  doi       = {10.4230/DagRep.9.10.95},
  note = {[<span class="s4">S4</span>]}
}

@article{Linker2019a,
author = {Sven Linker and Michele Sevegnani},
title = {Target counting with Presburger constraints and its application in sensor networks},
journal = {Proceedings of the Royal Society A},
volume = {475},
number = {2231},
year = {2019},
url = {https://doi.org/10.1098/rspa.2019.0278},
doi = {10.1098/rspa.2019.0278},
  note = {[<span class="s4">S4</span>]}
}

@inproceedings{Farrell2019b,
  author    = {Farrell, M. and Cardoso, R. C. and Dennis, L. and Dixon, C. and Fisher, M. and Kourtis, G. and Lisitsa, A. and Luckcuck, M. and Webster, M},
  title     = {Modular Verification of Autonomous Space Robotics},
  booktitle = {Assurance of Autonomy for Robotic Space Missions Workshop},
  year      = {2019},
  note = {[<span class="fs">FAIR-SPACE</span>]}
}

@InProceedings{Farrell2019,
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",
note = {[<span class="fs">FAIR-SPACE</span>]}
}

@InProceedings{Luckcuck2019Summary,
author="Luckcuck, Matt and Farrell, Marie and Dennis, Louise A. and Dixon, Clare and Fisher, Michael",
editor="Ahrendt, Wolfgang and Tapia Tarifa, Silvia Lizeth",
title="A Summary of Formal Specification and Verification of Autonomous Robotic Systems",
booktitle="Integrated Formal Methods",
year="2019",
publisher="Springer International Publishing",
address="Cham",
doi = {10.1007/978-3-030-34968-4_33},
pages="538--541",
abstract="Autonomous robotic systems are complex, hybrid, and often safety-critical; this makes their formal specification and verification uniquely challenging. Though commonly used, testing and simulation alone are insufficient to ensure the correctness of, or provide sufficient evidence for the certification of, autonomous robotics. Formal methods for autonomous robotics have received some attention in the literature, but no resource provides a current overview. This short paper summarises the contributions published in [5], which surveys the state-of-the-art in formal specification and verification for autonomous robotics.",
isbn="978-3-030-34968-4",
note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}
}

@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},
note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="orca">ORCA</span>]}
}

@inproceedings{ZhaoRFD0W19,
  author    = {Xingyu Zhao and
               Valentin Robu and
               David Flynn and
               Fateme Dinmohammadi and
               Michael Fisher and
               Matt Webster},
  title     = {Probabilistic Model Checking of Robots Deployed in Extreme Environments},
  booktitle = {Proc. 23rd {AAAI} Conference on Artificial Intelligence},
  pages     = {8066--8074},
  year      = {2019},
  publisher = {{AAAI} Press},
  url       = {https://www.aaai.org/Library/AAAI/aaai19contents.php},
  note = {[<span class="orca">ORCA</span>]}
}

@InProceedings{Page19ICAS,
  author    = {Page, Vincent and Webster, Matt and Fisher, Michael and Jump, Mike},
  title     = {Towards a {Methodology} to {Test} {UAVs} in {Hazardous} {Environments}},
  booktitle = {ICAS 2019, The Fifteenth International Conference on Autonomic and Autonomous Systems},
  year      = {2019},
  pages     = {38--45},
  month     = jun,
  isbn      = {978-1-61208-712-2},
  url       = {http://www.thinkmind.org/index.php?view=article&articleid=icas_2019_3_20_28007},
  urldate   = {2019-06-12},
}

@inproceedings{Koeman19EMAS,
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",
  note = {[<span class="orca">ORCA</span>, <span class="va">Verifiable Autonomy</span>]}
}

@inproceedings{Cardoso19EMAS,
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",
  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}
}
@inproceedings{Ferrando19EMAS,
  author    = {Angelo Ferrando and Michael Winikoff and Stephen Cranefield and Frank Dignum and Viviana Mascardi},
  title     = {On Enactability of Agent Interaction Protocols: Towards a Unified Approach},
  booktitle = {Proc. of the 7th International Workshop on Engineering Multi-Agent Systems (EMAS)},
  year      = {2019},
  note = {[<span class="orca">ORCA</span>, <span class="rain">RAIN</span>]}
}

@ARTICLE{BremnerDFW19,
author={P. {Bremner} and L. A. {Dennis} and M. {Fisher} and A. F. {Winfield}},
journal={Proceedings of the IEEE},
title={On Proactive, Transparent, and Verifiable Ethical Reasoning for Robots},
year={2019},
volume={},
number={},
pages={1-21},
keywords={Robots;Cognition;Ethics;Predictive models;Safety;Standards;Computer architecture;Ethics;formal verification;intelligent robots;software architecture.},
doi={10.1109/JPROC.2019.2898267},
ISSN={0018-9219},
month={},
note = {[<span  class="va">Verifiable Autonomy</span>]}}

@inproceedings{Cardoso19AAMAS,
  author    = {Rafael C. Cardoso and Rafael H. Bordini},
  title     = {Decentralised Planning for Multi-Agent Programming Platforms},
  booktitle = {Proc. of the 18th International Conference on Autonomous Agents and MultiAgent Systems (AAMAS)},
  year      = {2019},
  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}
}

@inproceedings{NalonHD18,
author = {Cl\'audia Nalon and Ullrich Hustadt and Clare Dixon},
title = "{KSP A Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments}",
journal = {Journal of Automated Reasoning},
year = {2018},
  volume    = {},
publisher = {Springer},
note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}
}

@article{WebsterBDFM18,
  author    =  {Matthew Webster and Michael Breza and Clare Dixon and Michael Fisher and Julie McCann},
  title     = {Formal Verification of Synchronisation, Gossip and Environmental Effects for Wireless Sensor Networks},
  journal   = {Electronic Communications of the EASST},
  volume    = {},
  year      = {2018},
  note = {[<span class="fs">FAIR-SPACE</span>, <span class="orca">ORCA</span>, <span class="rain">RAIN</span>]}
}

@article{CalderDFM18,
  author    = {Muffy Calder and
               Simon Dobson and
               Michael Fisher and
               Julie A. McCann},
  title     = "{Making Sense of the World: Framing Models for Trustworthy Sensor-Driven
               Systems}",
  journal   = {Computers},
  volume    = {7},
  number    = {4},
  pages     = {62},
  year      = {2018},
  doi       = {10.3390/computers7040062},
  note = {[<span class="s4">S4</span>]}
}

@inproceedings{HustadtEtAl:PAAR2018,
author = {Ullrich Hustadt and Cl\'audia Nalon and Clare Dixon},
title = "{Evaluating Pre-Processing Techniques for the Separated Normal Form for Temporal Logics}",
booktitle = {Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning (PAAR)},
year = {2018},
pages = {34--48},
editor = {Boris Konev and Josef Urban and Philipp R\"ummer},
number = 2162,
series = {CEUR Workshop Proceedings},
address = {Aachen},
issn = {1613-0073},
url = {http://ceur-ws.org/Vol-2162/#paper-04},
venue = {Oxford, UK},
eventdate = {2018-07-19},
note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>]}
}

@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,
  url = {http://www.comp.hkbu.edu.hk/~cib/2018/Aug/article2/iib_vol19no1_article2.pdf},
  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="va">Verifiable Autonomy</span>]}
}

@InProceedings{Ferrando:RV18,
   author = {Angelo Ferrando and Louise A. Dennis and Davide Ancona and Michael Fisher and Viviana Mascardi},
    title = "{Verifying and Validating Autonomous Systems: an Integrated Approach}",
booktitle = {Proc. 8th IEEE International Conference on Runtime
                  Verification (RV)},
year = {2018},
note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="va">Verifiable Autonomy</span>]}
}

@inproceedings{FarrellLF:IFM018,
  author    = {Marie Farrell and Matt Luckcuck and Michael Fisher},
  editor    = {Carlo A. Furia and Kirsten Winter},
  title     = {Robotics and Integrated Formal Methods: Necessity Meets Opportunity},
  booktitle = {Proc. 14th International Conference on Integrated
               Formal Methods (iFM)},
  series    = {Lecture Notes in Computer Science},
  volume    = {11023},
  pages     = {161-171},
  publisher = {Springer},
  year      = {2018},
  url       = {https://doi.org/10.1007/978-3-319-98938-9_10},
  doi       = {10.1007/978-3-319-98938-9_10},
  biburl    = {https://dblp.org/rec/bib/conf/ifm/FarrellL018},
note = {[<span class="fs">FAIR-SPACE</span>, <span class="orca">ORCA</span>, <span class="rain">RAIN</span>]}
}

@inproceedings{AlShareefiLD:ABZ18,
  author    = {Farah Al{-}Shareefi and
               Alexei Lisitsa and Clare Dixon},
  editor    = {Michael J. Butler and
               Alexander Raschke and
               Thai Son Hoang and
               Klaus Reichl},
  title     = "{Clarification of Ambiguity for the Simple Authentication
                and Security  Layer}",
  booktitle = {Proc. 6th International Conference on Abstract
               State Machines, Alloy, B, TLA, VDM, and {Z} (ABZ)},
  series    = {Lecture Notes in Computer Science},
  volume    = {10817},
  pages     = {189-203},
  publisher = {Springer},
  year      = {2018},
  url       = {https://doi.org/10.1007/978-3-319-91271-4\_13},
  doi       = {10.1007/978-3-319-91271-4\_13},
  biburl    = {https://dblp.org/rec/bib/conf/asm/Al-ShareefiLD18},
  note = {[<span class="fs">FAIR-SPACE</span>]}
}

@InProceedings{Fisher:WoSoCer18,
   author = {Michael Fisher and Emily Collins and Louise A. Dennis and Matt Luckcuck and Matthew Webster and Michael Jump and Vincent Page and Charles Patchett and Fateme Dinmohammadi
            and David Flynn and Valentin Robu and Xingu Zhao},
    title = "{Verifiable Self-Certifying Autonomous Systems}",
booktitle = {Proc. 8th IEEE International Workshop on Software Certification (WoSoCer)},
year = {2018},
address = {Memphis, USA},
note = {[<span class="orca">ORCA</span>]}
}

@INPROCEEDINGS{Dinmohammadi:PHM18,
author={Fateme Dinmohammadi and David Flynn and Michael Fisher and Michael Jump and Vincent Page and Valentin Robu and Charles Patchett and Wenshuo Tang and Matthew Webster},
booktitle={Proc. Prognostics and System Health Management
     Conference (PHM-Chongqing)},
title="{Certification of Safe and Trusted Robotic Inspection of Assets}",
year={2018},
volume={},
number={},
address = {Chongqing, China},
pages={},
publisher = {IEEE},
note = {[<span class="orca">ORCA</span>]}
}

@InProceedings{WinikoffDF:EMAS18,
   author = {Michael Winikoff and Louise A. Dennis and Michael Fisher},
   title = "{Slicing Agent Programs for more Efficient Verification}",
booktitle = {Proc. 6th International Workshop in Engineering Multi-Agent Systems},
year = {2019},
volume={11375},
pages={139-157},
editor={D. Weyns and V. Mascardi and A. Ricci},
series={Lecture Notes in Computer Science},
address = {Stockholm, Sweden},
note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="va">Verifiable Autonomy</span>]}
}

@inproceedings{FerrandoDA0M18,
  author    = {Angelo Ferrando and Louise A. Dennis and Davide Ancona and Michael Fisher and Viviana Mascardi},
  title     = "{Recognising Assumption Violations in Autonomous Systems Verification}",
  booktitle = {Proc. 17th International Conference on Autonomous Agents
               and MultiAgent Systems (AAMAS)},
  pages     = {1933--1935},
  year      = {2018},
  publisher = {IFAAMAS/ACM},
  url       = {http://dl.acm.org/citation.cfm?id=3238028},
  timestamp = {Mon, 16 Jul 2018 09:21:17 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/atal/FerrandoDA0M18},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="fs">FAIR-SPACE</span>, <span class="rain">RAIN</span>, <span class="va">Verifiable Autonomy</span>]}
}

@inproceedings{KamaliLF:FTSCS18,
  author    = {Maryam Kamali and Sven Linker and Michael Fisher},
  title     = "{Modular Verification of Vehicle Platooning with Respect to Decisions,
               Space and Time}",
  booktitle = {Workshop on Formal Techniques for Safety-Critical Systems (FTSCS)},
  year      = {2018},
  url       = {http://arxiv.org/abs/1804.06647},
  note = {[<span class="fs">FAIR-SPACE</span>,<span class="s4">S4</span>,<span class="va">Verifiable Autonomy</span>]}
}

@InProceedings{8539217,
  author    = {Michael Fisher and Emily Collins and Louise A. Dennis and Matt Luckcuck and Matthew Webster and Michael Jump and Vincent Page and Charles Patchett and Fateme Dinmohammadi
            and David Flynn and Valentin Robu and Xingu Zhao},
  title     = {Verifiable Self-Certifying Autonomous Systems},
  booktitle = {2018 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW)},
  year      = {2018},
  pages     = {341-348},
  month     = {Oct},
  doi       = {10.1109/ISSREW.2018.00028},
  note = {[<span class="orca">ORCA</span>]}
}

@inproceedings{DBLP:conf/icfem/GainerLDH018,
  author    = {Paul Gainer and
               Sven Linker and
               Clare Dixon and
               Ullrich Hustadt and
               Michael Fisher},
  title     = {The Power of Synchronisation: Formal Analysis of Power Consumption
               in Networks of Pulse-Coupled Oscillators},
  booktitle = {Formal Methods and Software Engineering - 20th International Conference
               on Formal Engineering Methods, {ICFEM} 2018, Gold Coast, QLD, Australia,
               November 12-16, 2018, Proceedings},
  pages     = {160--176},
  year      = {2018},
  crossref  = {DBLP:conf/icfem/2018},
  url       = {https://doi.org/10.1007/978-3-030-02450-5\_10},
  doi       = {10.1007/978-3-030-02450-5\_10},
  timestamp = {Mon, 05 Nov 2018 11:04:23 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/icfem/GainerLDH018},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="s4">S4</span>]}
}



@article{DBLP:journals/corr/abs-1809-10655,
  author    = {Paul Gainer and
               Sven Linker and
               Clare Dixon and
               Ullrich Hustadt and
               Michael Fisher},
  title     = {Multi-Scale Verification of Distributed Synchronisation},
  journal   = {CoRR},
  volume    = {abs/1809.10655},
  year      = {2018},
  url       = {http://arxiv.org/abs/1809.10655},
  archivePrefix = {arXiv},
  eprint    = {1809.10655},
  timestamp = {Fri, 05 Oct 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1809-10655},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="s4">S4</span>]}
}

@inproceedings{DBLP:conf/cade/HustadtOD17,
  author    = {Ullrich Hustadt and
               Ana Ozaki and
               Clare Dixon},
  title     = {Theorem Proving for Metric Temporal Logic over the Naturals},
  booktitle = {Automated Deduction - {CADE} 26 - 26th International Conference on
               Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings},
  pages     = {326--343},
  year      = {2017},
  crossref  = {DBLP:conf/cade/2017},
  url       = {https://doi.org/10.1007/978-3-319-63046-5\_20},
  doi       = {10.1007/978-3-319-63046-5\_20},
  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/cade/HustadtOD17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/fmics/GainerDDFHSW17,
  author    = {Paul Gainer and
               Clare Dixon and
               Kerstin Dautenhahn and
               Michael Fisher and
               Ullrich Hustadt and
               Joe Saunders and
               Matt Webster},
  title     = {CRutoN: Automatic Verification of a Robotic Assistant's Behaviours},
  booktitle = {Critical Systems: Formal Methods and Automated Verification - Joint
               22nd International Workshop on Formal Methods for Industrial Critical
               Systems - and - 17th International Workshop on Automated Verification
               of Critical Systems, FMICS-AVoCS 2017, Turin, Italy, September 18-20,
               2017, Proceedings},
  pages     = {119--133},
  year      = {2017},
  crossref  = {DBLP:conf/fmics/2017},
  url       = {https://doi.org/10.1007/978-3-319-67113-0\_8},
  doi       = {10.1007/978-3-319-67113-0\_8},
  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/fmics/GainerDDFHSW17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/ijcai/NalonHD17,
  author    = {Cl{\'{a}}udia Nalon and
               Ullrich Hustadt and
               Clare Dixon},
  title     = {{KSP:} {A} Resolution-based Prover for Multimodal K, Abridged Report},
  booktitle = {Proceedings of the Twenty-Sixth International Joint Conference on
               Artificial Intelligence, {IJCAI} 2017, Melbourne, Australia, August
               19-25, 2017},
  pages     = {4919--4923},
  year      = {2017},
  crossref  = {DBLP:conf/ijcai/2017},
  url       = {https://doi.org/10.24963/ijcai.2017/694},
  doi       = {10.24963/ijcai.2017/694},
  timestamp = {Wed, 27 Jun 2018 12:24:11 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/ijcai/NalonHD17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/qest/GainerLDHF17,
  author    = {Paul Gainer and
               Sven Linker and
               Clare Dixon and
               Ullrich Hustadt and
               Michael Fisher},
  title     = {Investigating Parametric Influence on Discrete Synchronisation Protocols
               Using Quantitative Model Checking},
  booktitle = {Quantitative Evaluation of Systems - 14th International Conference,
               {QEST} 2017, Berlin, Germany, September 5-7, 2017, Proceedings},
  pages     = {224--239},
  year      = {2017},
  crossref  = {DBLP:conf/qest/2017},
  url       = {https://doi.org/10.1007/978-3-319-66335-7\_14},
  doi       = {10.1007/978-3-319-66335-7\_14},
  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/qest/GainerLDHF17},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="s4">S4</span>]}
}

@inproceedings{DBLP:conf/sbmf/Al-ShareefiLD17,
  author    = {Farah Al{-}Shareefi and
               Alexei Lisitsa and
               Clare Dixon},
  title     = {Abstract State Machines and System Theoretic Process Analysis for
               Safety-Critical Systems},
  booktitle = {Formal Methods: Foundations and Applications - 20th Brazilian Symposium,
               {SBMF} 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings},
  pages     = {15--32},
  year      = {2017},
  crossref  = {DBLP:conf/sbmf/2017},
  url       = {https://doi.org/10.1007/978-3-319-70848-5\_3},
  doi       = {10.1007/978-3-319-70848-5\_3},
  timestamp = {Fri, 17 Nov 2017 14:28:29 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/sbmf/Al-ShareefiLD17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/frocos/2017,
  editor    = {Clare Dixon and
               Marcelo Finger},
  title     = {Frontiers of Combining Systems - 11th International Symposium, FroCoS
               2017, Bras{\'{\i}}lia, Brazil, September 27-29, 2017, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {10483},
  publisher = {Springer},
  year      = {2017},
  url       = {https://doi.org/10.1007/978-3-319-66167-4},
  doi       = {10.1007/978-3-319-66167-4},
  isbn      = {978-3-319-66166-7},
  timestamp = {Tue, 05 Sep 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/frocos/2017},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/corr/abs-1709-04385,
  author    = {Paul Gainer and
               Sven Linker and
               Clare Dixon and
               Ullrich Hustadt and
               Michael Fisher},
  title     = {The Power of Synchronisation: Formal Analysis of Power Consumption
               in Networks of Pulse-Coupled Oscillators},
  journal   = {CoRR},
  volume    = {abs/1709.04385},
  year      = {2017},
  url       = {http://arxiv.org/abs/1709.04385},
  archivePrefix = {arXiv},
  eprint    = {1709.04385},
  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1709-04385},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="s4">S4</span>]}
}

@article{DBLP:journals/thms/WebsterDFSSKDS16,
  author    = {Matt Webster and
               Clare Dixon and
               Michael Fisher and
               Maha Salem and
               Joe Saunders and
               Kheng Lee Koay and
               Kerstin Dautenhahn and
               Joan Saez{-}Pons},
  title     = {Toward Reliable Autonomous Robotic Assistants Through Formal Verification:
               {A} Case Study},
  journal   = {{IEEE} Trans. Human-Machine Systems},
  volume    = {46},
  number    = {2},
  pages     = {186--196},
  year      = {2016},
  url       = {https://doi.org/10.1109/THMS.2015.2425139},
  doi       = {10.1109/THMS.2015.2425139},
  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/thms/WebsterDFSSKDS16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/NalonHD16,
  author    = {Cl{\'{a}}udia Nalon and
               Ullrich Hustadt and
               Clare Dixon},
  title     = {: {A} Resolution-Based Prover for Multimodal {K}},
  booktitle = {Automated Reasoning - 8th International Joint Conference, {IJCAR}
               2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},
  pages     = {406--415},
  year      = {2016},
  crossref  = {DBLP:conf/cade/2016},
  url       = {https://doi.org/10.1007/978-3-319-40229-1\_28},
  doi       = {10.1007/978-3-319-40229-1\_28},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/NalonHD16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/taros/GainerDH16,
  author    = {Paul Gainer and
               Clare Dixon and
               Ullrich Hustadt},
  title     = {Probabilistic Model Checking of Ant-Based Positionless Swarming},
  booktitle = {Towards Autonomous Robotic Systems - 17th Annual Conference, {TAROS}
               2016, Sheffield, UK, June 26 - July 1, 2016, Proceedings},
  pages     = {127--138},
  year      = {2016},
  crossref  = {DBLP:conf/taros/2016},
  url       = {https://doi.org/10.1007/978-3-319-40379-3\_13},
  doi       = {10.1007/978-3-319-40379-3\_13},
  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/taros/GainerDH16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/corr/WebsterWADEFP16,
  author    = {Matt Webster and
               David Western and
               Dejanira Araiza{-}Illan and
               Clare Dixon and
               Kerstin Eder and
               Michael Fisher and
               Anthony G. Pipe},
  title     = {An Assurance-based Approach to Verification and Validation of Human-Robot
               Teams},
  journal   = {CoRR},
  volume    = {abs/1608.07403},
  year      = {2016},
  url       = {http://arxiv.org/abs/1608.07403},
  archivePrefix = {arXiv},
  eprint    = {1608.07403},
  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/WebsterWADEFP16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/eswa/El-SalhiCDK15,
  author    = {Subhieh El{-}Salhi and
               Frans Coenen and
               Clare Dixon and
               M. Sulaiman Khan},
  title     = {Predicting "springback" using 3D surface representation techniques:
               {A} case study in sheet metal forming},
  journal   = {Expert Syst. Appl.},
  volume    = {42},
  number    = {1},
  pages     = {79--93},
  year      = {2015},
  url       = {https://doi.org/10.1016/j.eswa.2014.07.041},
  doi       = {10.1016/j.eswa.2014.07.041},
  timestamp = {Fri, 26 May 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/eswa/El-SalhiCDK15},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/tableaux/HustadtGDNZ15,
  author    = {Ullrich Hustadt and
               Paul Gainer and
               Clare Dixon and
               Cl{\'{a}}udia Nalon and
               Lan Zhang},
  title     = {Ordered Resolution for Coalition Logic},
  booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods - 24th
               International Conference, {TABLEAUX} 2015, Wroc{\l}aw, Poland, September
               21-24, 2015. Proceedings},
  pages     = {169--184},
  year      = {2015},
  crossref  = {DBLP:conf/tableaux/2015},
  url       = {https://doi.org/10.1007/978-3-319-24312-2\_12},
  doi       = {10.1007/978-3-319-24312-2\_12},
  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/tableaux/HustadtGDNZ15},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/tableaux/NalonHD15,
  author    = {Cl{\'{a}}udia Nalon and
               Ullrich Hustadt and
               Clare Dixon},
  title     = {A Modal-Layered Resolution Calculus for {K}},
  booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods - 24th
               International Conference, {TABLEAUX} 2015, Wroc{\l}aw, Poland, September
               21-24, 2015. Proceedings},
  pages     = {185--200},
  year      = {2015},
  crossref  = {DBLP:conf/tableaux/2015},
  url       = {https://doi.org/10.1007/978-3-319-24312-2\_13},
  doi       = {10.1007/978-3-319-24312-2\_13},
  timestamp = {Thu, 15 Jun 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/tableaux/NalonHD15},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/taros/2015,
  editor    = {Clare Dixon and
               Karl Tuyls},
  title     = {Towards Autonomous Robotic Systems - 16th Annual Conference, {TAROS}
               2015, Liverpool, UK, September 8-10, 2015, Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {9287},
  publisher = {Springer},
  year      = {2015},
  url       = {https://doi.org/10.1007/978-3-319-22416-9},
  doi       = {10.1007/978-3-319-22416-9},
  isbn      = {978-3-319-22415-2},
  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/taros/2015},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/logcom/NalonZDH14,
  author    = {Cl{\'{a}}udia Nalon and
               Lan Zhang and
               Clare Dixon and
               Ullrich Hustadt},
  title     = {A resolution-based calculus for Coalition Logic},
  journal   = {J. Log. Comput.},
  volume    = {24},
  number    = {4},
  pages     = {883--917},
  year      = {2014},
  url       = {https://doi.org/10.1093/logcom/ext074},
  doi       = {10.1093/logcom/ext074},
  timestamp = {Wed, 17 May 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/logcom/NalonZDH14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/tocl/ZhangHD14,
  author    = {Lan Zhang and
               Ullrich Hustadt and
               Clare Dixon},
  title     = {A resolution calculus for the branching-time temporal logic {CTL}},
  journal   = {{ACM} Trans. Comput. Log.},
  volume    = {15},
  number    = {1},
  pages     = {10:1--10:38},
  year      = {2014},
  url       = {https://doi.org/10.1145/2529993},
  doi       = {10.1145/2529993},
  timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/tocl/ZhangHD14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/aaaiss/WebsterD0SSKD14,
  author    = {Matt Webster and
               Clare Dixon and
               Michael Fisher and
               Maha Salem and
               Joe Saunders and
               Kheng Lee Koay and
               Kerstin Dautenhahn},
  title     = {Formal Verification of an Autonomous Personal Robotic Assistant},
  booktitle = {2014 {AAAI} Spring Symposia, Stanford University, Palo Alto, California,
               USA, March 24-26, 2014},
  year      = {2014},
  crossref  = {DBLP:conf/aaaiss/2014},
  url       = {http://www.aaai.org/ocs/index.php/SSS/SSS14/paper/view/7734},
  timestamp = {Wed, 14 Nov 2018 14:23:12 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/aaaiss/WebsterD0SSKD14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/NalonMD14,
  author    = {Cl{\'{a}}udia Nalon and
               Jo{\~{a}}o Marcos and
               Clare Dixon},
  title     = {Clausal Resolution for Modal Logics of Confluence},
  booktitle = {Automated Reasoning - 7th International Joint Conference, {IJCAR}
               2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
               Austria, July 19-22, 2014. Proceedings},
  pages     = {322--336},
  year      = {2014},
  crossref  = {DBLP:conf/cade/2014},
  url       = {https://doi.org/10.1007/978-3-319-08587-6\_24},
  doi       = {10.1007/978-3-319-08587-6\_24},
  timestamp = {Sun, 21 May 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/cade/NalonMD14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/taros/DixonWSFD14,
  author    = {Clare Dixon and
               Matthew P. Webster and
               Joe Saunders and
               Michael Fisher and
               Kerstin Dautenhahn},
  title     = {"The Fridge Door is Open"-Temporal Verification of a Robotic Assistant's
               Behaviours},
  booktitle = {Advances in Autonomous Robotics Systems - 15th Annual Conference,
               {TAROS} 2014, Birmingham, UK, September 1-3, 2014. Proceedings},
  pages     = {97--108},
  year      = {2014},
  crossref  = {DBLP:conf/taros/2014},
  url       = {https://doi.org/10.1007/978-3-319-10401-0\_9},
  doi       = {10.1007/978-3-319-10401-0\_9},
  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/taros/DixonWSFD14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:journals/corr/NalonZDH14,
  author    = {Cl{\'{a}}udia Nalon and
               Lan Zhang and
               Clare Dixon and
               Ullrich Hustadt},
  title     = {A Resolution Prover for Coalition Logic},
  booktitle = {Proceedings 2nd International Workshop on Strategic Reasoning, {SR}
               2014, Grenoble, France, April 5-6, 2014.},
  pages     = {65--73},
  year      = {2014},
  crossref  = {DBLP:journals/corr/MogaveroMV14},
  url       = {https://doi.org/10.4204/EPTCS.146.9},
  doi       = {10.4204/EPTCS.146.9},
  timestamp = {Wed, 12 Sep 2018 01:05:14 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/NalonZDH14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@incollection{DBLP:conf/birthday/DixonF14,
  author    = {Clare Dixon and
               Michael Fisher},
  title     = {On and On the Temporal Way},
  booktitle = {{HOWARD-60:} {A} Festschrift on the Occasion of Howard Barringer's
               60th Birthday},
  pages     = {85--111},
  year      = {2014},
  crossref  = {DBLP:conf/birthday/2014howard},
  url       = {http://www.easychair.org/publications/?page=2015413951},
  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/birthday/DixonF14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/corr/NalonMD14,
  author    = {Cl{\'{a}}udia Nalon and
               Jo{\~{a}}o Marcos and
               Clare Dixon},
  title     = {Clausal Resolution for Modal Logics of Confluence},
  journal   = {CoRR},
  volume    = {abs/1405.0293},
  year      = {2014},
  url       = {http://arxiv.org/abs/1405.0293},
  archivePrefix = {arXiv},
  eprint    = {1405.0293},
  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/NalonMD14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/jossw/Dennis18,
  author    = {Louise A. Dennis},
  title     = {The {MCAPL} Framework including the Agent Infrastructure Layer an
               Agent Java Pathfinder},
  journal   = {J. Open Source Software},
  volume    = {3},
  number    = {24},
  pages     = {617},
  year      = {2018},
  url       = {https://doi.org/10.21105/joss.00617},
  doi       = {10.21105/joss.00617},
  timestamp = {Tue, 13 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/jossw/Dennis18},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/logcom/Dennis0W18,
  author    = {Louise A. Dennis and
               Michael Fisher and
               Matt Webster},
  title     = {Two-stage agent program verification},
  journal   = {J. Log. Comput.},
  volume    = {28},
  number    = {3},
  pages     = {499--523},
  year      = {2018},
  url       = {https://doi.org/10.1093/logcom/exv002},
  doi       = {10.1093/logcom/exv002},
  timestamp = {Mon, 07 May 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/logcom/Dennis0W18},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="va">Verifiable Autonomy</span>]}
}

@inproceedings{DBLP:conf/isaim/F18,
  author    = {Louise A. Dennis and
               Michael Fisher},
  title     = {Practical Challenges in Explicit Ethical Machine Reasoning},
  booktitle = {International Symposium on Artificial Intelligence and Mathematics,
               {ISAIM} 2018, Fort Lauderdale, Florida, USA, January 3-5, 2018.},
  year      = {2018},
  crossref  = {DBLP:conf/isaim/2018},
  url       = {http://isaim2018.cs.virginia.edu/papers/ISAIM2018\_Ethics\_Dennis\_Fischer.pdf},
  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/isaim/DennisF18},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="va">Verifiable Autonomy</span>]}
}

@article{DBLP:journals/scp/KamaliDMFV17,
  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   = {Sci. Comput. Program.},
  volume    = {148},
  pages     = {88--106},
  year      = {2017},
  url       = {https://doi.org/10.1016/j.scico.2017.05.006},
  doi       = {10.1016/j.scico.2017.05.006},
  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/scp/KamaliDMFV17},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="va">Verifiable Autonomy</span>]}
}

@article{DBLP:journals/corr/CharisiDFLMSSWY17,
  author    = {Vicky Charisi and
               Louise A. Dennis and
               Michael Fisher and
               Robert Lieck and
               Andreas Matthias and
               Marija Slavkovik and
               Janina Sombetzki and
               Alan F. T. Winfield and
               Roman Yampolskiy},
  title     = {Towards Moral Autonomous Systems},
  journal   = {CoRR},
  volume    = {abs/1703.04741},
  year      = {2017},
  url       = {http://arxiv.org/abs/1703.04741},
  archivePrefix = {arXiv},
  eprint    = {1703.04741},
  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/CharisiDFLMSSWY17},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="va">Verifiable Autonomy</span>]}
}

@article{DBLP:journals/ase/DennisFLLV16,
  author    = {Louise A. Dennis and
               Michael Fisher and
               Nicholas Lincoln and
               Alexei Lisitsa and
               Sandor M. Veres},
  title     = {Practical verification of decision-making in agent-based autonomous
               systems},
  journal   = {Autom. Softw. Eng.},
  volume    = {23},
  number    = {3},
  pages     = {305--359},
  year      = {2016},
  url       = {https://doi.org/10.1007/s10515-014-0168-9},
  doi       = {10.1007/s10515-014-0168-9},
  timestamp = {Tue, 26 Jun 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/ase/DennisFLLV16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/ras/DennisFSW16,
  author    = {Louise A. Dennis and
               Michael Fisher and
               Marija Slavkovik and
               Matt Webster},
  title     = {Formal verification of ethical choices in autonomous systems},
  journal   = {Robotics and Autonomous Systems},
  volume    = {77},
  pages     = {1--14},
  year      = {2016},
  url       = {https://doi.org/10.1016/j.robot.2015.11.012},
  doi       = {10.1016/j.robot.2015.11.012},
  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/ras/DennisFSW16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/atal/DennisSF16,
  author    = {Louise A. Dennis and
               Marija Slavkovik and
               Michael Fisher},
  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},
  pages     = {42--59},
  year      = {2016},
  crossref  = {DBLP:conf/atal/2016coin},
  url       = {https://doi.org/10.1007/978-3-319-66595-5\_3},
  doi       = {10.1007/978-3-319-66595-5\_3},
  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/atal/DennisSF16},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="va">Verifiable Autonomy</span>]}
}

@inproceedings{DBLP:conf/taros/DennisACCKMSAGV16,
  author    = {Louise A. Dennis and
               Jonathan M. Aitken and
               Joe Collenette and
               Elisa Cucco and
               Maryam Kamali and
               Owen McAree and
               Affan Shaukat and
               Katie Atkinson and
               Yang Gao and
               Sandor M. Veres and
               Michael Fisher},
  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},
  pages     = {75--86},
  year      = {2016},
  crossref  = {DBLP:conf/taros/2016},
  url       = {https://doi.org/10.1007/978-3-319-40379-3\_8},
  doi       = {10.1007/978-3-319-40379-3\_8},
  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/taros/DennisACCKMSAGV16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@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},
  archivePrefix = {arXiv},
  eprint    = {1602.01718},
  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/KamaliDMFV16},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="va">Verifiable Autonomy</span>]}
}

@article{DBLP:journals/dpd/SlavkovikDF15,
  author    = {Marija Slavkovik and
               Louise A. Dennis and
               Michael Fisher},
  title     = {An abstract formal basis for digital crowds},
  journal   = {Distributed and Parallel Databases},
  volume    = {33},
  number    = {1},
  pages     = {3--31},
  year      = {2015},
  url       = {https://doi.org/10.1007/s10619-014-7161-y},
  doi       = {10.1007/s10619-014-7161-y},
  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/dpd/SlavkovikDF15},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/aaai/DennisFW15,
  author    = {Louise Abigail Dennis and
               Michael Fisher and
               Alan F. T. Winfield},
  title     = {Towards Verifiably Ethical Robot Behaviour},
  booktitle = {Artificial Intelligence and Ethics, Papers from the 2015 {AAAI} Workshop,
               Austin, Texas, USA, January 25, 2015.},
  year      = {2015},
  crossref  = {DBLP:conf/aaai/2015ethics},
  url       = {http://aaai.org/ocs/index.php/WS/AAAIW15/paper/view/10119},
  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/aaai/DennisFW15},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="va">Verifiable Autonomy</span>]}
}

@inproceedings{DBLP:conf/atal/RiemsdijkDFH15,
  author    = {M. Birna van Riemsdijk and
               Louise A. Dennis and
               Michael Fisher and
               Koen V. Hindriks},
  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, {AAMAS} 2015, Istanbul, Turkey, May 4-8, 2015},
  pages     = {423--432},
  year      = {2015},
  crossref  = {DBLP:conf/atal/2015},
  url       = {http://dl.acm.org/citation.cfm?id=2772935},
  timestamp = {Tue, 20 Feb 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/atal/RiemsdijkDFH15},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="va">Verifiable Autonomy</span>]}
}

@article{DBLP:journals/corr/DennisFW15,
  author    = {Louise A. Dennis and
               Michael Fisher and
               Alan F. T. Winfield},
  title     = {Towards Verifiably Ethical Robot Behaviour},
  journal   = {CoRR},
  volume    = {abs/1504.03592},
  year      = {2015},
  url       = {http://arxiv.org/abs/1504.03592},
  archivePrefix = {arXiv},
  eprint    = {1504.03592},
  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/DennisFW15},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="va">Verifiable Autonomy</span>]}
}

@article{DBLP:journals/ki/DennisFAVGSB14,
  author    = {Louise A. Dennis and
               Michael Fisher and
               Jonathan M. Aitken and
               Sandor M. Veres and
               Yang Gao and
               Affan Shaukat and
               Guy Burroughes},
  title     = {Reconfigurable Autonomy},
  journal   = {{KI}},
  volume    = {28},
  number    = {3},
  pages     = {199--207},
  year      = {2014},
  url       = {https://doi.org/10.1007/s13218-014-0308-1},
  doi       = {10.1007/s13218-014-0308-1},
  timestamp = {Tue, 26 Jun 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/ki/DennisFAVGSB14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/ecai/DennisF14,
  author    = {Louise A. Dennis and
               Michael Fisher},
  title     = {Actions with Durations and Failures in {BDI} Languages},
  booktitle = {{ECAI} 2014 - 21st European Conference on Artificial Intelligence,
               18-22 August 2014, Prague, Czech Republic - Including Prestigious
               Applications of Intelligent Systems {(PAIS} 2014)},
  pages     = {995--996},
  year      = {2014},
  crossref  = {DBLP:conf/ecai/2014},
  url       = {https://doi.org/10.3233/978-1-61499-419-0-995},
  doi       = {10.3233/978-1-61499-419-0-995},
  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/ecai/DennisF14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/corr/SlavkovikDF14,
  author    = {Marija Slavkovik and
               Louise A. Dennis and
               Michael Fisher},
  title     = {An Abstract Formal Basis for Digital Crowds},
  journal   = {CoRR},
  volume    = {abs/1408.1592},
  year      = {2014},
  url       = {http://arxiv.org/abs/1408.1592},
  archivePrefix = {arXiv},
  eprint    = {1408.1592},
  timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/SlavkovikDF14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/fac/KonurFDK14,
  author    = {Savas Konur and
               Michael Fisher and
               Simon Dobson and
               Stephen Knox},
  title     = {Formal verification of a pervasive messaging system},
  journal   = {Formal Asp. Comput.},
  volume    = {26},
  number    = {4},
  pages     = {677--694},
  year      = {2014},
  url       = {https://doi.org/10.1007/s00165-013-0277-4},
  doi       = {10.1007/s00165-013-0277-4},
  timestamp = {Tue, 20 Feb 2018 18:30:38 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/fac/KonurFDK14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/jacic/WebsterCFJ14,
  author    = {Matthew P. Webster and
               Neil Cameron and
               Michael Fisher and
               Mike Jump},
  title     = {Generating Certification Evidence for Autonomous Unmanned Aircraft
               Using Model Checking and Simulation},
  journal   = {J. Aerospace Inf. Sys.},
  volume    = {11},
  number    = {5},
  pages     = {258--279},
  year      = {2014},
  url       = {https://doi.org/10.2514/1.I010096},
  doi       = {10.2514/1.I010096},
  timestamp = {Fri, 02 Nov 2018 09:33:11 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/jacic/WebsterCFJ14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/logcom/FisherTDG14,
  author    = {Michael Fisher and
               Leendert W. N. van der Torre and
               Mehdi Dastani and
               Guido Governatori},
  title     = {Preface to the Special Issue on Computational Logic in Multi-Agent
               Systems {(CLIMA} {XIII)}},
  journal   = {J. Log. Comput.},
  volume    = {24},
  number    = {6},
  pages     = {1251--1252},
  year      = {2014},
  url       = {https://doi.org/10.1093/logcom/ext075},
  doi       = {10.1093/logcom/ext075},
  timestamp = {Wed, 14 Nov 2018 10:17:07 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/logcom/FisherTDG14},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/corr/abs-1803-10478,
  author    = {Muffy Calder and
               Simon Dobson and
               Michael Fisher and
               Julie A. McCann},
  title     = {Making Sense of the World: Models for Reliable Sensor-Driven Systems},
  journal   = {CoRR},
  volume    = {abs/1803.10478},
  year      = {2018},
  url       = {http://arxiv.org/abs/1803.10478},
  archivePrefix = {arXiv},
  eprint    = {1803.10478},
  timestamp = {Mon, 13 Aug 2018 16:46:50 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1803-10478},
  bibsource = {dblp computer science bibliography, https://dblp.org}
  note = {[<span class="s4">S4</span>]}
}

@article{DBLP:journals/corr/abs-1804-06647,
  author    = {Maryam Kamali and
               Sven Linker and
               Michael Fisher},
  title     = {Modular Verification of Vehicle Platooning with Respect to Decisions,
               Space and Time},
  journal   = {CoRR},
  volume    = {abs/1804.06647},
  year      = {2018},
  url       = {http://arxiv.org/abs/1804.06647},
  archivePrefix = {arXiv},
  eprint    = {1804.06647},
  timestamp = {Mon, 13 Aug 2018 16:48:43 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1804-06647},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="va">Verifiable Autonomy</span>, <span class="s4">S4</span>]}
}

@inproceedings{DBLP:journals/corr/abs-1709-02557,
  author    = {Lucas E. R. Fernandes and
               Vinicius Custodio and
               Gleifer V. Alves and
               Michael Fisher},
  title     = {A Rational Agent Controlling an Autonomous Vehicle: Implementation
               and Formal Verification},
  booktitle = {Proceedings First Workshop on Formal Verification of Autonomous Vehicles,
               FVAV@iFM 2017, Turin, Italy, 19th September 2017.},
  pages     = {35--42},
  year      = {2017},
  url       = {https://doi.org/10.4204/EPTCS.257.5},
  doi       = {10.4204/EPTCS.257.5},
  timestamp = {Fri, 02 Nov 2018 09:30:18 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1709-02557},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/corr/abs-1709-07171,
  author    = {Omar I. Al{-}Bataineh and
               Michael Fisher and
               David Rosenblum},
  title     = {Finding Maximum Expected Termination Time of Probabilistic Timed Automata
               Models with Cyclic behavior},
  journal   = {CoRR},
  volume    = {abs/1709.07171},
  year      = {2017},
  url       = {http://arxiv.org/abs/1709.07171},
  archivePrefix = {arXiv},
  eprint    = {1709.07171},
  timestamp = {Mon, 13 Aug 2018 16:48:50 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1709-07171},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/dagstuhl-reports/FisherLSW16,
  author    = {Michael Fisher and
               Christian List and
               Marija Slavkovik and
               Alan F. T. Winfield},
  title     = {Engineering Moral Agents - from Human Morality to Artificial Morality
               (Dagstuhl Seminar 16222)},
  journal   = {Dagstuhl Reports},
  volume    = {6},
  number    = {5},
  pages     = {114--137},
  year      = {2016},
  url       = {https://doi.org/10.4230/DagRep.6.5.114},
  doi       = {10.4230/DagRep.6.5.114},
  timestamp = {Tue, 20 Feb 2018 18:30:38 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/dagstuhl-reports/FisherLSW16},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/ker/KonurF15,
  author    = {Savas Konur and
               Michael Fisher},
  title     = {A roadmap to pervasive systems verification},
  journal   = {Knowledge Eng. Review},
  volume    = {30},
  number    = {3},
  pages     = {324--341},
  year      = {2015},
  url       = {https://doi.org/10.1017/S0269888914000228},
  doi       = {10.1017/S0269888914000228},
  timestamp = {Tue, 20 Feb 2018 18:30:38 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/ker/KonurF15},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}


@inproceedings{DBLP:conf/diagrams/Linker18,
  author    = {Sven Linker},
  title     = {Sequent Calculus for Euler Diagrams},
  booktitle = {Diagrammatic Representation and Inference - 10th International Conference,
               Diagrams 2018, Edinburgh, UK, June 18-22, 2018, Proceedings},
  pages     = {399--407},
  year      = {2018},
  crossref  = {DBLP:conf/diagrams/2018},
  url       = {https://doi.org/10.1007/978-3-319-91376-6\_37},
  doi       = {10.1007/978-3-319-91376-6\_37},
  timestamp = {Tue, 10 Jul 2018 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/diagrams/Linker18},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="s4">S4</span>]}
}


@article{DBLP:journals/corr/abs-1811-01774,
  author    = {Mario Gleirscher and
               Sven Linker and
               Stefan Kugele},
  title     = {SCAV'18: Report of the 2nd International Workshop on Safe Control
               of Autonomous Vehicles},
  journal   = {CoRR},
  volume    = {abs/1811.01774},
  year      = {2018},
  url       = {http://arxiv.org/abs/1811.01774},
  archivePrefix = {arXiv},
  eprint    = {1811.01774},
  timestamp = {Thu, 22 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1811-01774},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="va">Verifiable Autonomy</span>]}
}

@article{Linker17,
  author    = {Sven Linker},
  title     = {Hybrid Multi-Lane Spatial Logic},
  journal   = {Archive of Formal Proofs},
  year      = {2017},
  url       = {https://www.isa-afp.org/entries/Hybrid\_Multi\_Lane\_Spatial\_Logic.html},
  note = {[<span class="va">Verifiable Autonomy</span>, <span class="s4">S4</span>]}
}

@article{DBLP:journals/fac/BochmannHLO17,
  author    = {Gregor von Bochmann and
               Martin Hilscher and
               Sven Linker and
               Ernst{-}R{\"{u}}diger Olderog},
  title     = {Synthesizing and verifying controllers for multi-lane traffic maneuvers},
  journal   = {Formal Asp. Comput.},
  volume    = {29},
  number    = {4},
  pages     = {583--600},
  year      = {2017},
  url       = {https://doi.org/10.1007/s00165-017-0424-4},
  doi       = {10.1007/s00165-017-0424-4},
  timestamp = {Wed, 26 Jul 2017 01:00:00 +0200},
  biburl    = {https://dblp.org/rec/bib/journals/fac/BochmannHLO17},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/ifm/Linker17,
  author    = {Sven Linker},
  title     = {Spatial Reasoning About Motorway Traffic Safety with Isabelle/HOL},
  booktitle = {Integrated Formal Methods - 13th International Conference, {IFM} 2017,
               Turin, Italy, September 20-22, 2017, Proceedings},
  pages     = {34--49},
  year      = {2017},
  crossref  = {DBLP:conf/ifm/2017},
  url       = {https://doi.org/10.1007/978-3-319-66845-1\_3},
  doi       = {10.1007/978-3-319-66845-1\_3},
  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/conf/ifm/Linker17},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="va">Verifiable Autonomy</span>, <span class="s4">S4</span>]}
}

@inproceedings{DBLP:journals/corr/abs-1802-01791,
  author    = {Sven Linker and
               Michele Sevegnani},
  title     = {Formalising Sensor Topologies for Target Counting},
  booktitle = {Proceedings First Workshop on Architectures, Languages and Paradigms
               for IoT, ALP4IoT@iFM 2017, Turin, Italy, September 18, 2017.},
  pages     = {43--57},
  year      = {2017},
  crossref  = {DBLP:journals/corr/abs-1802-00976},
  url       = {https://doi.org/10.4204/EPTCS.264.5},
  doi       = {10.4204/EPTCS.264.5},
  timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
  biburl    = {https://dblp.org/rec/bib/journals/corr/abs-1802-01791},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  note = {[<span class="s4">S4</span>]}
}