Publication List

EPSRC Grant GR/N11667

iMoc: Infinite State Model Checking Using Abstract Interpretation and Model Checking

• P. Hartel, M. Butler, A. Currie, P. Henderson, M. Leuschel, A. Martin, A. Smith, U. Ultes-Nitsche, and B. Walters.
  Questions and answers about ten formal methods.
  In S. Gnesi and D. Latella, editors, Proceedings of FMICS'99, pages 179-203, Trento, Italy, July 1999.
  Extended version as technical report DSSE-TR-99-1, Department of Electronics and Computer Science, University of Southampton.
• H. Lehmann and M. Leuschel.
  Decidability results for the propositional fluent calculus.
  In J. Lloyd, editor, Proceedings of the International Conference on Computational Logic (CL'2000), LNAI 1861, pages 762-776, London, UK, 2000. Springer-Verlag.
• H. Lehmann and M. Leuschel.
  Solving planning problems by partial deduction.
  In M. Parigot and A. Voronkov, editors, Proceedings of the International Conference on Logic for Programming and Automated Reasoning (LPAR'2000), LNAI 1955, pages 451-468, Reunion Island, France, 2000. Springer-Verlag.
• H. Lehmann and M. Leuschel.
  Generating inductive verification proofs for Isabelle using the partial evaluator Ecce.
  Technical Report DSSE-TR-2002-2, Department of Electronics and Computer Science, University of Southampton, UK, September 2002.
• M. Leuschel.
  The ECCE partial deduction system and the DPPD library of benchmarks. Obtainable via http://www.ecs.soton.ac.uk/~mal, 1996-2002.
• M. Leuschel.
  Logic program specialisation and top-down abstract interpretation reconciled.
  Technical Report DSSE-TR-2000-3, Department of Electronics and Computer Science, University of Southampton, May 2000.
• M. Leuschel.
  Design and implementation of the high-level specification language CSP(LP) in Prolog.
  In I. V. Ramakrishnan, editor, Proceedings of PADL'01, LNCS 1990, pages 14-28. Springer-Verlag, March 2001.
• M. Leuschel, L. Adhianto, M. Butler, C. Ferreira, and L. Mikhailov.
  Animation and model checking of CSP and B using prolog technology.
  In Proceedings of VCL'2001, pages 97-109, Florence, Italy, September 2001.
• M. Leuschel and S. Gruner.
  Abstract partial deduction using regular types and its application to model checking.
  In A. Pettorossi, editor, Proc. of 11th Int'l Workshop on Logic-based Program Synthesis and Transformation, LOPSTR'2001, LNCS 2372, pages 91-110, Paphos, Cyprus, 2001. Springer-Verlag.
• M. Leuschel and H. Lehmann.
  Coverability of reset Petri nets and other well-structured transition systems by partial deduction.
  In J. Lloyd, editor, Proceedings of the International Conference on Computational Logic (CL'2000), LNAI 1861, pages 101-115, London, UK, 2000. Springer-Verlag.
• M. Leuschel and H. Lehmann.
  Solving coverability problems of Petri nets by partial deduction.
  In M. Gabbrielli and F. Pfenning, editors, Proceedings of PPDP'2000, pages 268-279, Montreal, Canada, 2000. ACM Press.
• M. Leuschel and T. Massart.
  Infinite state model checking by abstract interpretation and program specialisation.
  In A. Bossi, editor, Logic-Based Program Synthesis and Transformation. Proceedings of LOPSTR'99, LNCS 1817, pages 63-82, Venice, Italy, 2000.
• M. Leuschel and T. Massart.
  Logic programming and partial deduction for the verification of reactive systems: An experimental evaluation.
  In G. Norman, M. Kwiatkowska, and D. Guelev, editors, Proceedings of AVoCS 2002, Second Workshop on Automated Verification of Critical Systems, pages 143-149, Brimingham, UK, 2002.
  Available as Technical Report CSR-02-6, University of Birmingham.
• M. Leuschel, I. Wolton, T. Massart, and L. Adhianto.
  Temporal model checking of CSP: Tools and techniques.
  In D. Nowak, editor, Proceedings of the Workshop on Automated Verification of Critical Systems (AVoCS 2001), Oxford, UK, 2002.
  Available as Technical Report PRG-RR-01-07, Oxford University Computing Laboratory.