Publications

Published research papers

  • An Ontology to support Knowledge Management in Behaviour-based Healthcare.
    John Kingston and Nathaniel Charlton. To appear in Proceedings of AI 2017
    (37th SGAI International Conference on Artificial Intelligence, December 2017). PDF will be available here soon.
  • Using Data Mining to Refine Digital Behaviour Change Interventions.
    Nathaniel Charlton, John Kingston, Miltos Petridis and Ben (C) Fletcher.
    To appear in Proceedings of 7th ACM Conference on Digital Health (July 2017).
    Available here.
  • Separating temporal and topological effects in walk-based network centrality. Ewan Colman and Nathaniel Charlton. In Physics Review E, Volume 94, Issue 1 (July 2016). Available here (official APS version) or as a pre-print here.
  • In the mood: the dynamics of collective sentiments on Twitter. Nathaniel Charlton, Colin Singleton and Danica Vukadinovic Greetham. In Royal Society Open Science Volume 3, Issue 6 (June 2016). Available here (official Royal Society version) and here.
  • Symbolic Execution Proofs for Higher Order Store Programs. Bernhard Reus, Nathaniel Charlton and Ben Horsfall. Long version of VMCAI conference paper detailed below. In Journal of Automated Reasoning Volume 54, Issue 3 (March 2015). Available here (official Springer version) and here.
  • Weighted alpha-rate dominating sets in social networks. Danica Vukadinovic Greetham, Anush Poghosyan and Nathaniel Charlton. In Proceedings of Complex Networks 2014 (Third International Workshop on Complex Networks and their Applications). Here (official IEEE version) and here.
  • A refined parametric model for short term load forecasting. Nathaniel Charlton and Colin Singleton. This work describes our winning entry in the GEFCom2012 load forecasting competition. In International Journal of Forecasting (Volume 30, Issue 2, April–June 2014). Here (official Springer version) and here.
  • Graph-based algorithms for comparison and prediction of household-level energy use profiles. Nathaniel Charlton, Danica Vukadinovic Greetham and Colin Singleton. In Proceedings of IWIES 2013 (International Workshop on Intelligent Energy Systems). Here (official IEEE version) and here.
  • Specification patterns and proofs for recursion through the store. Nathaniel Charlton and Bernhard Reus. Long version of FCT conference paper detailed below. In Information and Computation Volume 231, October 2013. Available here (official Springer version) and here.
  • Verifying the reflective visitor pattern. Ben Horsfall, Nathaniel Charlton and Bernhard Reus. In Proceedings of FTfJP 2012 (Formal Techniques for Java-like Programs). Here (official ACM version) and here.
  • Crowfoot: a verifier for higher-order store programs. Nathaniel Charlton, Ben Horsfall and Bernhard Reus. Here (official Springer version) and here. In Proceedings of VMCAI 2012 (Verification, Model Checking, and Abstract Interpretation), LNCS 7148.
  • Specification patterns and proofs for recursion through the store. Nathaniel Charlton and Bernhard Reus. Here (official Springer version) and here. In Proceedings of FCT 2011 (18th International Symposium on Fundamentals of Computation Theory), LNCS 6914.
  • Hoare logic for higher order store using simple semantics. Nathaniel Charlton. Here (official Springer version) and here. In Proceedings of WoLLIC 2011 (18th Workshop on Logic, Language, Information and Computation), LNCS 6642.
  • Formal Reasoning about Runtime Code Update. Nathaniel Charlton, Ben Horsfall and Bernhard Reus. Here (official IEEE version) and here. In Proceedings of HotSWUp 2011 (Hot Topics in Software Upgrades).
  • A decidable class of verification conditions for programs with higher order store. Nathaniel Charlton and Bernhard Reus. Here. In Proceedings of Automated Verification of Critical Systems 2009 (AVoCS 09), Electronic Communications of EASST, Volume 23.
  • Falsifying safety properties through games on over-approximating models. Nathaniel Charlton and Michael Huth. Here. In Proceedings of Workshop on Reachability Problems 2008 (WRP 08), ENTCS 223.
  • Hector: software model checking with cooperating analysis plugins. Nathaniel Charlton and Michael Huth. Here. In Proceedings of Computer Aided Verification 2007 (CAV 07), LNCS 4590.
  • Program Verification with Interacting Analysis Plugins. Nathaniel Charlton. Here. In Formal Aspects of Computing (Volume 19, Number 3 / August 2007). A more in-depth, earlier version of this article is available as a technical report (see below).
  • Polynomial-Time Under-Approximation of Winning Regions in Parity Games. Adam Antonik, Nathaniel Charlton and Michael Huth. Here. In Proceedings of Mathematical Foundations of Computer Science and Information Technology (MFCSIT 06), ENTCS 225.
  • Verification of Java Programs with Interacting Analysis Plugins. Nathaniel Charlton. Here. In Proceedings of Workshop on Automated Verification of Critical Systems 2005 (AVoCS 05), ENTCS 145.

Technical reports

  • Diversity and inclusiveness, wellbeing and openness to change: the effects of a Do Something Different programme in a global organisation. Nathaniel Charlton, Karen Pine and Ben (C) Fletcher. White Paper Number 5, Do Something Different Ltd, September 2016. Here or at Do Something Different.
  • On minimum cost local permutation problems and their application to smart meter data. Nathaniel Charlton, Danica Vukadinovic Greetham and Colin Singleton. Report 2/2013 in University of Reading Mathematics Report Series. Here or at University of Reading.
  • Program Verification with Interacting Analysis Plugins. Nathaniel Charlton. Technical Report 2006/11, Department of Computing, Imperial College London, ISSN 1469-4174. This is an earlier, more detailed version of the Formal Aspects of Computing paper. Available here or at Imperial College.

Unpublished manuscripts

  • Algorithms for alpha-rate domination problems on weighted graphs.
    Danica Vukadinovic Greetham, Anush Poghosyan and Nathaniel Charlton.
    Available from arXiv here.
  • Hoare logic for higher order store with simple foundations. Nathaniel Charlton. Here. (This is a longer version of the WoLLIC 2011 paper above, with further results.)
  • Reasoning about string-based runtime code generation. Nathaniel Charlton. Here.

(As I am no longer pursuing these topics, these pieces of work will probably not be formally published.)

Phd thesis

  • Cooperatively combining program verifiers: foundations and tool support. Nathaniel Charlton. Submitted August 2008 and examined September 2008. Here (Imperial College repository) and here.

Extended abstracts

  • A deeper understanding of the deep frame axiom. Nathaniel Charlton and Bernhard Reus. Here. Presented at LOLA 2010 (Syntax and Semantics of Low Level Languages).
  • Cleanly combining specialised program analysers. Nathaniel Charlton and Michael Huth. Here (Imperial College repository) and here. Presented at Automated Reasoning Workshop 2007 (ARW 07).
  • Computing safe winning regions of parity games in polynomial time. Adam Antonik, Nathaniel Charlton and Michael Huth. Here (Imperial College repository) and here. Presented at Mathematical Foundations of Computer Science and Information Technology (MFCSIT 06).