State Machine Theory of Digital Forensic Analysis

This page presents my work on formalisation and automation of digital forensic analysis in the early 2000s. It is one of the first completely rigorous formalisations of digital forensic analysis based on theoretical computer science. The draft versions of papers and other documents posted on this web page are provided for non-commercial use only.


Event Analysis and Reconstruction in Lisp (EARL) is my historical proof-of-concept software for finite state machine analysis of digital evidence illustrated with a couple of examples.

Articles and Reports

  1. J. James, P. Gladyshev, M.T.Abdullah, Y. Zhu "Analysis of Evidence Using Formal Event Reconstruction", in Proceedings of the First International Conference on Digital Fonrensics and Cyberc Crime (ICDF2C), Albany, NY, USA, September 2009.

  2. P. Gladyshev, A. Enbacka "Rigorous Development of Automated Inconsistency Checks for Digital Evidence Using the B Method", International Journal of Digital Evidence, vol. 6, no. 2., Utica College, November 2007.

  3. P. Gladyshev, A. Patel "Formalising Event Time Bounding in Digital Investigations", International Journal of Digital Evidence, vol. 4, no. 2., Utica College, December 2005.

  4. P. Gladyshev, "Adding Real Time into State Machine Analysis of Digital Evidence", University College Dublin, June 2005.

  5. P. Gladyshev, "Finite State Machine Analysis of a Blackmail Investigation", International Journal of Digital Evidence, vol. 4, no. 1., Utica College, May 2005.

  6. P. Gladyshev, "Formalising Event Reconstruction in Digital Investigations", Ph.D. dissertation, Department of Computer Science, University College Dublin, August 2004.

  7. P. Gladyshev, A. Patel, "Finite State Machine Approach to Digital Event Reconstruction", Digital Investigation journal, vol.1, no. 2, Elsevier, May 2004. A draft of the paper is available here.

Pavel Gladyshev, Ph.D., M.Sc., Dip.Eng.

School of Computer Science,
University College Dublin,
Belfield, Dublin 4, Ireland
email: pavel dot gladyshev at ucd dot ie

Last updated: 27 March 2020