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