1. Jean-Raymond Abrial (2010): Modeling in Event-B - System and Software Engineering. Cambridge University Press, doi:10.1017/CBO9781139195881. Available at
  2. Jean-Raymond Abrial, Michael J. Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta & Laurent Voisin (2010): Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6), pp. 447–466, doi:10.1007/s10009-010-0145-y.
  3. (2015): The Asmeta tool set for ASM.
  4. Egon Börger & Robert F. Stärk (2003): Abstract State Machines. A Method for High-Level System Design and Analysis. Springer, doi:10.1007/978-3-642-18216-7.
  5. M. Clavel, F. Durn, S. Eker, P. Lincoln, N. Marti-Oliet, J. Meseguer & J. F. Quesada (1999): The Maude System. In: Rewriting Techniques and Applications. Springer, LNCS1631, doi:10.1007/3-540-48685-2_18.
  6. Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer & Carolyn L. Talcott (2007): All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. Lecture Notes of Computer Science 4350. Springer-Verlag, doi:10.1007/978-3-540-71999-1.
  7. Joey W. Coleman, Anders Kaels Malmos, Peter Gorm Larsen, Jan Peleska, Ralph Hains, Zoe Andrews, Richard Payne, Simon Foster, Alvaro Miyazawa, Cristiano Bertolini & André Didier (2012): COMPASS Tool Vision for a System of Systems Collaborative Development Environment. In: Proceedings of the 7th International Conference on System of System Engineering, IEEE SoSE 2012, pp. 451–456, doi:10.1109/SYSoSE.2012.6384150.
  8. Joey W. Coleman, Anders Kaels Malmos, Claus Ballegaard Nielsen & Peter Gorm Larsen (2012): Evolution of the Overture Tool Platform. In: Proceedings of the 10th Overture Workshop 2012, School of Computing Science, Newcastle University.
  9. Controllab products (2013): 20-Sim official website.
  10. Luís Diogo Couto & Richard Payne (2013): The COMPASS Proof Obligation Generator: A test case of Overture Extensibility. In: Proceedings of the 11th Overture Workshop.
  11. Luís Diogo Couto & Peter W. V. Tran-Jørgensen (2015): Extending the Overture code generator towards Isabelle syntax. In: 13th Overture Workshop, Oslo, Norway.
  12. Luís Diogo Couto, Peter W. V. Tran-Jørgensen, Joey W. Coleman & Kenneth Lausdahl (2015): Migrating to an Extensible Architecture for Abstract Syntax Trees. In: 12th Working IEEE / IFIP Conference on Software Architecture.
  13. Eclipse (2015): Dynamic Languages Toolkit. Available at
  14. (2015): Event-B and the Rodin Platform.
  15. John Fitzgerald & Peter Gorm Larsen (2009): Modelling Systems – Practical Tools and Techniques in Software Development, Second edition. Cambridge University Press, The Edinburgh Building, Cambridge CB2 2RU, UK, doi:10.1017/CBO9780511626975. ISBN 0-521-62348-0.
  16. John Fitzgerald, Peter Gorm Larsen, Paul Mukherjee, Nico Plat & Marcel Verhoef (2005): Validated Designs for Object–oriented Systems. Springer, New York, doi:10.1007/b138800. Available at
  17. John Fitzgerald, Peter Gorm Larsen & Shin Sahara (2008): VDMTools: Advances in Support for Formal Modeling in VDM. ACM Sigplan Notices 43(2), pp. 3–11, doi:10.1145/1361213.1361214.
  18. John Fitzgerald, Peter Gorm Larsen & Marcel Verhoef (2014): Collaborative Design for Embedded Systems – Co-modelling and Co-simulation. Springer, doi:10.1007/978-3-642-54118-6. Available at
  19. Simon Foster, Frank Zeyda & Jim Woodcock (2015): Isabelle/UTP: A mechanised theory engineering framework. In: Unifying Theories of Programming. Springer, pp. 21–41, doi:10.1007/978-3-319-14806-9_2.
  20. Etienne M. Gagnon & Laurie J. Hendren (1998): SableCC, an Object-Oriented Compiler Framework. In: Proceedings of the Technology of Object-Oriented Languages and Systems, TOOLS '98. IEEE Computer Society, Washington, DC, USA, pp. 140–154, doi:10.1109/TOOLS.1998.711009.
  21. E. Gamma, R. Helm, R. Johnson & R. Vlissides (1995): Design Patterns. Elements of Reusable Object-Oriented Software.. Addison-Wesley Professional Computing Series. Addison-Wesley Publishing Company.
  22. C.A.R Hoare (1978): Communicating Sequential Processes. Communications of the ACM 21(8), doi:10.1145/359576.359585.
  23. Tony Hoare & He Jifeng (1998): Unifying Theories of Programming. Prentice Hall, doi:10.1007/11768173.
  24. Isabelle/Eclipse (2015): Isabelle/Eclipse. Available at
  25. Ethan K. Jackson, Dirk Seifert, Markus Dahlweid, Thomas Santen, Nikolaj Bjørner & Wolfram Schulte (2009): Specifying and Composing Non-functional Requirements in Model-Based Development. In: Alexandre Bergel & Johan Fabry: Software Composition, Lecture Notes in Computer Science 5634. Springer Berlin Heidelberg, pp. 72–89, doi:10.1007/978-3-642-02655-3_7.
  26. Cliff B. Jones (1999): Scientific Decisions which Characterize VDM. In: J.M. Wing, J.C.P. Woodcock & J. Davies: FM'99 - Formal Methods. Springer-Verlag, pp. 28–47, doi:10.1007/3-540-48119-2_2. Lecture Notes in Computer Science 1708.
  27. Peter W.V. Jørgensen, Luís D. Couto & Morten Larsen (2014): A Code Generation Platform for VDM. In: The Overture 2014 workshop.
  28. Leslie Lamport (2002): Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley. Available at
  29. P. G. Larsen & B. S. Hansen (1996): Information technology – Programming languages, their environments and system software interfaces – Vienna Development Method – Specification Language – Part 1: Base language. International Standard ISO/IEC 13817-1.
  30. Peter Gorm Larsen, Nick Battle, Miguel Ferreira, John Fitzgerald, Kenneth Lausdahl & Marcel Verhoef (2010): The Overture Initiative – Integrating Tools for VDM. SIGSOFT Softw. Eng. Notes 35(1), pp. 1–6, doi:10.1145/1668862.1668864.
  31. Peter Gorm Larsen, Kenneth Lausdahl & Nick Battle (2010): Combinatorial Testing for VDM. In: Proceedings of the 2010 8th IEEE International Conference on Software Engineering and Formal Methods, SEFM '10. IEEE Computer Society, Washington, DC, USA, pp. 278–285, doi:10.1109/SEFM.2010.32. ISBN 978-0-7695-4153-2.
  32. Kenneth Lausdahl, Hiroshi Ishikawa & Peter Gorm Larsen (2015): Interpreting Implicit VDM Specifications using ProB. In: Proceedings of the 12th Overture Workshop, Technical Report Series CS-TR-1446. Computing Science, Newcastle University, pp. 1–15. Available at
  33. Kenneth Lausdahl, Peter Gorm Larsen & Nick Battle (2011): A Deterministic Interpreter Simulating A Distributed real time system using VDM. In: Shengchao Qin & Zongyan Qiu: Proceedings of the 13th international conference on Formal methods and software engineering, Lecture Notes in Computer Science 6991. Springer-Verlag, Berlin, Heidelberg, pp. 179–194, doi:10.1007/978-3-642-24559-6_14. Available at ISBN 978-3-642-24558-9.
  34. Michael Leuschel & Michael Butler (2003): ProB: A model checker for B. In: FME 2003: Formal Methods. Springer, pp. 855–874, doi:10.1007/978-3-540-45236-2_46.
  35. Michael Leuschel & Michael Butler (2005): Automatic refinement checking for B. In: Formal Methods and Software Engineering. Springer, pp. 345–359, doi:10.1007/11576280_24.
  36. Paul Mukherjee, Fabien Bousquet, Jérôme Delabre, Stephen Paynter & Peter Gorm Larsen (2000): Exploring Timing Properties Using VDM++ on an Industrial Application. In: J.C. Bicarregui & J.S. Fitzgerald: Proceedings of the Second VDM Workshop. Available at
  37. Tobias Nipkow, Lawrence C Paulson & Markus Wenzel (2002): Isabelle/HOL: a proof assistant for higher-order logic 2283. Springer Science & Business Media, doi:10.1007/3-540-45949-9.
  38. Terence Parr (2007): The Definitive ANTLR Reference: Building Domain-Specific Languages. Pragmatic Bookshelf.
  39. Lawrence C. Paulson (2010): Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers. In: Renate A. Schmidt, Stephan Schulz & Boris Konev: Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, PAAR-2010, Edinburgh, Scotland, UK, July 14, 2010, EPiC Series 9, pp. 1–10.
  40. Jan Peleska, Elena Vorobev & Florian Lapschies (2011): Automated Test Case Generation with SMT-Solving and Abstract Interpretation. In: Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann & Rajeev Joshi: Nasa Formal Methods, Third International Symposium, NFM 2011. NASA. Springer LNCS 6617, Pasadena, CA, USA, pp. 298–312, doi:10.1007/978-3-642-20398-5_22.
  41. (2015): The TLA Toolbox.
  42. Marcel Verhoef (2009): Modeling and Validating Distributed Embedded Real-Time Control Systems. Radboud University Nijmegen.
  43. Marcel Verhoef, Peter Gorm Larsen & Jozef Hooman (2006): Modeling and Validating Distributed Embedded Real-Time Systems with VDM++. In: Jayadev Misra, Tobias Nipkow & Emil Sekerinski: FM 2006: Formal Methods, Lecture Notes in Computer Science 4085. Springer-Verlag, pp. 147–162, doi:10.1007/11813040_11.
  44. J. Woodcock, A. Cavalcanti, J. Fitzgerald, P. Larsen, A. Miyazawa & S. Perry (2012): Features of CML: a Formal Modelling Language for Systems of Systems. In: Proceedings of the 7th International Conference on System of System Engineering. IEEE, doi:10.1109/SYSoSE.2012.6384144.
  45. Xtext (2015): Xtext. Available at

Comments and questions to:
For website issues: