var bibbase_data = {"data":"<img src=\"//bibbase.org/img/ajax-loader.gif\" id=\"spinner\"\n  style=\"display: none;\" alt=\"Loading..\" />\n\n<div id=\"bibbase\">\n\n  <script type=\"text/javascript\">\n    var bibbase = {\n      params: {\"bib\":\"http://lausdahl.github.io/overturetool.github.io/publications/overtureweb.bib\",\"jsonp\":\"1\",\"host\":\"bibbase.org\",\"ssl\":false},\n      data: [{\"bibtype\":\"techreport\",\"type\":\"techreport\",\"key\":\"Larsen&10b\",\"author\":[{\"firstnames\":[\"Peter\",\"Gorm\"],\"propositions\":[],\"lastnames\":[\"Larsen\"],\"suffixes\":[]},{\"firstnames\":[\"Kenneth\"],\"propositions\":[],\"lastnames\":[\"Lausdahl\"],\"suffixes\":[]},{\"firstnames\":[\"Nick\"],\"propositions\":[],\"lastnames\":[\"Battle\"],\"suffixes\":[]}],\"title\":\"The VDM-10 Language Manual\",\"institution\":\"The Overture Open Source Initiative\",\"year\":\"2010\",\"month\":\"April\",\"number\":\"TR-2010-06\",\"annote\":\"\",\"url_paper\":\"http://lausdahl.github.io/overturetool.github.io/files/VDM10_lang_man.pdf\",\"comment\":\"PGL\",\"bibtex\":\"@TECHREPORT{Larsen&10b,\\n  KEY           = \\\"Larsen\\\\&10\\\",\\n  AUTHOR        = \\\"Peter Gorm Larsen and Kenneth Lausdahl and Nick Battle\\\",\\n  TITLE         = \\\"{The VDM-10 Language Manual}\\\",\\n  INSTITUTION   = \\\"The Overture Open Source Initiative\\\",\\n  YEAR          = \\\"2010\\\",\\n  MONTH         = \\\"April\\\",\\n  NUMBER        = \\\"TR-2010-06\\\",\\n  ANNOTE        = \\\"\\\",\\n  url_Paper = {http://lausdahl.github.io/overturetool.github.io/files/VDM10_lang_man.pdf},\\n  COMMENT       = \\\"PGL\\\"}\\n  \\n%G VDM TOOL\\n\",\"author_short\":[\"Larsen, P. G.\",\"Lausdahl, K.\",\"Battle, N.\"],\"id\":\"Larsen&10b\",\"bibbaseid\":\"larsen-lausdahl-battle-thevdm10languagemanual-2010\",\"role\":\"author\",\"urls\":{\" paper\":\"http://lausdahl.github.io/overturetool.github.io/files/VDM10_lang_man.pdf\"},\"metadata\":{\"authorlinks\":{}},\"downloads\":2,\"html\":\"\"},{\"bibtype\":\"techreport\",\"type\":\"techreport\",\"key\":\"Larsen&10d\",\"author\":[{\"firstnames\":[\"Peter\",\"Gorm\"],\"propositions\":[],\"lastnames\":[\"Larsen\"],\"suffixes\":[]},{\"firstnames\":[\"Kenneth\"],\"propositions\":[],\"lastnames\":[\"Lausdahl\"],\"suffixes\":[]},{\"firstnames\":[\"Augusto\"],\"propositions\":[],\"lastnames\":[\"Ribeiro\"],\"suffixes\":[]},{\"firstnames\":[\"Sune\"],\"propositions\":[],\"lastnames\":[\"Wolff\"],\"suffixes\":[]},{\"firstnames\":[\"Nick\"],\"propositions\":[],\"lastnames\":[\"Battle\"],\"suffixes\":[]}],\"title\":\"Overture VDM-10 Tool Support: User Guide\",\"institution\":\"The Overture Initiative\",\"address\":\"www.overturetool.org\",\"year\":\"2010\",\"month\":\"May\",\"number\":\"TR-2010-02\",\"size\":\"103\",\"annote\":\"\",\"comment\":\"We have the sources PGL\",\"bibtex\":\"@TECHREPORT{Larsen&10d,\\n  KEY           = \\\"Larsen\\\\&10\\\",\\n  AUTHOR        = \\\"Peter Gorm Larsen and Kenneth Lausdahl and Augusto Ribeiro and\\n                   Sune Wolff and Nick Battle\\\",\\n  TITLE         = \\\"{Overture VDM-10 Tool Support: User Guide}\\\",\\n  INSTITUTION   = \\\"The Overture Initiative\\\",\\n  ADDRESS       = \\\"www.overturetool.org\\\",\\n  YEAR          = \\\"2010\\\",\\n  MONTH         = \\\"May\\\",\\n  NUMBER        = \\\"TR-2010-02\\\",\\n  SIZE          = \\\"103\\\",\\n  ANNOTE        = \\\"\\\",\\n  COMMENT       = \\\"We have the sources PGL\\\"}\\n  \\n%TR-003: Tutorial for Overture/VDM-SL, P. G. Larsen, J. S. Fitzgerald, S. Wolff, N. Battle, K. G. Lausdahl, A. Ribeiro, K. G. Pierce, S. Riddle, version 2, February 2011\\n%TR-004: Tutorial for Overture/VDM++, P. G. Larsen, J. S. Fitzgerald, S. Wolff, N. Battle, K. G. Lausdahl, A. Ribeiro, K. G. Pierce, and S. Riddle, version 2, February 2011\\n%TR-005: Tutorial for Overture/VDM-RT, P. G. Larsen, J. S. Fitzgerald, S. Wolff, N. Battle, K. G. Lausdahl, A. Ribeiro, K. G. Pierce, and S. Riddle, version 2, February 2011\\n%TR-006: Development Process for Distributed Embedded Systems using VDM, P. G. Larsen, S. Wolff, N. Battle, J. S. Fitzgerald, and K. G. Pierce version 2, February 2011\\n%TR-007: VDMJ Tool Support: User Guide, Nick Battle version 1, February 2011\\n\\n\\n%\\n% books\\n%\\n\\n%G VDM TUTOR FORMAL\\n\",\"author_short\":[\"Larsen, P. G.\",\"Lausdahl, K.\",\"Ribeiro, A.\",\"Wolff, S.\",\"Battle, N.\"],\"id\":\"Larsen&10d\",\"bibbaseid\":\"larsen-lausdahl-ribeiro-wolff-battle-overturevdm10toolsupportuserguide-2010\",\"role\":\"author\",\"urls\":{},\"metadata\":{\"authorlinks\":{}},\"downloads\":0,\"html\":\"\"},{\"bibtype\":\"book\",\"type\":\"book\",\"key\":\"Fitzgerald&05\",\"author\":[{\"firstnames\":[\"John\"],\"propositions\":[],\"lastnames\":[\"Fitzgerald\"],\"suffixes\":[]},{\"firstnames\":[\"Peter\",\"Gorm\"],\"propositions\":[],\"lastnames\":[\"Larsen\"],\"suffixes\":[]},{\"firstnames\":[\"Paul\"],\"propositions\":[],\"lastnames\":[\"Mukherjee\"],\"suffixes\":[]},{\"firstnames\":[\"Nico\"],\"propositions\":[],\"lastnames\":[\"Plat\"],\"suffixes\":[]},{\"firstnames\":[\"Marcel\"],\"propositions\":[],\"lastnames\":[\"Verhoef\"],\"suffixes\":[]}],\"title\":\"Validated Designs for Object–oriented Systems\",\"publisher\":\"Springer, New York\",\"year\":\"2005\",\"url\":\"http://www.vdmbook.com\",\"isbn\":\"1-85233-881-4\",\"annote\":\"\",\"comment\":\"PGL\",\"bibtex\":\"@BOOK{Fitzgerald&05,\\n  KEY           = \\\"Fitzgerald\\\\&05\\\",\\n  AUTHOR        = \\\"John Fitzgerald and Peter Gorm Larsen and Paul Mukherjee and\\n                   Nico Plat and Marcel Verhoef\\\",\\n  TITLE         = \\\"{Validated Designs for Object--oriented Systems}\\\",\\n  PUBLISHER     = \\\"Springer, New York\\\",\\n  YEAR          = \\\"2005\\\",\\n  URL           = \\\"http://www.vdmbook.com\\\",\\n  ISBN          = \\\"1-85233-881-4\\\",\\n  ANNOTE        = \\\"\\\",\\n  COMMENT       = \\\"PGL\\\"}\\n  \\n% Validated Designs for Object-oriented Systems (in Japanese), Hiroshi Sakoh, 2010, ISBN-10: 479811961X (Amazon link).\\n\\n%G VDM TUTOR FORMAL\\n\",\"author_short\":[\"Fitzgerald, J.\",\"Larsen, P. G.\",\"Mukherjee, P.\",\"Plat, N.\",\"Verhoef, M.\"],\"id\":\"Fitzgerald&05\",\"bibbaseid\":\"fitzgerald-larsen-mukherjee-plat-verhoef-validateddesignsforobjectorientedsystems-2005\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://www.vdmbook.com\"},\"metadata\":{\"authorlinks\":{}},\"downloads\":0,\"html\":\"\"},{\"bibtype\":\"book\",\"type\":\"book\",\"key\":\"Fitzgerald&09\",\"author\":[{\"firstnames\":[\"John\"],\"propositions\":[],\"lastnames\":[\"Fitzgerald\"],\"suffixes\":[]},{\"firstnames\":[\"Peter\",\"Gorm\"],\"propositions\":[],\"lastnames\":[\"Larsen\"],\"suffixes\":[]}],\"title\":\"Modelling Systems – Practical Tools and Techniques in Software Development\",\"publisher\":\"Cambridge University Press\",\"address\":\"The Edinburgh Building, Cambridge CB2 2RU, UK\",\"year\":\"2009\",\"edition\":\"Second\",\"note\":\"ISBN 0-521-62348-0\",\"annote\":\"\",\"comment\":\"I have the source PGL\",\"bibtex\":\"@BOOK{Fitzgerald&09,\\n  KEY           = \\\"Fitzgerald\\\\&09\\\",\\n  AUTHOR        = \\\"John Fitzgerald and Peter Gorm Larsen\\\",\\n  TITLE         = \\\"{Modelling Systems -- Practical Tools and Techniques in\\n                    Software Development}\\\",\\n  PUBLISHER     = \\\"Cambridge University Press\\\",\\n  ADDRESS       = \\\"The Edinburgh Building, Cambridge CB2 2RU, UK\\\",\\n  YEAR          = \\\"2009\\\",\\n  EDITION       = \\\"{Second}\\\",\\n  NOTE          = \\\"{ISBN 0-521-62348-0}\\\",\\n  ANNOTE        = \\\"\\\",\\n  COMMENT       = \\\"I have the source PGL\\\"}\\n  \\n%Formal Specification by VDM++ (in Japanese), Dr. Fuyuki Ishikawa, ISBN-10: 4764904098. (Amazon link).\\n\\n%2013\\n\\n% IPA/SEC Investigative Report: Success Stories of Formal Methods in Strict Specification (in Japanese), Hiroshi Sakoh and Tomohiro Oda, January 2013.\\n\\n%G VDM ALLOY TOOL\\n\",\"author_short\":[\"Fitzgerald, J.\",\"Larsen, P. G.\"],\"id\":\"Fitzgerald&09\",\"bibbaseid\":\"fitzgerald-larsen-modellingsystemspracticaltoolsandtechniquesinsoftwaredevelopment-2009\",\"role\":\"author\",\"urls\":{},\"metadata\":{\"authorlinks\":{}},\"downloads\":0,\"html\":\"\"},{\"bibtype\":\"incollection\",\"type\":\"incollection\",\"key\":\"Lausdahl&13\",\"year\":\"2013\",\"isbn\":\"978-3-642-38612-1\",\"booktitle\":\"Integrated Formal Methods\",\"volume\":\"7940\",\"series\":\"Lecture Notes in Computer Science\",\"editor\":[{\"propositions\":[],\"lastnames\":[\"Johnsen\"],\"firstnames\":[\"Einar\",\"Broch\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Petre\"],\"firstnames\":[\"Luigia\"],\"suffixes\":[]}],\"doi\":\"10.1007/978-3-642-38613-8_4\",\"title\":\"Translating VDM to Alloy\",\"url\":\"http://dx.doi.org/10.1007/978-3-642-38613-8_4\",\"publisher\":\"Springer Berlin Heidelberg\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Lausdahl\"],\"firstnames\":[\"Kenneth\"],\"suffixes\":[]}],\"pages\":\"46-60\",\"note\":\"10th International Conference, IFM 2013\",\"bibtex\":\"@incollection{Lausdahl&13,\\n  KEY       = \\\"Lausdahl\\\\&13\\\",\\n  year\\t\\t={2013},\\n  isbn\\t\\t={978-3-642-38612-1},\\n  booktitle\\t={Integrated Formal Methods},\\n  volume\\t={7940},\\n  series\\t={Lecture Notes in Computer Science},\\n  editor\\t={Johnsen, Einar Broch and Petre, Luigia},\\n  doi\\t\\t={10.1007/978-3-642-38613-8_4},\\n  title\\t\\t=\\\"{Translating VDM to Alloy}\\\",\\n  url\\t\\t={http://dx.doi.org/10.1007/978-3-642-38613-8_4},\\n  publisher\\t={Springer Berlin Heidelberg},\\n  author\\t={Lausdahl, Kenneth},\\n  pages\\t\\t={46-60},\\n  note\\t\\t={10th International Conference, IFM 2013},\\n}\\n\\n% 2012\\n\\n\",\"author_short\":[\"Lausdahl, K.\"],\"editor_short\":[\"Johnsen, E. B.\",\"Petre, L.\"],\"id\":\"Lausdahl&13\",\"bibbaseid\":\"lausdahl-translatingvdmtoalloy-2013\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://dx.doi.org/10.1007/978-3-642-38613-8_4\"},\"metadata\":{\"authorlinks\":{\"lausdahl, k\":\"https://bibbase.org/show?bib=blog.lausdahl.com/wp-content/uploads/publications/lausdahl.bib&proxy=1&groupby=year\"}},\"downloads\":4,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"key\":\"Christiansen&12a\",\"author\":[{\"firstnames\":[\"Martin\",\"Peter\"],\"propositions\":[],\"lastnames\":[\"Christiansen\"],\"suffixes\":[]},{\"firstnames\":[\"Kim\"],\"propositions\":[],\"lastnames\":[\"Bjerge\"],\"suffixes\":[]},{\"firstnames\":[\"Gareth\"],\"propositions\":[],\"lastnames\":[\"Edwards\"],\"suffixes\":[]},{\"firstnames\":[\"Peter\",\"Gorm\"],\"propositions\":[],\"lastnames\":[\"Larsen\"],\"suffixes\":[]}],\"title\":\"Towards a Methodology for Modelling and Validation of an Agricultural Vehicle's Dynamics and Control\",\"editor\":[{\"firstnames\":[\"Sergio\"],\"propositions\":[],\"lastnames\":[\"Junco\"],\"suffixes\":[]}],\"pages\":\"112-119\",\"year\":\"2012\",\"month\":\"September\",\"booktitle\":\"The 6th International Conference on Integrated Modeling and Analysis in Applied Control and Automation\",\"series\":\"IMAACA\",\"bibtex\":\"@INPROCEEDINGS{Christiansen&12a,\\n  KEY \\t\\t= \\\"Christiansen\\\\&12\\\",\\n  AUTHOR\\t= \\\"Martin Peter Christiansen and Kim Bjerge and Gareth Edwards and Peter Gorm Larsen\\\",\\n  TITLE\\t\\t= \\\"Towards a Methodology for Modelling and Validation of an Agricultural Vehicle's Dynamics and Control\\\",\\n  EDITOR    = \\\"Sergio Junco\\\",\\n  PAGES     = \\\"112-119\\\",\\n  YEAR\\t\\t= \\\"2012\\\",\\n  MONTH\\t\\t= \\\"September\\\",\\n  BOOKTITLE\\t= \\\"{The 6th International Conference on Integrated Modeling and Analysis in Applied Control and Automation}\\\",\\n  SERIES\\t= {IMAACA}\\n}\\n\\n%A Rigorous Approach to the Design of Resilient Cyber-physical Systems through Co-Simulation John Fitzgerald, Ken Pierce, Carl Gamble, in Dependable Systems and Networks Workshops (DSN-W) 2012 (WORCS), presented in June 2012, Boston, MA, USA.\\n\\n\",\"author_short\":[\"Christiansen, M. P.\",\"Bjerge, K.\",\"Edwards, G.\",\"Larsen, P. G.\"],\"editor_short\":[\"Junco, S.\"],\"id\":\"Christiansen&12a\",\"bibbaseid\":\"christiansen-bjerge-edwards-larsen-towardsamethodologyformodellingandvalidationofanagriculturalvehiclesdynamicsandcontrol-2012\",\"role\":\"author\",\"urls\":{},\"metadata\":{\"authorlinks\":{}},\"downloads\":0,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"key\":\"Wolff12a\",\"author\":[{\"firstnames\":[\"Sune\"],\"propositions\":[],\"lastnames\":[\"Wolff\"],\"suffixes\":[]}],\"title\":\"Scrum Goes Formal: Agile Methods for Safety-Critical Systems\",\"booktitle\":\"ICSE 2012: Proceedings of the 34th International Conference on Software Engineering\",\"note\":\"Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches, FormSERA 2012\",\"year\":\"2012\",\"month\":\"June\",\"pages\":\"23–29\",\"size\":\"7\",\"isbn\":\"978-1-4673-1906-5\",\"annote\":\"\",\"comment\":\"\",\"bibtex\":\"@INPROCEEDINGS{Wolff12a,\\n  KEY           = \\\"Wolff12\\\",\\n  AUTHOR        = \\\"Sune Wolff\\\",\\n  TITLE         = \\\"{Scrum Goes Formal: Agile Methods for Safety-Critical Systems}\\\",\\n  BOOKTITLE     = \\\"ICSE 2012: Proceedings of the 34th International Conference on Software\\n\\t\\t\\t\\t   Engineering\\\",\\n  NOTE\\t\\t\\t= \\\"{Workshop on Formal Methods in Software Engineering: Rigorous\\n\\t\\t\\t\\t   and Agile Approaches, FormSERA 2012}\\\",\\n  YEAR          = \\\"2012\\\",\\n  MONTH         = \\\"June\\\",\\n  PAGES         = \\\"23--29\\\",\\n  SIZE\\t\\t\\t= \\\"7\\\",\\n  ISBN          = \\\"978-1-4673-1906-5\\\",\\n  ANNOTE        = \\\"\\\",\\n  COMMENT       = \\\"\\\"}\\n  \\n\",\"author_short\":[\"Wolff, S.\"],\"id\":\"Wolff12a\",\"bibbaseid\":\"wolff-scrumgoesformalagilemethodsforsafetycriticalsystems-2012\",\"role\":\"author\",\"urls\":{},\"metadata\":{\"authorlinks\":{}},\"downloads\":0,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"key\":\"Nielsen&12\",\"author\":[{\"firstnames\":[\"Claus\",\"Ballegaard\"],\"propositions\":[],\"lastnames\":[\"Nielsen\"],\"suffixes\":[]},{\"firstnames\":[\"Kenneth\"],\"propositions\":[],\"lastnames\":[\"Lausdahl\"],\"suffixes\":[]},{\"firstnames\":[\"Peter\",\"Gorm\"],\"propositions\":[],\"lastnames\":[\"Larsen\"],\"suffixes\":[]}],\"title\":\"Combining VDM with Executable Code\",\"booktitle\":\"Abstract State Machines, Alloy, B, VDM, and Z\",\"volume\":\"7316\",\"editor\":[{\"propositions\":[],\"lastnames\":[\"Derrick\"],\"firstnames\":[\"John\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Fitzgerald\"],\"firstnames\":[\"John\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Gnesi\"],\"firstnames\":[\"Stefania\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Khurshid\"],\"firstnames\":[\"Sarfraz\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Leuschel\"],\"firstnames\":[\"Michael\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Reeves\"],\"firstnames\":[\"Steve\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Riccobene\"],\"firstnames\":[\"Elvinia\"],\"suffixes\":[]}],\"year\":\"2012\",\"location\":\"Pisa, Italy\",\"pages\":\"266–279\",\"numpages\":\"14\",\"series\":\"Lecture Notes in Computer Science\",\"publisher\":\"Springer-Verlag\",\"address\":\"Berlin, Heidelberg\",\"note\":\"ISBN 978-3-642-30884-0\",\"url\":\"http://dx.doi.org/10.1007/978-3-642-30885-7_19\",\"bibtex\":\"@INPROCEEDINGS{Nielsen&12,\\n  KEY\\t\\t\\t= \\\"Nielsen\\\\&12\\\",\\n  AUTHOR\\t\\t= \\\"Claus Ballegaard Nielsen and Kenneth Lausdahl and Peter Gorm Larsen\\\",\\n  TITLE\\t\\t\\t= \\\"{Combining VDM with Executable Code}\\\",\\n  booktitle  \\t= \\\"{Abstract State Machines, Alloy, B, VDM, and Z}\\\",\\n  volume\\t\\t= {7316},\\n  editor\\t\\t= {Derrick, John and Fitzgerald, John and Gnesi, Stefania and Khurshid, Sarfraz and Leuschel, Michael and Reeves, Steve and Riccobene, Elvinia},\\n  YEAR\\t\\t\\t= \\\"2012\\\",\\n  location \\t\\t= {Pisa, Italy},\\n  pages \\t\\t= {266--279},\\n  numpages \\t\\t= {14},\\n  SERIES        = \\\"Lecture Notes in Computer Science\\\",\\n  VOLUME        = \\\"7316\\\",\\n  publisher \\t= {Springer-Verlag},\\n  address \\t\\t= {Berlin, Heidelberg},\\n  NOTE       \\t= \\\"{ISBN 978-3-642-30884-0}\\\",\\n  url \\t\\t\\t= {http://dx.doi.org/10.1007/978-3-642-30885-7_19},\\n  }\\n  \\n\",\"author_short\":[\"Nielsen, C. B.\",\"Lausdahl, K.\",\"Larsen, P. G.\"],\"editor_short\":[\"Derrick, J.\",\"Fitzgerald, J.\",\"Gnesi, S.\",\"Khurshid, S.\",\"Leuschel, M.\",\"Reeves, S.\",\"Riccobene, E.\"],\"id\":\"Nielsen&12\",\"bibbaseid\":\"nielsen-lausdahl-larsen-combiningvdmwithexecutablecode-2012\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://dx.doi.org/10.1007/978-3-642-30885-7_19\"},\"metadata\":{\"authorlinks\":{\"lausdahl, k\":\"https://bibbase.org/show?bib=blog.lausdahl.com/wp-content/uploads/publications/lausdahl.bib&proxy=1&groupby=year\"}},\"downloads\":2,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"key\":\"Payne&12a\",\"author\":[{\"firstnames\":[\"Richard\"],\"propositions\":[],\"lastnames\":[\"Payne\"],\"suffixes\":[]},{\"firstnames\":[\"Jeremy\"],\"propositions\":[],\"lastnames\":[\"Bryans\"],\"suffixes\":[]},{\"firstnames\":[\"John\"],\"propositions\":[],\"lastnames\":[\"Fitzgerald\"],\"suffixes\":[]},{\"firstnames\":[\"Steve\"],\"propositions\":[],\"lastnames\":[\"Riddle\"],\"suffixes\":[]}],\"title\":\"Interface Specification for System-of-Systems Architectures\",\"booktitle\":\"Proceedings of the 7th International Conference on System of System Engineering, IEEE SoSE 2012\",\"publisher\":\"IEEE\",\"year\":\"2012\",\"month\":\"July\",\"bibtex\":\"@INPROCEEDINGS{Payne&12a,\\n  KEY           = \\\"Payne&12a\\\",\\n  AUTHOR        = \\\"Richard Payne and Jeremy Bryans and John Fitzgerald and Steve Riddle\\\",\\n  TITLE         = \\\"{Interface Specification for System-of-Systems Architectures}\\\",\\n  BOOKTITLE     = \\\"Proceedings of the 7th International Conference on\\n                   System of System Engineering, IEEE SoSE 2012\\\",\\n  PUBLISHER     = \\\"{IEEE}\\\",\\n  YEAR          = 2012,\\n  MONTH         = \\\"July\\\"}\\n  \\n\",\"author_short\":[\"Payne, R.\",\"Bryans, J.\",\"Fitzgerald, J.\",\"Riddle, S.\"],\"id\":\"Payne&12a\",\"bibbaseid\":\"payne-bryans-fitzgerald-riddle-interfacespecificationforsystemofsystemsarchitectures-2012\",\"role\":\"author\",\"urls\":{},\"metadata\":{\"authorlinks\":{}},\"downloads\":0,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"key\":\"Fitzgerald&12c\",\"author\":[{\"firstnames\":[\"John\",\"S.\"],\"propositions\":[],\"lastnames\":[\"Fitzgerald\"],\"suffixes\":[]},{\"firstnames\":[\"Jeremy\"],\"propositions\":[],\"lastnames\":[\"Bryans\"],\"suffixes\":[]},{\"firstnames\":[\"Richard\"],\"propositions\":[],\"lastnames\":[\"Payne\"],\"suffixes\":[]}],\"title\":\"A Formal Model-Based Approach to Engineering Systems-of-Systems\",\"editor\":[{\"firstnames\":[\"Luis\",\"M.\"],\"propositions\":[],\"lastnames\":[\"Camarinha-Matos\"],\"suffixes\":[]},{\"firstnames\":[\"Lai\"],\"propositions\":[],\"lastnames\":[\"Xu\"],\"suffixes\":[]},{\"firstnames\":[\"Hamideh\"],\"propositions\":[],\"lastnames\":[\"Afsarmanesh\"],\"suffixes\":[]}],\"booktitle\":\"Collaborative Networks in the Internet of Services - 13th IFIP WG 5.5 Working Conference on Virtual Enterprises, PRO-VE 2012, Bournemouth, UK, October 1-3, 2012. Proceedings\",\"publisher\":\"Springer\",\"series\":\"IFIP Advances in Information and Communication Technology\",\"volume\":\"380\",\"year\":\"2012\",\"pages\":\"53-62\",\"ee\":\"http://dx.doi.org/10.1007/978-3-642-32775-9_6\",\"bibsource\":\"DBLP, http://dblp.uni-trier.de\",\"bibtex\":\"@inproceedings{Fitzgerald&12c,\\n  key       = \\\"Fitzgerald\\\\&12c\\\",\\n  author    = {John S. Fitzgerald and\\n               Jeremy Bryans and\\n               Richard Payne},\\n  title     = {A Formal Model-Based Approach to Engineering\\nSystems-of-Systems},\\n  editor    = {Luis M. Camarinha-Matos and\\n               Lai Xu and\\n               Hamideh Afsarmanesh},\\n  booktitle = {Collaborative Networks in the Internet of Services - 13th\\n               IFIP WG 5.5 Working Conference on Virtual Enterprises,\\nPRO-VE 2012, Bournemouth, UK, October 1-3, 2012. Proceedings},\\n  publisher = {Springer},\\n  series    = {IFIP Advances in Information and Communication Technology},\\n  volume    = {380},\\n  year      = {2012},\\n  pages     = {53-62},\\n  ee        = {http://dx.doi.org/10.1007/978-3-642-32775-9_6},\\n  bibsource = {DBLP, http://dblp.uni-trier.de}\\n}\\n\\n\",\"author_short\":[\"Fitzgerald, J. S.\",\"Bryans, J.\",\"Payne, R.\"],\"editor_short\":[\"Camarinha-Matos, L. M.\",\"Xu, L.\",\"Afsarmanesh, H.\"],\"id\":\"Fitzgerald&12c\",\"bibbaseid\":\"fitzgerald-bryans-payne-aformalmodelbasedapproachtoengineeringsystemsofsystems-2012\",\"role\":\"author\",\"urls\":{\"Link\":\"http://dx.doi.org/10.1007/978-3-642-32775-9_6\"},\"metadata\":{\"authorlinks\":{}},\"downloads\":1,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"key\":\"Larsen&12a\",\"author\":[{\"firstnames\":[\"Peter\",\"Gorm\"],\"propositions\":[],\"lastnames\":[\"Larsen\"],\"suffixes\":[]},{\"firstnames\":[\"Joey\",\"W.\\\\\"],\"propositions\":[],\"lastnames\":[\"Coleman\"],\"suffixes\":[]},{\"firstnames\":[\"John\"],\"propositions\":[],\"lastnames\":[\"Fitzgerald\"],\"suffixes\":[]}],\"editor\":[{\"firstnames\":[\"Alexander\",\"K.\"],\"propositions\":[],\"lastnames\":[\"Petrenko\"],\"suffixes\":[]}],\"title\":\"Getting Software Engineering out of Isolation\",\"booktitle\":\"SYRCoSE Software Engineering Colloquium\",\"address\":\"Perm, Russia\",\"year\":\"2012\",\"month\":\"May\",\"note\":\"ISBN 978-5-91474-019-8\",\"pages\":\"\",\"annote\":\"\",\"comment\":\"BIB PGL I also have the sources\",\"bibtex\":\"@INPROCEEDINGS{Larsen&12a,\\n  KEY           = \\\"Larsen\\\\&12\\\",\\n  AUTHOR        = \\\"Peter Gorm Larsen and Joey W.\\\\ Coleman and John Fitzgerald\\\",\\n  EDITOR        = \\\"Alexander K. Petrenko\\\",\\n  TITLE         = \\\"{Getting Software Engineering out of Isolation}\\\",\\n  BOOKTITLE     = \\\"SYRCoSE Software Engineering Colloquium\\\",\\n  ADDRESS       = \\\"Perm, Russia\\\",\\n  YEAR          = \\\"2012\\\",\\n  MONTH         = \\\"May\\\",\\n  NOTE          = \\\"ISBN 978-5-91474-019-8\\\",\\n  PAGES         = \\\"\\\",\\n  ANNOTE        = \\\"\\\",\\n  COMMENT       = \\\"BIB PGL I also have the sources\\\"}\\n  \\n%2011\\n\\n\",\"author_short\":[\"Larsen, P. G.\",\"Coleman, J. W.\",\"Fitzgerald, J.\"],\"editor_short\":[\"Petrenko, A. K.\"],\"id\":\"Larsen&12a\",\"bibbaseid\":\"larsen-coleman-fitzgerald-gettingsoftwareengineeringoutofisolation-2012\",\"role\":\"author\",\"urls\":{},\"metadata\":{\"authorlinks\":{}},\"downloads\":0,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"key\":\"Lausdahl&11\",\"author\":[{\"firstnames\":[\"Kenneth\"],\"propositions\":[],\"lastnames\":[\"Lausdahl\"],\"suffixes\":[]},{\"firstnames\":[\"Peter\",\"Gorm\"],\"propositions\":[],\"lastnames\":[\"Larsen\"],\"suffixes\":[]},{\"firstnames\":[\"Nick\"],\"propositions\":[],\"lastnames\":[\"Battle\"],\"suffixes\":[]}],\"title\":\"A Deterministic Interpreter Simulating A Distributed real time system using VDM\",\"booktitle\":\"Proceedings of the 13th international conference on Formal methods and software engineering\",\"series\":\"Lecture Notes in Computer Science\",\"volume\":\"6991\",\"editor\":[{\"propositions\":[],\"lastnames\":[\"Qin\"],\"firstnames\":[\"Shengchao\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Qiu\"],\"firstnames\":[\"Zongyan\"],\"suffixes\":[]}],\"year\":\"2011\",\"month\":\"October\",\"note\":\"ISBN 978-3-642-24558-9\",\"location\":\"Durham, UK\",\"pages\":\"179–194\",\"numpages\":\"16\",\"url\":\"http://dl.acm.org/citation.cfm?id=2075089.2075107\",\"publisher\":\"Springer-Verlag\",\"address\":\"Berlin, Heidelberg\",\"bibtex\":\"@INPROCEEDINGS{Lausdahl&11,\\n  KEY           = \\\"Lausdahl\\\\&11\\\",\\n  AUTHOR        = \\\"Kenneth Lausdahl and Peter Gorm Larsen and Nick Battle\\\",\\n  title \\t\\t= \\\"{A Deterministic Interpreter Simulating A Distributed real time system using VDM}\\\",\\n  booktitle \\t= {Proceedings of the 13th international conference on Formal methods and software engineering},\\n  series\\t\\t= {Lecture Notes in Computer Science},\\n  volume\\t\\t= {6991},\\n  editor\\t\\t= {Qin, Shengchao and Qiu, Zongyan},\\n  YEAR          = \\\"2011\\\",\\n  MONTH         = \\\"October\\\",\\n  note        \\t= \\\"{ISBN 978-3-642-24558-9}\\\",\\n   location \\t= {Durham, UK},\\n pages \\t\\t\\t= {179--194},\\n numpages \\t\\t= {16},\\n url \\t\\t\\t= {http://dl.acm.org/citation.cfm?id=2075089.2075107},\\n   publisher \\t= {Springer-Verlag},\\n address \\t\\t= {Berlin, Heidelberg},\\n  }\\n  \\n\",\"author_short\":[\"Lausdahl, K.\",\"Larsen, P. G.\",\"Battle, N.\"],\"editor_short\":[\"Qin, S.\",\"Qiu, Z.\"],\"id\":\"Lausdahl&11\",\"bibbaseid\":\"lausdahl-larsen-battle-adeterministicinterpretersimulatingadistributedrealtimesystemusingvdm-2011\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://dl.acm.org/citation.cfm?id=2075089.2075107\"},\"metadata\":{\"authorlinks\":{\"lausdahl, k\":\"https://bibbase.org/show?bib=blog.lausdahl.com/wp-content/uploads/publications/lausdahl.bib&proxy=1&groupby=year\"}},\"downloads\":0,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"key\":\"Pierce&11\",\"author\":[{\"firstnames\":[\"Ken\"],\"propositions\":[],\"lastnames\":[\"Pierce\"],\"suffixes\":[]},{\"firstnames\":[\"John\"],\"propositions\":[],\"lastnames\":[\"Fitzgerald\"],\"suffixes\":[]},{\"firstnames\":[\"Carl\"],\"propositions\":[],\"lastnames\":[\"Gamble\"],\"suffixes\":[]}],\"title\":\"Modelling Faults and Fault Tolerance Mechanisms in a Paper Pinch Co- model\",\"booktitle\":\"Proceedings of the ERCIM/EWICS/Cyber-physical Systems Workshop at SafeComp 2011, Naples, Italy (to appear)\",\"year\":\"2011\",\"month\":\"September\",\"publisher\":\"ERCIM\",\"bibtex\":\"@INPROCEEDINGS{Pierce&11,\\n  KEY = {Pierce\\\\&11},\\n  AUTHOR = {Ken Pierce and John Fitzgerald and Carl Gamble},\\n  TITLE = {Modelling Faults and Fault Tolerance Mechanisms in a Paper Pinch Co- model},\\n  BOOKTITLE = {Proceedings of the ERCIM/EWICS/Cyber-physical Systems Workshop at SafeComp 2011, Naples, Italy (to appear)},\\n  YEAR = {2011},\\n  MONTH = {September},\\n  PUBLISHER = {ERCIM}\\n}\\n\\n\\n% VDM-SL, VDM++ Simple Reference (in Japanese), Dr. Fuyuki Ishikawa, June 2011.\\n\\n%VDM specification as Structured Japanese Specification (in Japanese), Shin Sahara, SEC journal, Vol. 26., 31th March, 2011, pp. 23-27, ISSN 1349-8622.\\n\\n%Answers to Frequently Asked Questions for the Practice of Formal Methods (in Japanese), Dr. Taro Kurita, SEC journal, Vol. 26., 31th March, 2011, pp. 34-39, ISSN 1349-8622.\\n\\n%2010\\n\\n\",\"author_short\":[\"Pierce, K.\",\"Fitzgerald, J.\",\"Gamble, C.\"],\"id\":\"Pierce&11\",\"bibbaseid\":\"pierce-fitzgerald-gamble-modellingfaultsandfaulttolerancemechanismsinapaperpinchcomodel-2011\",\"role\":\"author\",\"urls\":{},\"metadata\":{\"authorlinks\":{}},\"downloads\":0,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"key\":\"Ribeiro&10\",\"author\":[{\"firstnames\":[\"Augusto\"],\"propositions\":[],\"lastnames\":[\"Ribeiro\"],\"suffixes\":[]},{\"firstnames\":[\"Peter\",\"Gorm\"],\"propositions\":[],\"lastnames\":[\"Larsen\"],\"suffixes\":[]}],\"editor\":[{\"firstnames\":[\"Jin\"],\"propositions\":[],\"lastnames\":[\"Song\"],\"suffixes\":[]},{\"firstnames\":[],\"propositions\":[],\"lastnames\":[\"Huibiao\"],\"suffixes\":[]}],\"title\":\"Proof Obligation Generation and Discharging for Recursive Definitions in VDM\",\"booktitle\":\"The 12th International Conference on Formal Engineering Methods (ICFEM 2010)\",\"publisher\":\"Springer-Verlag\",\"year\":\"2010\",\"month\":\"November\",\"annote\":\"\",\"comment\":\"I have the sources PGL\",\"bibtex\":\"@INPROCEEDINGS{Ribeiro&10,\\n  KEY           = \\\"Ribeiro\\\\&10\\\",\\n  AUTHOR        = \\\"Augusto Ribeiro and Peter Gorm Larsen\\\",\\n  EDITOR        = \\\"Jin Song and Huibiao\\\",\\n  TITLE         = \\\"{Proof Obligation Generation and Discharging for\\n                   Recursive Definitions in {VDM}}\\\",\\n  BOOKTITLE     = \\\"The 12th International Conference on Formal Engineering\\n                   Methods (ICFEM 2010)\\\",\\n  PUBLISHER     = \\\"Springer-Verlag\\\",\\n  YEAR          = \\\"2010\\\",\\n  MONTH         = \\\"November\\\",\\n  ANNOTE        = \\\"\\\",\\n  COMMENT       = \\\"I have the sources PGL\\\"}\\n  \\n\",\"author_short\":[\"Ribeiro, A.\",\"Larsen, P. G.\"],\"editor_short\":[\"Song, J.\",\"Huibiao\"],\"id\":\"Ribeiro&10\",\"bibbaseid\":\"ribeiro-larsen-proofobligationgenerationanddischargingforrecursivedefinitionsinvdm-2010\",\"role\":\"author\",\"urls\":{},\"metadata\":{\"authorlinks\":{}},\"downloads\":0,\"html\":\"\"},{\"bibtype\":\"techreport\",\"type\":\"techreport\",\"key\":\"Fitzgerald&10a\",\"author\":[{\"firstnames\":[\"John\"],\"propositions\":[],\"lastnames\":[\"Fitzgerald\"],\"suffixes\":[]},{\"firstnames\":[\"Peter\",\"Gorm\"],\"propositions\":[],\"lastnames\":[\"Larsen\"],\"suffixes\":[]},{\"firstnames\":[\"Ken\"],\"propositions\":[],\"lastnames\":[\"Pierce\"],\"suffixes\":[]},{\"firstnames\":[\"Marcel\"],\"propositions\":[],\"lastnames\":[\"Verhoef\"],\"suffixes\":[]},{\"firstnames\":[\"Sune\"],\"propositions\":[],\"lastnames\":[\"Wolff\"],\"suffixes\":[]}],\"title\":\"Collaborative Modelling and Co-simulation in the Development of Dependable Embedded Systems\",\"institution\":\"School of Computing Science, Newcastle University\",\"year\":\"2010\",\"month\":\"July\",\"number\":\"CS-TR-1213\",\"url\":\"http://www.cs.ncl.ac.uk/publications/trs/papers/1213.pdf\",\"bibtex\":\"@TECHREPORT{Fitzgerald&10a,\\n  KEY           = \\\"Fitzgerald\\\\&10a\\\",\\n  AUTHOR        = {John Fitzgerald and Peter Gorm Larsen and Ken Pierce and Marcel Verhoef and Sune Wolff},\\n  TITLE         = \\\"{Collaborative Modelling and Co-simulation in the Development of Dependable Embedded Systems}\\\",\\n  INSTITUTION   = \\\"School of Computing Science, Newcastle University\\\",\\n  YEAR          = \\\"2010\\\",\\n  MONTH         = \\\"July\\\",\\n  NUMBER        = \\\"{CS-TR-1213}\\\",\\n  URL           = \\\"http://www.cs.ncl.ac.uk/publications/trs/papers/1213.pdf\\\"}\\n  \\n\",\"author_short\":[\"Fitzgerald, J.\",\"Larsen, P. G.\",\"Pierce, K.\",\"Verhoef, M.\",\"Wolff, S.\"],\"id\":\"Fitzgerald&10a\",\"bibbaseid\":\"fitzgerald-larsen-pierce-verhoef-wolff-collaborativemodellingandcosimulationinthedevelopmentofdependableembeddedsystems-2010\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://www.cs.ncl.ac.uk/publications/trs/papers/1213.pdf\"},\"metadata\":{\"authorlinks\":{}},\"downloads\":3,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"key\":\"Larsen&10g\",\"author\":[{\"firstnames\":[\"Peter\",\"Gorm\"],\"propositions\":[],\"lastnames\":[\"Larsen\"],\"suffixes\":[]},{\"firstnames\":[\"John\"],\"propositions\":[],\"lastnames\":[\"Fitzgerald\"],\"suffixes\":[]},{\"firstnames\":[\"Sune\"],\"propositions\":[],\"lastnames\":[\"Wolff\"],\"suffixes\":[]}],\"editor\":[{\"firstnames\":[\"Stefan\"],\"propositions\":[],\"lastnames\":[\"Gruner\"],\"suffixes\":[]},{\"firstnames\":[\"Bernhard\"],\"propositions\":[],\"lastnames\":[\"Rumpe\"],\"suffixes\":[]}],\"title\":\"Are Formal Methods Ready for Agility? A Reality Check\",\"booktitle\":\"2nd International Workshop on Formal Methods and Agile Methods\",\"publisher\":\"Lecture Notes in Informatics\",\"pages\":\"13–25\",\"year\":\"2010\",\"month\":\"September\",\"note\":\"ISSH 1617-5468\",\"annote\":\"\",\"comment\":\"BIB I have the sources PGL\",\"bibtex\":\"@INPROCEEDINGS{Larsen&10g,\\n  KEY           = \\\"Larsen\\\\&10\\\",\\n  AUTHOR        = \\\"Peter Gorm Larsen and John Fitzgerald and Sune Wolff\\\",\\n  EDITOR        = \\\"Stefan Gruner and Bernhard Rumpe\\\",\\n  TITLE         = \\\"Are Formal Methods Ready for Agility? A Reality Check\\\",\\n  BOOKTITLE     = \\\"2nd International Workshop on Formal Methods and Agile\\n                   Methods\\\",\\n  PUBLISHER     = \\\"Lecture Notes in Informatics\\\",\\n  PAGES         = \\\"13--25\\\",\\n  YEAR          = \\\"2010\\\",\\n  MONTH         = \\\"September\\\",\\n  NOTE          = \\\"ISSH 1617-5468\\\",\\n  ANNOTE        = \\\"\\\",\\n  COMMENT       = \\\"BIB I have the sources PGL\\\"}\\n  \\n\",\"author_short\":[\"Larsen, P. G.\",\"Fitzgerald, J.\",\"Wolff, S.\"],\"editor_short\":[\"Gruner, S.\",\"Rumpe, B.\"],\"id\":\"Larsen&10g\",\"bibbaseid\":\"larsen-fitzgerald-wolff-areformalmethodsreadyforagilityarealitycheck-2010\",\"role\":\"author\",\"urls\":{},\"metadata\":{\"authorlinks\":{}},\"downloads\":0,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"key\":\"Larsen&09a\",\"author\":[{\"firstnames\":[\"Peter\",\"Gorm\"],\"propositions\":[],\"lastnames\":[\"Larsen\"],\"suffixes\":[]},{\"firstnames\":[\"Kenneth\"],\"propositions\":[],\"lastnames\":[\"Lausdahl\"],\"suffixes\":[]},{\"firstnames\":[\"Nick\"],\"propositions\":[],\"lastnames\":[\"Battle\"],\"suffixes\":[]}],\"title\":\"Combinatorial Testing for VDM++\",\"booktitle\":\"Submitted for publication\",\"year\":\"2009\",\"month\":\"December\",\"note\":\"Outdated by i̧teLarsen&10c\",\"annote\":\"\",\"comment\":\"Outdated by i̧teLarsen&10c\",\"bibtex\":\"@INPROCEEDINGS{Larsen&09a,\\n  KEY           = \\\"Larsen\\\\&09\\\",\\n  AUTHOR        = \\\"Peter Gorm Larsen and Kenneth Lausdahl and Nick Battle\\\",\\n  TITLE         = \\\"{Combinatorial Testing for VDM++}\\\",\\n  BOOKTITLE     = \\\"Submitted for publication\\\",\\n  YEAR          = \\\"2009\\\",\\n  MONTH         = \\\"December\\\",\\n  NOTE          = \\\"Outdated by \\\\cite{Larsen&10c}\\\",\\n  ANNOTE        = \\\"\\\",\\n  COMMENT       = \\\"Outdated by \\\\cite{Larsen&10c}\\\"}\\n  \\n\",\"author_short\":[\"Larsen, P. G.\",\"Lausdahl, K.\",\"Battle, N.\"],\"id\":\"Larsen&09a\",\"bibbaseid\":\"larsen-lausdahl-battle-combinatorialtestingforvdm-2009\",\"role\":\"author\",\"urls\":{},\"metadata\":{\"authorlinks\":{}},\"downloads\":0,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"key\":\"Broenink&10\",\"author\":[{\"propositions\":[],\"lastnames\":[\"Broenink\"],\"firstnames\":[\"J.\",\"F.\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Larsen\"],\"firstnames\":[\"P.\",\"G.\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Verhoef\"],\"firstnames\":[\"M.\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Kleijn\"],\"firstnames\":[\"C.\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Jovanovic\"],\"firstnames\":[\"D.\"],\"suffixes\":[]},{\"propositions\":[],\"lastnames\":[\"Pierce\"],\"firstnames\":[\"K.\"],\"suffixes\":[]},{\"firstnames\":[\"Wouters\"],\"propositions\":[],\"lastnames\":[\"F.\"],\"suffixes\":[]}],\"title\":\"Design Support and Tooling for Dependable Embedded Control Software\",\"booktitle\":\"Proceedings of Serene 2010 International Workshop on Software Engineering for Resilient Systems\",\"publisher\":\"ACM\",\"year\":\"2010\",\"month\":\"April\",\"pages\":\"77–82\",\"annote\":\"\",\"comment\":\"I have the sources (PGL)\",\"bibtex\":\"@INPROCEEDINGS{Broenink&10,\\n  KEY           = \\\"Broenink\\\\&10\\\",\\n  AUTHOR        = \\\"Broenink, J. F. and Larsen, P. G. and  Verhoef, M. and\\n                   Kleijn, C. and  Jovanovic, D. and Pierce, K. and\\n                   Wouters F.\\\",\\n  TITLE         = \\\"{Design Support and Tooling for Dependable Embedded Control Software}\\\",\\n  BOOKTITLE     = \\\"Proceedings of Serene 2010 International Workshop on\\n                   Software Engineering for Resilient Systems\\\",\\n  PUBLISHER     = \\\"ACM\\\",\\n  YEAR          = \\\"2010\\\",\\n  MONTH         = \\\"April\\\",\\n  PAGES         = \\\"77--82\\\",\\n  ANNOTE        = \\\"\\\",\\n  COMMENT       = \\\"I have the sources (PGL)\\\"}\\n  \\n% Proving Consistency of VDM models using HOL, Sander D. Vermolen, Jozef Hooman and Peter Gorm Larsen, in Proceedings of the 2010 ACM Symposium on Applied Computing, ACM, March 2010.\\n\\n% Formal Semantics of a VDM Extension for Distributed Embedded Systems, Jozef Hooman and Marcel Verhoef, in D. Dams and U. Hannemann and M. Steffen (eds): W.P. de Roever Festschrift, LNCS 5930, pp 142-161, 2010.\\n\\n\",\"author_short\":[\"Broenink, J. F.\",\"Larsen, P. G.\",\"Verhoef, M.\",\"Kleijn, C.\",\"Jovanovic, D.\",\"Pierce, K.\",\"F., W.\"],\"id\":\"Broenink&10\",\"bibbaseid\":\"broenink-larsen-verhoef-kleijn-jovanovic-pierce-f-designsupportandtoolingfordependableembeddedcontrolsoftware-2010\",\"role\":\"author\",\"urls\":{},\"metadata\":{\"authorlinks\":{}},\"downloads\":0,\"html\":\"\"},{\"bibtype\":\"article\",\"type\":\"article\",\"key\":\"Larsen&10a\",\"author\":[{\"firstnames\":[\"Peter\",\"Gorm\"],\"propositions\":[],\"lastnames\":[\"Larsen\"],\"suffixes\":[]},{\"firstnames\":[\"Nick\"],\"propositions\":[],\"lastnames\":[\"Battle\"],\"suffixes\":[]},{\"firstnames\":[\"Miguel\"],\"propositions\":[],\"lastnames\":[\"Ferreira\"],\"suffixes\":[]},{\"firstnames\":[\"John\"],\"propositions\":[],\"lastnames\":[\"Fitzgerald\"],\"suffixes\":[]},{\"firstnames\":[\"Kenneth\"],\"propositions\":[],\"lastnames\":[\"Lausdahl\"],\"suffixes\":[]},{\"firstnames\":[\"Marcel\"],\"propositions\":[],\"lastnames\":[\"Verhoef\"],\"suffixes\":[]}],\"title\":\"The Overture Initiative – Integrating Tools for VDM\",\"journal\":\"SIGSOFT Softw. Eng. Notes\",\"year\":\"2010\",\"month\":\"January\",\"volume\":\"35\",\"number\":\"1\",\"pages\":\"1–6\",\"size\":\"6\",\"annote\":\"\",\"numpages\":\"6\",\"issn\":\"0163-5948\",\"address\":\"New York, NY, USA\",\"publisher\":\"ACM\",\"url\":\"http://doi.acm.org/10.1145/1668862.1668864\",\"bibtex\":\"@ARTICLE{Larsen&10a,\\n  KEY           = \\\"Larsen\\\\&10\\\",\\n  AUTHOR        = \\\"Peter Gorm Larsen and Nick Battle and Miguel Ferreira\\n                   and John Fitzgerald and Kenneth Lausdahl and Marcel\\n                   Verhoef\\\",\\n  TITLE         = \\\"{The Overture Initiative -- Integrating Tools for VDM}\\\",\\n  JOURNAL       = {SIGSOFT Softw. Eng. Notes},\\n  YEAR          = \\\"2010\\\",\\n  MONTH         = \\\"January\\\",\\n  VOLUME        = \\\"35\\\",\\n  NUMBER        = \\\"1\\\",\\n  PAGES         = \\\"1--6\\\",\\n  SIZE          = \\\"6\\\",\\n  ANNOTE        = \\\"\\\",\\n  numpages = {6},\\n  issn = {0163-5948},\\n  address = {New York, NY, USA},\\n  publisher = {ACM},\\n  URL\\t\\t\\t= \\\"http://doi.acm.org/10.1145/1668862.1668864\\\"}\\n  \\n%2009\\n\\n\",\"author_short\":[\"Larsen, P. G.\",\"Battle, N.\",\"Ferreira, M.\",\"Fitzgerald, J.\",\"Lausdahl, K.\",\"Verhoef, M.\"],\"id\":\"Larsen&10a\",\"bibbaseid\":\"larsen-battle-ferreira-fitzgerald-lausdahl-verhoef-theovertureinitiativeintegratingtoolsforvdm-2010\",\"role\":\"author\",\"urls\":{\"Paper\":\"http://doi.acm.org/10.1145/1668862.1668864\"},\"metadata\":{\"authorlinks\":{\"lausdahl, k\":\"https://bibbase.org/show?bib=blog.lausdahl.com/wp-content/uploads/publications/lausdahl.bib&proxy=1&groupby=year\"}},\"downloads\":1,\"html\":\"\"},{\"bibtype\":\"phdthesis\",\"type\":\"phdthesis\",\"key\":\"Verhoef09\",\"author\":[{\"firstnames\":[\"Marcel\"],\"propositions\":[],\"lastnames\":[\"Verhoef\"],\"suffixes\":[]}],\"title\":\"Modeling and Validating Distributed Embedded Real-Time Control Systems\",\"school\":\"Radboud University Nijmegen\",\"year\":\"2009\",\"number\":\"RU. 2009-01\",\"annote\":\"ISBN 978-90-9023705-3\",\"comment\":\"I have a copy PGL\",\"bibtex\":\"@PHDTHESIS{Verhoef09,\\n  KEY           = \\\"Verhoef09\\\",\\n  AUTHOR        = \\\"Marcel Verhoef\\\",\\n  TITLE         = \\\"{Modeling and Validating Distributed Embedded Real-Time\\n                    Control Systems}\\\",\\n  SCHOOL        = \\\"Radboud University Nijmegen\\\",\\n  YEAR          = \\\"2009\\\",\\n  NUMBER        = \\\"RU. 2009-01\\\",\\n  ANNOTE          = \\\"{ISBN 978-90-9023705-3}\\\",\\n  COMMENT       = \\\"I have a copy PGL\\\"}\\n  \\n\",\"author_short\":[\"Verhoef, M.\"],\"id\":\"Verhoef09\",\"bibbaseid\":\"verhoef-modelingandvalidatingdistributedembeddedrealtimecontrolsystems-2009\",\"role\":\"author\",\"urls\":{},\"metadata\":{\"authorlinks\":{}},\"downloads\":0,\"html\":\"\"},{\"bibtype\":\"inproceedings\",\"type\":\"inproceedings\",\"key\":\"Verhoef&07\",\"author\":[{\"firstnames\":[\"Marcel\"],\"propositions\":[],\"lastnames\":[\"Verhoef\"],\"suffixes\":[]},{\"firstnames\":[\"Peter\",\"Gorm\"],\"propositions\":[],\"lastnames\":[\"Larsen\"],\"suffixes\":[]}],\"editor\":[{\"firstnames\":[\"Brian\"],\"propositions\":[],\"lastnames\":[\"Sauser\"],\"suffixes\":[]},{\"firstnames\":[\"Gerrit\"],\"propositions\":[],\"lastnames\":[\"Muller\"],\"suffixes\":[]}],\"title\":\"Interpreting Distributed System Architectures Using VDM++ – A Case Study\",\"booktitle\":\"5th Annual Conference on Systems Engineering Research\",\"publisher\":\"\",\"year\":\"2007\",\"month\":\"March\",\"note\":\"Available at http://www.stevens.edu/engineering/cser/\",\"annote\":\"\",\"comment\":\"I have the sources (PGL)\",\"bibtex\":\"@INPROCEEDINGS{Verhoef&07,\\n  KEY           = \\\"Verhoef\\\\&07\\\",\\n  AUTHOR        = \\\"Marcel Verhoef and Peter Gorm Larsen\\\",\\n  EDITOR        = \\\"Brian Sauser and Gerrit Muller\\\",\\n  TITLE         = \\\"{Interpreting Distributed System Architectures Using VDM++\\n                   -- A Case Study}\\\",\\n  BOOKTITLE     = \\\"5th Annual Conference on Systems Engineering Research\\\",\\n  PUBLISHER     = \\\"\\\",\\n  YEAR          = \\\"2007\\\",\\n  MONTH         = \\\"March\\\",\\n  NOTE          = \\\"{Available at http://www.stevens.edu/engineering/cser/}\\\",\\n  ANNOTE        = \\\"\\\",\\n  COMMENT       = \\\"I have the sources (PGL)\\\"}\\n  \\n% Modeling and Validating Distributed Embedded Real-Time Systems in VDM++, Marcel Verhoef, Peter Gorm Larsen and Jozef Hooman, in Jayadev Misra, Tobias Nipkow and Emil Sekerinski (Eds.), FM 2006: Formal Methods, Proc. 14th Intl. Symposium on Formal Methods, Lecture Notes in Computer Science 4085, Springer-Verlag, 2006, ISBN: 3-540-37215-6. Slides.\\n\\n% Adding Syntax Error Repair to a Java-based Parser Generator, P. van der Spek, N. Plat and C. Pronk. ACM SIGPLAN Notices, 40(4):47-50. April 2005.\",\"author_short\":[\"Verhoef, M.\",\"Larsen, P. G.\"],\"editor_short\":[\"Sauser, B.\",\"Muller, G.\"],\"id\":\"Verhoef&07\",\"bibbaseid\":\"verhoef-larsen-interpretingdistributedsystemarchitecturesusingvdmacasestudy-2007\",\"role\":\"author\",\"urls\":{},\"metadata\":{\"authorlinks\":{}},\"downloads\":0,\"html\":\"\"}],\n      metadata: {\"authorlinks\":{}},\n      ownerID: undefined\n    };\n  </script>\n\n  <script type=\"text/javascript\">\n  var site$;\n  if (typeof $ != 'undefined') {\n    console.log('existing jquery: storing and then restoring');\n    site$ = $;\n    $ = null;\n  }\n  </script>\n\n  <script src=\"https://ajax.googleapis.com/ajax/libs/jquery/2.2.4/jquery.min.js\">\n  </script>\n  <script type=\"text/javascript\">\n  if (site$) {\n    console.log('existing jquery: avoiding conflict and restoring');\n    bb$ = $.noConflict(true);\n    $ = site$;\n  } else {\n    bb$ = $;\n  }\n  </script>\n\n  <script src=\"//bibbase.org/js/bibbase.min.js\"\n          type=\"text/javascript\">\n  </script>\n\n  <script type=\"text/javascript\"\n          src=\"https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.1/MathJax.js?config=TeX-AMS-MML_HTMLorMML\">\n  </script>\n  <script type=\"text/x-mathjax-config\">\n    MathJax.Hub.Config({tex2jax: {inlineMath: [['$','$'], ['\\\\(','\\\\)']]},\n                        skipTags: [\"body\"],\n                        processClass: \"bibbase_paper\"});\n  </script>\n\n  <style>\n  @media print {\n    .dontprint {\n        display: none !important;\n    }\n\n  .bibbase_group {\n    background-color: #E0E0E0;\n    font-style: italic;\n    font-size: larger;\n    text-shadow: 0px 0px 3px #FFFFFF;\n    border-radius: 4px 4px 4px 4px;\n    -moz-border-radius: 4px 4px 4px 4px;\n    -webkit-border-radius: 4px;\n    padding: 5px 40px 5px;\n    margin-top: 10px;\n    margin-bottom: 5px;\n    cursor: pointer;\n  }\n\n  .bibbase_paper {\n    margin-bottom: 5px;\n  }\n\n  }\n  </style>\n\n  \n  <div style=\"float: right; margin-right: 10px; margin-top: 10px; text-align: right; font-size: 12px\">\n    generated by\n    <a href=\"//bibbase.org\"\n       onclick=\"trackOutboundLink('bibbase', 'logo clicked', window.location.href, '//bibbase.org'); return false;\">\n      <img src=\"//bibbase.org/img/logo.svg\"\n           style=\"vertical-align: middle; margin-left: 3px; height: 16px;\"/\n           alt=\"bibbase.org\"\n           title=\"BibBase – The easiest way to maintain your publications page.\"\n        ></a>\n    \n  </div>\n  \n\n  <div id=\"bibbase_header\" class=\"dontprint\" style=\"\">\n\n    <ul class=\"nav nav-pills\" style=\"margin: 0px;\">\n\n      <li class=\"dropdown\" id=\"groupby_dropdown\">\n      <a class=\"dropdown-toggle\"\n         data-toggle=\"dropdown\"\n         href=\"#\">\n          Group by\n          <b class=\"caret\"></b>\n      </a>\n      <ul class=\"dropdown-menu\">\n        <li class=\"groupby year\"><a onclick=\"groupby('year')\">\n            Year</a>\n        </li>\n        <li class=\"groupby author\"><a onclick=\"groupby('author_short')\">\n            Author</a>\n        </li>\n        <li class=\"groupby type\"><a onclick=\"groupby('type')\">\n            Type</a>\n        </li>\n        <li class=\"groupby keyword\"><a onclick=\"groupby('keyword')\">\n            Keyword</a>\n        </li>\n        <li class=\"groupby downloads\"><a onclick=\"groupby('downloads')\">\n            Downloads</a>\n        </li>\n      </ul>\n      </li>\n\n\n      <li class=\"dropdown\" id=\"menu_dropdown\">\n      <a class=\"dropdown-toggle\"\n         data-toggle=\"dropdown\"\n         href=\"#\" alt=\"controls\">\n          <i class=\"fa fa-reorder\" alt=\"controls\"></i>\n          <b class=\"caret\"></b>\n      </a>\n      <ul class=\"dropdown-menu\">\n        <li>\n          <a onclick=\"toggleAll()\">\n            <i class=\"fa fa-chevron-down fa-fw\"></i> Expand/Collapse All\n          </a>\n        </li>\n        <li>\n          <a download=\"overtureweb.bib\" href=\"data:text/bibtex;base64,QFRFQ0hSRVBPUlR7TGFyc2VuJjEwYiwKICBLRVkgICAgICAgICAgID0gIkxhcnNlblwmMTAiLAogIEFVVEhPUiAgICAgICAgPSAiUGV0ZXIgR29ybSBMYXJzZW4gYW5kIEtlbm5ldGggTGF1c2RhaGwgYW5kIE5pY2sgQmF0dGxlIiwKICBUSVRMRSAgICAgICAgID0gIntUaGUgVkRNLTEwIExhbmd1YWdlIE1hbnVhbH0iLAogIElOU1RJVFVUSU9OICAgPSAiVGhlIE92ZXJ0dXJlIE9wZW4gU291cmNlIEluaXRpYXRpdmUiLAogIFlFQVIgICAgICAgICAgPSAiMjAxMCIsCiAgTU9OVEggICAgICAgICA9ICJBcHJpbCIsCiAgTlVNQkVSICAgICAgICA9ICJUUi0yMDEwLTA2IiwKICBBTk5PVEUgICAgICAgID0gIiIsCiAgdXJsX1BhcGVyID0ge2h0dHA6Ly9sYXVzZGFobC5naXRodWIuaW8vb3ZlcnR1cmV0b29sLmdpdGh1Yi5pby9maWxlcy9WRE0xMF9sYW5nX21hbi5wZGZ9LAogIENPTU1FTlQgICAgICAgPSAiUEdMIn0KICAKJUcgVkRNIFRPT0wKCgpAVEVDSFJFUE9SVHtMYXJzZW4mMTBkLAogIEtFWSAgICAgICAgICAgPSAiTGFyc2VuXCYxMCIsCiAgQVVUSE9SICAgICAgICA9ICJQZXRlciBHb3JtIExhcnNlbiBhbmQgS2VubmV0aCBMYXVzZGFobCBhbmQgQXVndXN0byBSaWJlaXJvIGFuZAogICAgICAgICAgICAgICAgICAgU3VuZSBXb2xmZiBhbmQgTmljayBCYXR0bGUiLAogIFRJVExFICAgICAgICAgPSAie092ZXJ0dXJlIFZETS0xMCBUb29sIFN1cHBvcnQ6IFVzZXIgR3VpZGV9IiwKICBJTlNUSVRVVElPTiAgID0gIlRoZSBPdmVydHVyZSBJbml0aWF0aXZlIiwKICBBRERSRVNTICAgICAgID0gInd3dy5vdmVydHVyZXRvb2wub3JnIiwKICBZRUFSICAgICAgICAgID0gIjIwMTAiLAogIE1PTlRIICAgICAgICAgPSAiTWF5IiwKICBOVU1CRVIgICAgICAgID0gIlRSLTIwMTAtMDIiLAogIFNJWkUgICAgICAgICAgPSAiMTAzIiwKICBBTk5PVEUgICAgICAgID0gIiIsCiAgQ09NTUVOVCAgICAgICA9ICJXZSBoYXZlIHRoZSBzb3VyY2VzIFBHTCJ9CiAgCiVUUi0wMDM6IFR1dG9yaWFsIGZvciBPdmVydHVyZS9WRE0tU0wsIFAuIEcuIExhcnNlbiwgSi4gUy4gRml0emdlcmFsZCwgUy4gV29sZmYsIE4uIEJhdHRsZSwgSy4gRy4gTGF1c2RhaGwsIEEuIFJpYmVpcm8sIEsuIEcuIFBpZXJjZSwgUy4gUmlkZGxlLCB2ZXJzaW9uIDIsIEZlYnJ1YXJ5IDIwMTEKJVRSLTAwNDogVHV0b3JpYWwgZm9yIE92ZXJ0dXJlL1ZETSsrLCBQLiBHLiBMYXJzZW4sIEouIFMuIEZpdHpnZXJhbGQsIFMuIFdvbGZmLCBOLiBCYXR0bGUsIEsuIEcuIExhdXNkYWhsLCBBLiBSaWJlaXJvLCBLLiBHLiBQaWVyY2UsIGFuZCBTLiBSaWRkbGUsIHZlcnNpb24gMiwgRmVicnVhcnkgMjAxMQolVFItMDA1OiBUdXRvcmlhbCBmb3IgT3ZlcnR1cmUvVkRNLVJULCBQLiBHLiBMYXJzZW4sIEouIFMuIEZpdHpnZXJhbGQsIFMuIFdvbGZmLCBOLiBCYXR0bGUsIEsuIEcuIExhdXNkYWhsLCBBLiBSaWJlaXJvLCBLLiBHLiBQaWVyY2UsIGFuZCBTLiBSaWRkbGUsIHZlcnNpb24gMiwgRmVicnVhcnkgMjAxMQolVFItMDA2OiBEZXZlbG9wbWVudCBQcm9jZXNzIGZvciBEaXN0cmlidXRlZCBFbWJlZGRlZCBTeXN0ZW1zIHVzaW5nIFZETSwgUC4gRy4gTGFyc2VuLCBTLiBXb2xmZiwgTi4gQmF0dGxlLCBKLiBTLiBGaXR6Z2VyYWxkLCBhbmQgSy4gRy4gUGllcmNlIHZlcnNpb24gMiwgRmVicnVhcnkgMjAxMQolVFItMDA3OiBWRE1KIFRvb2wgU3VwcG9ydDogVXNlciBHdWlkZSwgTmljayBCYXR0bGUgdmVyc2lvbiAxLCBGZWJydWFyeSAyMDExCgoKJQolIGJvb2tzCiUKCiVHIFZETSBUVVRPUiBGT1JNQUwKCgpAQk9PS3tGaXR6Z2VyYWxkJjA1LAogIEtFWSAgICAgICAgICAgPSAiRml0emdlcmFsZFwmMDUiLAogIEFVVEhPUiAgICAgICAgPSAiSm9obiBGaXR6Z2VyYWxkIGFuZCBQZXRlciBHb3JtIExhcnNlbiBhbmQgUGF1bCBNdWtoZXJqZWUgYW5kCiAgICAgICAgICAgICAgICAgICBOaWNvIFBsYXQgYW5kIE1hcmNlbCBWZXJob2VmIiwKICBUSVRMRSAgICAgICAgID0gIntWYWxpZGF0ZWQgRGVzaWducyBmb3IgT2JqZWN0LS1vcmllbnRlZCBTeXN0ZW1zfSIsCiAgUFVCTElTSEVSICAgICA9ICJTcHJpbmdlciwgTmV3IFlvcmsiLAogIFlFQVIgICAgICAgICAgPSAiMjAwNSIsCiAgVVJMICAgICAgICAgICA9ICJodHRwOi8vd3d3LnZkbWJvb2suY29tIiwKICBJU0JOICAgICAgICAgID0gIjEtODUyMzMtODgxLTQiLAogIEFOTk9URSAgICAgICAgPSAiIiwKICBDT01NRU5UICAgICAgID0gIlBHTCJ9CiAgCiUgVmFsaWRhdGVkIERlc2lnbnMgZm9yIE9iamVjdC1vcmllbnRlZCBTeXN0ZW1zIChpbiBKYXBhbmVzZSksIEhpcm9zaGkgU2Frb2gsIDIwMTAsIElTQk4tMTA6IDQ3OTgxMTk2MVggKEFtYXpvbiBsaW5rKS4KCiVHIFZETSBUVVRPUiBGT1JNQUwKCgpAQk9PS3tGaXR6Z2VyYWxkJjA5LAogIEtFWSAgICAgICAgICAgPSAiRml0emdlcmFsZFwmMDkiLAogIEFVVEhPUiAgICAgICAgPSAiSm9obiBGaXR6Z2VyYWxkIGFuZCBQZXRlciBHb3JtIExhcnNlbiIsCiAgVElUTEUgICAgICAgICA9ICJ7TW9kZWxsaW5nIFN5c3RlbXMgLS0gUHJhY3RpY2FsIFRvb2xzIGFuZCBUZWNobmlxdWVzIGluCiAgICAgICAgICAgICAgICAgICAgU29mdHdhcmUgRGV2ZWxvcG1lbnR9IiwKICBQVUJMSVNIRVIgICAgID0gIkNhbWJyaWRnZSBVbml2ZXJzaXR5IFByZXNzIiwKICBBRERSRVNTICAgICAgID0gIlRoZSBFZGluYnVyZ2ggQnVpbGRpbmcsIENhbWJyaWRnZSBDQjIgMlJVLCBVSyIsCiAgWUVBUiAgICAgICAgICA9ICIyMDA5IiwKICBFRElUSU9OICAgICAgID0gIntTZWNvbmR9IiwKICBOT1RFICAgICAgICAgID0gIntJU0JOIDAtNTIxLTYyMzQ4LTB9IiwKICBBTk5PVEUgICAgICAgID0gIiIsCiAgQ09NTUVOVCAgICAgICA9ICJJIGhhdmUgdGhlIHNvdXJjZSBQR0wifQogIAolRm9ybWFsIFNwZWNpZmljYXRpb24gYnkgVkRNKysgKGluIEphcGFuZXNlKSwgRHIuIEZ1eXVraSBJc2hpa2F3YSwgSVNCTi0xMDogNDc2NDkwNDA5OC4gKEFtYXpvbiBsaW5rKS4KCiUyMDEzCgolIElQQS9TRUMgSW52ZXN0aWdhdGl2ZSBSZXBvcnQ6IFN1Y2Nlc3MgU3RvcmllcyBvZiBGb3JtYWwgTWV0aG9kcyBpbiBTdHJpY3QgU3BlY2lmaWNhdGlvbiAoaW4gSmFwYW5lc2UpLCBIaXJvc2hpIFNha29oIGFuZCBUb21vaGlybyBPZGEsIEphbnVhcnkgMjAxMy4KCiVHIFZETSBBTExPWSBUT09MCgoKQGluY29sbGVjdGlvbntMYXVzZGFobCYxMywKICBLRVkgICAgICAgPSAiTGF1c2RhaGxcJjEzIiwKICB5ZWFyCQk9ezIwMTN9LAogIGlzYm4JCT17OTc4LTMtNjQyLTM4NjEyLTF9LAogIGJvb2t0aXRsZQk9e0ludGVncmF0ZWQgRm9ybWFsIE1ldGhvZHN9LAogIHZvbHVtZQk9ezc5NDB9LAogIHNlcmllcwk9e0xlY3R1cmUgTm90ZXMgaW4gQ29tcHV0ZXIgU2NpZW5jZX0sCiAgZWRpdG9yCT17Sm9obnNlbiwgRWluYXIgQnJvY2ggYW5kIFBldHJlLCBMdWlnaWF9LAogIGRvaQkJPXsxMC4xMDA3Lzk3OC0zLTY0Mi0zODYxMy04XzR9LAogIHRpdGxlCQk9IntUcmFuc2xhdGluZyBWRE0gdG8gQWxsb3l9IiwKICB1cmwJCT17aHR0cDovL2R4LmRvaS5vcmcvMTAuMTAwNy85NzgtMy02NDItMzg2MTMtOF80fSwKICBwdWJsaXNoZXIJPXtTcHJpbmdlciBCZXJsaW4gSGVpZGVsYmVyZ30sCiAgYXV0aG9yCT17TGF1c2RhaGwsIEtlbm5ldGh9LAogIHBhZ2VzCQk9ezQ2LTYwfSwKICBub3RlCQk9ezEwdGggSW50ZXJuYXRpb25hbCBDb25mZXJlbmNlLCBJRk0gMjAxM30sCn0KCiUgMjAxMgoKCgpASU5QUk9DRUVESU5HU3tDaHJpc3RpYW5zZW4mMTJhLAogIEtFWSAJCT0gIkNocmlzdGlhbnNlblwmMTIiLAogIEFVVEhPUgk9ICJNYXJ0aW4gUGV0ZXIgQ2hyaXN0aWFuc2VuIGFuZCBLaW0gQmplcmdlIGFuZCBHYXJldGggRWR3YXJkcyBhbmQgUGV0ZXIgR29ybSBMYXJzZW4iLAogIFRJVExFCQk9ICJUb3dhcmRzIGEgTWV0aG9kb2xvZ3kgZm9yIE1vZGVsbGluZyBhbmQgVmFsaWRhdGlvbiBvZiBhbiBBZ3JpY3VsdHVyYWwgVmVoaWNsZSdzIER5bmFtaWNzIGFuZCBDb250cm9sIiwKICBFRElUT1IgICAgPSAiU2VyZ2lvIEp1bmNvIiwKICBQQUdFUyAgICAgPSAiMTEyLTExOSIsCiAgWUVBUgkJPSAiMjAxMiIsCiAgTU9OVEgJCT0gIlNlcHRlbWJlciIsCiAgQk9PS1RJVExFCT0gIntUaGUgNnRoIEludGVybmF0aW9uYWwgQ29uZmVyZW5jZSBvbiBJbnRlZ3JhdGVkIE1vZGVsaW5nIGFuZCBBbmFseXNpcyBpbiBBcHBsaWVkIENvbnRyb2wgYW5kIEF1dG9tYXRpb259IiwKICBTRVJJRVMJPSB7SU1BQUNBfQp9CgolQSBSaWdvcm91cyBBcHByb2FjaCB0byB0aGUgRGVzaWduIG9mIFJlc2lsaWVudCBDeWJlci1waHlzaWNhbCBTeXN0ZW1zIHRocm91Z2ggQ28tU2ltdWxhdGlvbiBKb2huIEZpdHpnZXJhbGQsIEtlbiBQaWVyY2UsIENhcmwgR2FtYmxlLCBpbiBEZXBlbmRhYmxlIFN5c3RlbXMgYW5kIE5ldHdvcmtzIFdvcmtzaG9wcyAoRFNOLVcpIDIwMTIgKFdPUkNTKSwgcHJlc2VudGVkIGluIEp1bmUgMjAxMiwgQm9zdG9uLCBNQSwgVVNBLgoKCgpASU5QUk9DRUVESU5HU3tXb2xmZjEyYSwKICBLRVkgICAgICAgICAgID0gIldvbGZmMTIiLAogIEFVVEhPUiAgICAgICAgPSAiU3VuZSBXb2xmZiIsCiAgVElUTEUgICAgICAgICA9ICJ7U2NydW0gR29lcyBGb3JtYWw6IEFnaWxlIE1ldGhvZHMgZm9yIFNhZmV0eS1Dcml0aWNhbCBTeXN0ZW1zfSIsCiAgQk9PS1RJVExFICAgICA9ICJJQ1NFIDIwMTI6IFByb2NlZWRpbmdzIG9mIHRoZSAzNHRoIEludGVybmF0aW9uYWwgQ29uZmVyZW5jZSBvbiBTb2Z0d2FyZQoJCQkJICAgRW5naW5lZXJpbmciLAogIE5PVEUJCQk9ICJ7V29ya3Nob3Agb24gRm9ybWFsIE1ldGhvZHMgaW4gU29mdHdhcmUgRW5naW5lZXJpbmc6IFJpZ29yb3VzCgkJCQkgICBhbmQgQWdpbGUgQXBwcm9hY2hlcywgRm9ybVNFUkEgMjAxMn0iLAogIFlFQVIgICAgICAgICAgPSAiMjAxMiIsCiAgTU9OVEggICAgICAgICA9ICJKdW5lIiwKICBQQUdFUyAgICAgICAgID0gIjIzLS0yOSIsCiAgU0laRQkJCT0gIjciLAogIElTQk4gICAgICAgICAgPSAiOTc4LTEtNDY3My0xOTA2LTUiLAogIEFOTk9URSAgICAgICAgPSAiIiwKICBDT01NRU5UICAgICAgID0gIiJ9CiAgCgoKQElOUFJPQ0VFRElOR1N7TmllbHNlbiYxMiwKICBLRVkJCQk9ICJOaWVsc2VuXCYxMiIsCiAgQVVUSE9SCQk9ICJDbGF1cyBCYWxsZWdhYXJkIE5pZWxzZW4gYW5kIEtlbm5ldGggTGF1c2RhaGwgYW5kIFBldGVyIEdvcm0gTGFyc2VuIiwKICBUSVRMRQkJCT0gIntDb21iaW5pbmcgVkRNIHdpdGggRXhlY3V0YWJsZSBDb2RlfSIsCiAgYm9va3RpdGxlICAJPSAie0Fic3RyYWN0IFN0YXRlIE1hY2hpbmVzLCBBbGxveSwgQiwgVkRNLCBhbmQgWn0iLAogIHZvbHVtZQkJPSB7NzMxNn0sCiAgZWRpdG9yCQk9IHtEZXJyaWNrLCBKb2huIGFuZCBGaXR6Z2VyYWxkLCBKb2huIGFuZCBHbmVzaSwgU3RlZmFuaWEgYW5kIEtodXJzaGlkLCBTYXJmcmF6IGFuZCBMZXVzY2hlbCwgTWljaGFlbCBhbmQgUmVldmVzLCBTdGV2ZSBhbmQgUmljY29iZW5lLCBFbHZpbmlhfSwKICBZRUFSCQkJPSAiMjAxMiIsCiAgbG9jYXRpb24gCQk9IHtQaXNhLCBJdGFseX0sCiAgcGFnZXMgCQk9IHsyNjYtLTI3OX0sCiAgbnVtcGFnZXMgCQk9IHsxNH0sCiAgU0VSSUVTICAgICAgICA9ICJMZWN0dXJlIE5vdGVzIGluIENvbXB1dGVyIFNjaWVuY2UiLAogIFZPTFVNRSAgICAgICAgPSAiNzMxNiIsCiAgcHVibGlzaGVyIAk9IHtTcHJpbmdlci1WZXJsYWd9LAogIGFkZHJlc3MgCQk9IHtCZXJsaW4sIEhlaWRlbGJlcmd9LAogIE5PVEUgICAgICAgCT0gIntJU0JOIDk3OC0zLTY0Mi0zMDg4NC0wfSIsCiAgdXJsIAkJCT0ge2h0dHA6Ly9keC5kb2kub3JnLzEwLjEwMDcvOTc4LTMtNjQyLTMwODg1LTdfMTl9LAogIH0KICAKCgpASU5QUk9DRUVESU5HU3tQYXluZSYxMmEsCiAgS0VZICAgICAgICAgICA9ICJQYXluZSYxMmEiLAogIEFVVEhPUiAgICAgICAgPSAiUmljaGFyZCBQYXluZSBhbmQgSmVyZW15IEJyeWFucyBhbmQgSm9obiBGaXR6Z2VyYWxkIGFuZCBTdGV2ZSBSaWRkbGUiLAogIFRJVExFICAgICAgICAgPSAie0ludGVyZmFjZSBTcGVjaWZpY2F0aW9uIGZvciBTeXN0ZW0tb2YtU3lzdGVtcyBBcmNoaXRlY3R1cmVzfSIsCiAgQk9PS1RJVExFICAgICA9ICJQcm9jZWVkaW5ncyBvZiB0aGUgN3RoIEludGVybmF0aW9uYWwgQ29uZmVyZW5jZSBvbgogICAgICAgICAgICAgICAgICAgU3lzdGVtIG9mIFN5c3RlbSBFbmdpbmVlcmluZywgSUVFRSBTb1NFIDIwMTIiLAogIFBVQkxJU0hFUiAgICAgPSAie0lFRUV9IiwKICBZRUFSICAgICAgICAgID0gMjAxMiwKICBNT05USCAgICAgICAgID0gIkp1bHkifQogIAoKCkBpbnByb2NlZWRpbmdze0ZpdHpnZXJhbGQmMTJjLAogIGtleSAgICAgICA9ICJGaXR6Z2VyYWxkXCYxMmMiLAogIGF1dGhvciAgICA9IHtKb2huIFMuIEZpdHpnZXJhbGQgYW5kCiAgICAgICAgICAgICAgIEplcmVteSBCcnlhbnMgYW5kCiAgICAgICAgICAgICAgIFJpY2hhcmQgUGF5bmV9LAogIHRpdGxlICAgICA9IHtBIEZvcm1hbCBNb2RlbC1CYXNlZCBBcHByb2FjaCB0byBFbmdpbmVlcmluZwpTeXN0ZW1zLW9mLVN5c3RlbXN9LAogIGVkaXRvciAgICA9IHtMdWlzIE0uIENhbWFyaW5oYS1NYXRvcyBhbmQKICAgICAgICAgICAgICAgTGFpIFh1IGFuZAogICAgICAgICAgICAgICBIYW1pZGVoIEFmc2FybWFuZXNofSwKICBib29rdGl0bGUgPSB7Q29sbGFib3JhdGl2ZSBOZXR3b3JrcyBpbiB0aGUgSW50ZXJuZXQgb2YgU2VydmljZXMgLSAxM3RoCiAgICAgICAgICAgICAgIElGSVAgV0cgNS41IFdvcmtpbmcgQ29uZmVyZW5jZSBvbiBWaXJ0dWFsIEVudGVycHJpc2VzLApQUk8tVkUgMjAxMiwgQm91cm5lbW91dGgsIFVLLCBPY3RvYmVyIDEtMywgMjAxMi4gUHJvY2VlZGluZ3N9LAogIHB1Ymxpc2hlciA9IHtTcHJpbmdlcn0sCiAgc2VyaWVzICAgID0ge0lGSVAgQWR2YW5jZXMgaW4gSW5mb3JtYXRpb24gYW5kIENvbW11bmljYXRpb24gVGVjaG5vbG9neX0sCiAgdm9sdW1lICAgID0gezM4MH0sCiAgeWVhciAgICAgID0gezIwMTJ9LAogIHBhZ2VzICAgICA9IHs1My02Mn0sCiAgZWUgICAgICAgID0ge2h0dHA6Ly9keC5kb2kub3JnLzEwLjEwMDcvOTc4LTMtNjQyLTMyNzc1LTlfNn0sCiAgYmlic291cmNlID0ge0RCTFAsIGh0dHA6Ly9kYmxwLnVuaS10cmllci5kZX0KfQoKCgpASU5QUk9DRUVESU5HU3tMYXJzZW4mMTJhLAogIEtFWSAgICAgICAgICAgPSAiTGFyc2VuXCYxMiIsCiAgQVVUSE9SICAgICAgICA9ICJQZXRlciBHb3JtIExhcnNlbiBhbmQgSm9leSBXLlwgQ29sZW1hbiBhbmQgSm9obiBGaXR6Z2VyYWxkIiwKICBFRElUT1IgICAgICAgID0gIkFsZXhhbmRlciBLLiBQZXRyZW5rbyIsCiAgVElUTEUgICAgICAgICA9ICJ7R2V0dGluZyBTb2Z0d2FyZSBFbmdpbmVlcmluZyBvdXQgb2YgSXNvbGF0aW9ufSIsCiAgQk9PS1RJVExFICAgICA9ICJTWVJDb1NFIFNvZnR3YXJlIEVuZ2luZWVyaW5nIENvbGxvcXVpdW0iLAogIEFERFJFU1MgICAgICAgPSAiUGVybSwgUnVzc2lhIiwKICBZRUFSICAgICAgICAgID0gIjIwMTIiLAogIE1PTlRIICAgICAgICAgPSAiTWF5IiwKICBOT1RFICAgICAgICAgID0gIklTQk4gOTc4LTUtOTE0NzQtMDE5LTgiLAogIFBBR0VTICAgICAgICAgPSAiIiwKICBBTk5PVEUgICAgICAgID0gIiIsCiAgQ09NTUVOVCAgICAgICA9ICJCSUIgUEdMIEkgYWxzbyBoYXZlIHRoZSBzb3VyY2VzIn0KICAKJTIwMTEKCgoKQElOUFJPQ0VFRElOR1N7TGF1c2RhaGwmMTEsCiAgS0VZICAgICAgICAgICA9ICJMYXVzZGFobFwmMTEiLAogIEFVVEhPUiAgICAgICAgPSAiS2VubmV0aCBMYXVzZGFobCBhbmQgUGV0ZXIgR29ybSBMYXJzZW4gYW5kIE5pY2sgQmF0dGxlIiwKICB0aXRsZSAJCT0gIntBIERldGVybWluaXN0aWMgSW50ZXJwcmV0ZXIgU2ltdWxhdGluZyBBIERpc3RyaWJ1dGVkIHJlYWwgdGltZSBzeXN0ZW0gdXNpbmcgVkRNfSIsCiAgYm9va3RpdGxlIAk9IHtQcm9jZWVkaW5ncyBvZiB0aGUgMTN0aCBpbnRlcm5hdGlvbmFsIGNvbmZlcmVuY2Ugb24gRm9ybWFsIG1ldGhvZHMgYW5kIHNvZnR3YXJlIGVuZ2luZWVyaW5nfSwKICBzZXJpZXMJCT0ge0xlY3R1cmUgTm90ZXMgaW4gQ29tcHV0ZXIgU2NpZW5jZX0sCiAgdm9sdW1lCQk9IHs2OTkxfSwKICBlZGl0b3IJCT0ge1FpbiwgU2hlbmdjaGFvIGFuZCBRaXUsIFpvbmd5YW59LAogIFlFQVIgICAgICAgICAgPSAiMjAxMSIsCiAgTU9OVEggICAgICAgICA9ICJPY3RvYmVyIiwKICBub3RlICAgICAgICAJPSAie0lTQk4gOTc4LTMtNjQyLTI0NTU4LTl9IiwKICAgbG9jYXRpb24gCT0ge0R1cmhhbSwgVUt9LAogcGFnZXMgCQkJPSB7MTc5LS0xOTR9LAogbnVtcGFnZXMgCQk9IHsxNn0sCiB1cmwgCQkJPSB7aHR0cDovL2RsLmFjbS5vcmcvY2l0YXRpb24uY2ZtP2lkPTIwNzUwODkuMjA3NTEwN30sCiAgIHB1Ymxpc2hlciAJPSB7U3ByaW5nZXItVmVybGFnfSwKIGFkZHJlc3MgCQk9IHtCZXJsaW4sIEhlaWRlbGJlcmd9LAogIH0KICAKCgpASU5QUk9DRUVESU5HU3tQaWVyY2UmMTEsCiAgS0VZID0ge1BpZXJjZVwmMTF9LAogIEFVVEhPUiA9IHtLZW4gUGllcmNlIGFuZCBKb2huIEZpdHpnZXJhbGQgYW5kIENhcmwgR2FtYmxlfSwKICBUSVRMRSA9IHtNb2RlbGxpbmcgRmF1bHRzIGFuZCBGYXVsdCBUb2xlcmFuY2UgTWVjaGFuaXNtcyBpbiBhIFBhcGVyIFBpbmNoIENvLSBtb2RlbH0sCiAgQk9PS1RJVExFID0ge1Byb2NlZWRpbmdzIG9mIHRoZSBFUkNJTS9FV0lDUy9DeWJlci1waHlzaWNhbCBTeXN0ZW1zIFdvcmtzaG9wIGF0IFNhZmVDb21wIDIwMTEsIE5hcGxlcywgSXRhbHkgKHRvIGFwcGVhcil9LAogIFlFQVIgPSB7MjAxMX0sCiAgTU9OVEggPSB7U2VwdGVtYmVyfSwKICBQVUJMSVNIRVIgPSB7RVJDSU19Cn0KCgolIFZETS1TTCwgVkRNKysgU2ltcGxlIFJlZmVyZW5jZSAoaW4gSmFwYW5lc2UpLCBEci4gRnV5dWtpIElzaGlrYXdhLCBKdW5lIDIwMTEuCgolVkRNIHNwZWNpZmljYXRpb24gYXMgU3RydWN0dXJlZCBKYXBhbmVzZSBTcGVjaWZpY2F0aW9uIChpbiBKYXBhbmVzZSksIFNoaW4gU2FoYXJhLCBTRUMgam91cm5hbCwgVm9sLiAyNi4sIDMxdGggTWFyY2gsIDIwMTEsIHBwLiAyMy0yNywgSVNTTiAxMzQ5LTg2MjIuCgolQW5zd2VycyB0byBGcmVxdWVudGx5IEFza2VkIFF1ZXN0aW9ucyBmb3IgdGhlIFByYWN0aWNlIG9mIEZvcm1hbCBNZXRob2RzIChpbiBKYXBhbmVzZSksIERyLiBUYXJvIEt1cml0YSwgU0VDIGpvdXJuYWwsIFZvbC4gMjYuLCAzMXRoIE1hcmNoLCAyMDExLCBwcC4gMzQtMzksIElTU04gMTM0OS04NjIyLgoKJTIwMTAKCgoKQElOUFJPQ0VFRElOR1N7UmliZWlybyYxMCwKICBLRVkgICAgICAgICAgID0gIlJpYmVpcm9cJjEwIiwKICBBVVRIT1IgICAgICAgID0gIkF1Z3VzdG8gUmliZWlybyBhbmQgUGV0ZXIgR29ybSBMYXJzZW4iLAogIEVESVRPUiAgICAgICAgPSAiSmluIFNvbmcgYW5kIEh1aWJpYW8iLAogIFRJVExFICAgICAgICAgPSAie1Byb29mIE9ibGlnYXRpb24gR2VuZXJhdGlvbiBhbmQgRGlzY2hhcmdpbmcgZm9yCiAgICAgICAgICAgICAgICAgICBSZWN1cnNpdmUgRGVmaW5pdGlvbnMgaW4ge1ZETX19IiwKICBCT09LVElUTEUgICAgID0gIlRoZSAxMnRoIEludGVybmF0aW9uYWwgQ29uZmVyZW5jZSBvbiBGb3JtYWwgRW5naW5lZXJpbmcKICAgICAgICAgICAgICAgICAgIE1ldGhvZHMgKElDRkVNIDIwMTApIiwKICBQVUJMSVNIRVIgICAgID0gIlNwcmluZ2VyLVZlcmxhZyIsCiAgWUVBUiAgICAgICAgICA9ICIyMDEwIiwKICBNT05USCAgICAgICAgID0gIk5vdmVtYmVyIiwKICBBTk5PVEUgICAgICAgID0gIiIsCiAgQ09NTUVOVCAgICAgICA9ICJJIGhhdmUgdGhlIHNvdXJjZXMgUEdMIn0KICAKCgpAVEVDSFJFUE9SVHtGaXR6Z2VyYWxkJjEwYSwKICBLRVkgICAgICAgICAgID0gIkZpdHpnZXJhbGRcJjEwYSIsCiAgQVVUSE9SICAgICAgICA9IHtKb2huIEZpdHpnZXJhbGQgYW5kIFBldGVyIEdvcm0gTGFyc2VuIGFuZCBLZW4gUGllcmNlIGFuZCBNYXJjZWwgVmVyaG9lZiBhbmQgU3VuZSBXb2xmZn0sCiAgVElUTEUgICAgICAgICA9ICJ7Q29sbGFib3JhdGl2ZSBNb2RlbGxpbmcgYW5kIENvLXNpbXVsYXRpb24gaW4gdGhlIERldmVsb3BtZW50IG9mIERlcGVuZGFibGUgRW1iZWRkZWQgU3lzdGVtc30iLAogIElOU1RJVFVUSU9OICAgPSAiU2Nob29sIG9mIENvbXB1dGluZyBTY2llbmNlLCBOZXdjYXN0bGUgVW5pdmVyc2l0eSIsCiAgWUVBUiAgICAgICAgICA9ICIyMDEwIiwKICBNT05USCAgICAgICAgID0gIkp1bHkiLAogIE5VTUJFUiAgICAgICAgPSAie0NTLVRSLTEyMTN9IiwKICBVUkwgICAgICAgICAgID0gImh0dHA6Ly93d3cuY3MubmNsLmFjLnVrL3B1YmxpY2F0aW9ucy90cnMvcGFwZXJzLzEyMTMucGRmIn0KICAKCgpASU5QUk9DRUVESU5HU3tMYXJzZW4mMTBnLAogIEtFWSAgICAgICAgICAgPSAiTGFyc2VuXCYxMCIsCiAgQVVUSE9SICAgICAgICA9ICJQZXRlciBHb3JtIExhcnNlbiBhbmQgSm9obiBGaXR6Z2VyYWxkIGFuZCBTdW5lIFdvbGZmIiwKICBFRElUT1IgICAgICAgID0gIlN0ZWZhbiBHcnVuZXIgYW5kIEJlcm5oYXJkIFJ1bXBlIiwKICBUSVRMRSAgICAgICAgID0gIkFyZSBGb3JtYWwgTWV0aG9kcyBSZWFkeSBmb3IgQWdpbGl0eT8gQSBSZWFsaXR5IENoZWNrIiwKICBCT09LVElUTEUgICAgID0gIjJuZCBJbnRlcm5hdGlvbmFsIFdvcmtzaG9wIG9uIEZvcm1hbCBNZXRob2RzIGFuZCBBZ2lsZQogICAgICAgICAgICAgICAgICAgTWV0aG9kcyIsCiAgUFVCTElTSEVSICAgICA9ICJMZWN0dXJlIE5vdGVzIGluIEluZm9ybWF0aWNzIiwKICBQQUdFUyAgICAgICAgID0gIjEzLS0yNSIsCiAgWUVBUiAgICAgICAgICA9ICIyMDEwIiwKICBNT05USCAgICAgICAgID0gIlNlcHRlbWJlciIsCiAgTk9URSAgICAgICAgICA9ICJJU1NIIDE2MTctNTQ2OCIsCiAgQU5OT1RFICAgICAgICA9ICIiLAogIENPTU1FTlQgICAgICAgPSAiQklCIEkgaGF2ZSB0aGUgc291cmNlcyBQR0wifQogIAoKCkBJTlBST0NFRURJTkdTe0xhcnNlbiYwOWEsCiAgS0VZICAgICAgICAgICA9ICJMYXJzZW5cJjA5IiwKICBBVVRIT1IgICAgICAgID0gIlBldGVyIEdvcm0gTGFyc2VuIGFuZCBLZW5uZXRoIExhdXNkYWhsIGFuZCBOaWNrIEJhdHRsZSIsCiAgVElUTEUgICAgICAgICA9ICJ7Q29tYmluYXRvcmlhbCBUZXN0aW5nIGZvciBWRE0rK30iLAogIEJPT0tUSVRMRSAgICAgPSAiU3VibWl0dGVkIGZvciBwdWJsaWNhdGlvbiIsCiAgWUVBUiAgICAgICAgICA9ICIyMDA5IiwKICBNT05USCAgICAgICAgID0gIkRlY2VtYmVyIiwKICBOT1RFICAgICAgICAgID0gIk91dGRhdGVkIGJ5IFxjaXRle0xhcnNlbiYxMGN9IiwKICBBTk5PVEUgICAgICAgID0gIiIsCiAgQ09NTUVOVCAgICAgICA9ICJPdXRkYXRlZCBieSBcY2l0ZXtMYXJzZW4mMTBjfSJ9CiAgCgoKQElOUFJPQ0VFRElOR1N7QnJvZW5pbmsmMTAsCiAgS0VZICAgICAgICAgICA9ICJCcm9lbmlua1wmMTAiLAogIEFVVEhPUiAgICAgICAgPSAiQnJvZW5pbmssIEouIEYuIGFuZCBMYXJzZW4sIFAuIEcuIGFuZCAgVmVyaG9lZiwgTS4gYW5kCiAgICAgICAgICAgICAgICAgICBLbGVpam4sIEMuIGFuZCAgSm92YW5vdmljLCBELiBhbmQgUGllcmNlLCBLLiBhbmQKICAgICAgICAgICAgICAgICAgIFdvdXRlcnMgRi4iLAogIFRJVExFICAgICAgICAgPSAie0Rlc2lnbiBTdXBwb3J0IGFuZCBUb29saW5nIGZvciBEZXBlbmRhYmxlIEVtYmVkZGVkIENvbnRyb2wgU29mdHdhcmV9IiwKICBCT09LVElUTEUgICAgID0gIlByb2NlZWRpbmdzIG9mIFNlcmVuZSAyMDEwIEludGVybmF0aW9uYWwgV29ya3Nob3Agb24KICAgICAgICAgICAgICAgICAgIFNvZnR3YXJlIEVuZ2luZWVyaW5nIGZvciBSZXNpbGllbnQgU3lzdGVtcyIsCiAgUFVCTElTSEVSICAgICA9ICJBQ00iLAogIFlFQVIgICAgICAgICAgPSAiMjAxMCIsCiAgTU9OVEggICAgICAgICA9ICJBcHJpbCIsCiAgUEFHRVMgICAgICAgICA9ICI3Ny0tODIiLAogIEFOTk9URSAgICAgICAgPSAiIiwKICBDT01NRU5UICAgICAgID0gIkkgaGF2ZSB0aGUgc291cmNlcyAoUEdMKSJ9CiAgCiUgUHJvdmluZyBDb25zaXN0ZW5jeSBvZiBWRE0gbW9kZWxzIHVzaW5nIEhPTCwgU2FuZGVyIEQuIFZlcm1vbGVuLCBKb3plZiBIb29tYW4gYW5kIFBldGVyIEdvcm0gTGFyc2VuLCBpbiBQcm9jZWVkaW5ncyBvZiB0aGUgMjAxMCBBQ00gU3ltcG9zaXVtIG9uIEFwcGxpZWQgQ29tcHV0aW5nLCBBQ00sIE1hcmNoIDIwMTAuCgolIEZvcm1hbCBTZW1hbnRpY3Mgb2YgYSBWRE0gRXh0ZW5zaW9uIGZvciBEaXN0cmlidXRlZCBFbWJlZGRlZCBTeXN0ZW1zLCBKb3plZiBIb29tYW4gYW5kIE1hcmNlbCBWZXJob2VmLCBpbiBELiBEYW1zIGFuZCBVLiBIYW5uZW1hbm4gYW5kIE0uIFN0ZWZmZW4gKGVkcyk6IFcuUC4gZGUgUm9ldmVyIEZlc3RzY2hyaWZ0LCBMTkNTIDU5MzAsIHBwIDE0Mi0xNjEsIDIwMTAuCgoKCkBBUlRJQ0xFe0xhcnNlbiYxMGEsCiAgS0VZICAgICAgICAgICA9ICJMYXJzZW5cJjEwIiwKICBBVVRIT1IgICAgICAgID0gIlBldGVyIEdvcm0gTGFyc2VuIGFuZCBOaWNrIEJhdHRsZSBhbmQgTWlndWVsIEZlcnJlaXJhCiAgICAgICAgICAgICAgICAgICBhbmQgSm9obiBGaXR6Z2VyYWxkIGFuZCBLZW5uZXRoIExhdXNkYWhsIGFuZCBNYXJjZWwKICAgICAgICAgICAgICAgICAgIFZlcmhvZWYiLAogIFRJVExFICAgICAgICAgPSAie1RoZSBPdmVydHVyZSBJbml0aWF0aXZlIC0tIEludGVncmF0aW5nIFRvb2xzIGZvciBWRE19IiwKICBKT1VSTkFMICAgICAgID0ge1NJR1NPRlQgU29mdHcuIEVuZy4gTm90ZXN9LAogIFlFQVIgICAgICAgICAgPSAiMjAxMCIsCiAgTU9OVEggICAgICAgICA9ICJKYW51YXJ5IiwKICBWT0xVTUUgICAgICAgID0gIjM1IiwKICBOVU1CRVIgICAgICAgID0gIjEiLAogIFBBR0VTICAgICAgICAgPSAiMS0tNiIsCiAgU0laRSAgICAgICAgICA9ICI2IiwKICBBTk5PVEUgICAgICAgID0gIiIsCiAgbnVtcGFnZXMgPSB7Nn0sCiAgaXNzbiA9IHswMTYzLTU5NDh9LAogIGFkZHJlc3MgPSB7TmV3IFlvcmssIE5ZLCBVU0F9LAogIHB1Ymxpc2hlciA9IHtBQ019LAogIFVSTAkJCT0gImh0dHA6Ly9kb2kuYWNtLm9yZy8xMC4xMTQ1LzE2Njg4NjIuMTY2ODg2NCJ9CiAgCiUyMDA5CgoKCkBQSERUSEVTSVN7VmVyaG9lZjA5LAogIEtFWSAgICAgICAgICAgPSAiVmVyaG9lZjA5IiwKICBBVVRIT1IgICAgICAgID0gIk1hcmNlbCBWZXJob2VmIiwKICBUSVRMRSAgICAgICAgID0gIntNb2RlbGluZyBhbmQgVmFsaWRhdGluZyBEaXN0cmlidXRlZCBFbWJlZGRlZCBSZWFsLVRpbWUKICAgICAgICAgICAgICAgICAgICBDb250cm9sIFN5c3RlbXN9IiwKICBTQ0hPT0wgICAgICAgID0gIlJhZGJvdWQgVW5pdmVyc2l0eSBOaWptZWdlbiIsCiAgWUVBUiAgICAgICAgICA9ICIyMDA5IiwKICBOVU1CRVIgICAgICAgID0gIlJVLiAyMDA5LTAxIiwKICBBTk5PVEUgICAgICAgICAgPSAie0lTQk4gOTc4LTkwLTkwMjM3MDUtM30iLAogIENPTU1FTlQgICAgICAgPSAiSSBoYXZlIGEgY29weSBQR0wifQogIAoKCkBJTlBST0NFRURJTkdTe1ZlcmhvZWYmMDcsCiAgS0VZICAgICAgICAgICA9ICJWZXJob2VmXCYwNyIsCiAgQVVUSE9SICAgICAgICA9ICJNYXJjZWwgVmVyaG9lZiBhbmQgUGV0ZXIgR29ybSBMYXJzZW4iLAogIEVESVRPUiAgICAgICAgPSAiQnJpYW4gU2F1c2VyIGFuZCBHZXJyaXQgTXVsbGVyIiwKICBUSVRMRSAgICAgICAgID0gIntJbnRlcnByZXRpbmcgRGlzdHJpYnV0ZWQgU3lzdGVtIEFyY2hpdGVjdHVyZXMgVXNpbmcgVkRNKysKICAgICAgICAgICAgICAgICAgIC0tIEEgQ2FzZSBTdHVkeX0iLAogIEJPT0tUSVRMRSAgICAgPSAiNXRoIEFubnVhbCBDb25mZXJlbmNlIG9uIFN5c3RlbXMgRW5naW5lZXJpbmcgUmVzZWFyY2giLAogIFBVQkxJU0hFUiAgICAgPSAiIiwKICBZRUFSICAgICAgICAgID0gIjIwMDciLAogIE1PTlRIICAgICAgICAgPSAiTWFyY2giLAogIE5PVEUgICAgICAgICAgPSAie0F2YWlsYWJsZSBhdCBodHRwOi8vd3d3LnN0ZXZlbnMuZWR1L2VuZ2luZWVyaW5nL2NzZXIvfSIsCiAgQU5OT1RFICAgICAgICA9ICIiLAogIENPTU1FTlQgICAgICAgPSAiSSBoYXZlIHRoZSBzb3VyY2VzIChQR0wpIn0KICAKJSBNb2RlbGluZyBhbmQgVmFsaWRhdGluZyBEaXN0cmlidXRlZCBFbWJlZGRlZCBSZWFsLVRpbWUgU3lzdGVtcyBpbiBWRE0rKywgTWFyY2VsIFZlcmhvZWYsIFBldGVyIEdvcm0gTGFyc2VuIGFuZCBKb3plZiBIb29tYW4sIGluIEpheWFkZXYgTWlzcmEsIFRvYmlhcyBOaXBrb3cgYW5kIEVtaWwgU2VrZXJpbnNraSAoRWRzLiksIEZNIDIwMDY6IEZvcm1hbCBNZXRob2RzLCBQcm9jLiAxNHRoIEludGwuIFN5bXBvc2l1bSBvbiBGb3JtYWwgTWV0aG9kcywgTGVjdHVyZSBOb3RlcyBpbiBDb21wdXRlciBTY2llbmNlIDQwODUsIFNwcmluZ2VyLVZlcmxhZywgMjAwNiwgSVNCTjogMy01NDAtMzcyMTUtNi4gU2xpZGVzLgoKJSBBZGRpbmcgU3ludGF4IEVycm9yIFJlcGFpciB0byBhIEphdmEtYmFzZWQgUGFyc2VyIEdlbmVyYXRvciwgUC4gdmFuIGRlciBTcGVrLCBOLiBQbGF0IGFuZCBDLiBQcm9uay4gQUNNIFNJR1BMQU4gTm90aWNlcywgNDAoNCk6NDctNTAuIEFwcmlsIDIwMDUu\">\n            <i class=\"fa fa-download fa-fw\"></i> Download BibTeX\n          </a>\n        </li>\n        <li>\n          <a href=\"//bibbase.org/rss?bib=http://lausdahl.github.io/overturetool.github.io/publications/overtureweb.bib\">\n            <i class=\"fa fa-rss fa-fw\"></i> RSS Feed\n          </a>\n          </li>\n      </ul>\n      </li>\n\n      \n\n\n      \n    </ul>\n\n\n    <div class=\"alert alert-success bibbase_msg\" id=\"bibbase_msg_embed\"\n         style=\"display: none;\">\n\n      Excellent! Next you can\n      <a href=\"/network/register?next=/network/newSiteFromTemplate%3Fbiburl=http://lausdahl.github.io/overturetool.github.io/publications/overtureweb.bib\"\n      >create a new website with this list</a>, or\n      embed it in an existing web page by copying &amp; pasting\n      any of the following snippets.\n\n      <div style=\"text-align: left; margin-top: 1em;\">\n        <strong>JavaScript</strong>\n        <span class=\"comment recommended\">(easiest)</span>\n        <div class=\"well well-small\">\n          <code>\n            &lt;script src=\"https://bibbase.org/show?bib=http%3A%2F%2Flausdahl.github.io%2Foverturetool.github.io%2Fpublications%2Fovertureweb.bib&amp;jsonp=1&amp;jsonp=1\"&gt;&lt;/script&gt;\n          </code>\n        </div>\n\n        <strong>PHP</strong>\n        <div class=\"well well-small\">\n          <code>\n            &lt;?php\n            $contents = file_get_contents(\"https://bibbase.org/show?bib=http%3A%2F%2Flausdahl.github.io%2Foverturetool.github.io%2Fpublications%2Fovertureweb.bib&amp;jsonp=1\");\n            print_r($contents);\n            ?&gt;\n          </code>\n        </div>\n\n        <strong>iFrame</strong>\n        <span class=\"comment\">(not recommended)</span>\n        <div class=\"well well-small\">\n          <code>\n            &lt;iframe src=\"https://bibbase.org/show?bib=http%3A%2F%2Flausdahl.github.io%2Foverturetool.github.io%2Fpublications%2Fovertureweb.bib&amp;jsonp=1\"&gt;&lt;/iframe&gt;\n          </code>\n        </div>\n\n        <p>\n          For more details see the <a href=\"//bibbase.org/help\">documention</a>.\n        </p>\n      </div>\n    </div>\n\n    <div class=\"alert alert-success bibbase_msg\" id=\"bibbase_msg_preview\"\n         style=\"display: none;\">\n\n      This is a preview! To use this list on your own web site\n      or create a new web site from it,\n      <a href=\"/network/register?next=/network/newAccountWithFile%3FfileId=\"\n      >create a free account</a>. The file will be added\n      and you will be able to edit it in the File Manager.\n      We will show you instructions once you've created your account.\n    </div>\n\n    <div class=\"alert alert-warning bibbase_msg\" id=\"bibbase_msg_mendeley1\"\n         style=\"display: none;\">\n\n      <p>To the site owner:</p>\n\n      <p><strong>Action required!</strong> Mendeley is changing its\n        API. In order to keep using Mendeley with BibBase past April\n        14th, you need to:\n        <ol>\n          <li>renew the authorization for BibBase on Mendeley, and</li>\n          <li>update the BibBase URL\n            in your page the same way you did when you initially set up\n            this page.\n          </li>\n        </ol>\n      </p>\n\n      <p>\n        <a href=\"http://bibbase.org/cgi-bin/mendeley2/get.py\">\n          <i class=\"fa fa-angle-double-right\"></i>\n          Fix it now</a>\n      </p>\n    </div>\n\n  </div>\n\n\n  <div id=\"bibbase_body\">\n    \n  \n  <div class=\"bibbase_group_whole\" id=\"group_2013\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2013')\"\n      onkeypress=\"toggleGroup('group_2013')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2013</span>\n      <span class=\"bibbase_group_count\">\n        \n        (1)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"lausdahl-translatingvdmtoalloy-2013\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://dx.doi.org/10.1007/978-3-642-38613-8_4\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'lausdahl-translatingvdmtoalloy-2013', 'http://dx.doi.org/10.1007/978-3-642-38613-8_4', event);\">\n    Translating VDM to Alloy.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://bibbase.org/show?bib=blog.lausdahl.com/wp-content/uploads/publications/lausdahl.bib&proxy=1&groupby=year\">Lausdahl, K.</a>\n</span>\n\n  \n\n</span>\n\n  In Johnsen, E. B.;  and Petre, L., editor(s), <i>Integrated Formal Methods</i>, volume 7940, of Lecture Notes in Computer Science, pages 46-60. Springer Berlin Heidelberg,  2013.\n  <span class=\"note\">10th International Conference, IFM 2013</span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://dx.doi.org/10.1007/978-3-642-38613-8_4\"\n     onclick=\"log_download('lausdahl-translatingvdmtoalloy-2013', 'http://dx.doi.org/10.1007/978-3-642-38613-8_4', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Translating VDM to Alloy [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"http://doi.org/10.1007/978-3-642-38613-8_4\"\n     onclick=\"log_download('lausdahl-translatingvdmtoalloy-2013', 'http://doi.org/10.1007/978-3-642-38613-8_4', event.ctrlKey)\"\n     class=\"bibbase doi link\">\n    <span>doi</span></a>\n  &nbsp;\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/lausdahl-translatingvdmtoalloy-2013\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>4 downloads</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('lausdahl-translatingvdmtoalloy-2013')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@incollection{Lausdahl&amp;13,\n  KEY       = &quot;Lausdahl\\&amp;13&quot;,\n  year\t\t={2013},\n  isbn\t\t={978-3-642-38612-1},\n  booktitle\t={Integrated Formal Methods},\n  volume\t={7940},\n  series\t={Lecture Notes in Computer Science},\n  editor\t={Johnsen, Einar Broch and Petre, Luigia},\n  doi\t\t={10.1007/978-3-642-38613-8_4},\n  title\t\t=&quot;{Translating VDM to Alloy}&quot;,\n  url\t\t={http://dx.doi.org/10.1007/978-3-642-38613-8_4},\n  publisher\t={Springer Berlin Heidelberg},\n  author\t={Lausdahl, Kenneth},\n  pages\t\t={46-60},\n  note\t\t={10th International Conference, IFM 2013},\n}\n\n% 2012\n\n</pre>\n</div>\n\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2012\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2012')\"\n      onkeypress=\"toggleGroup('group_2012')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2012</span>\n      <span class=\"bibbase_group_count\">\n        \n        (6)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"christiansen-bjerge-edwards-larsen-towardsamethodologyformodellingandvalidationofanagriculturalvehiclesdynamicsandcontrol-2012\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  Towards a Methodology for Modelling and Validation of an Agricultural Vehicle's Dynamics and Control.\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Christiansen, M. P.; Bjerge, K.; Edwards, G.;  and Larsen, P. G.\n</span>\n\n  \n\n</span>\n\n  In Junco, S., editor(s), <i>The 6th International Conference on Integrated Modeling and Analysis in Applied Control and Automation</i>, of <i>IMAACA</i>, pages 112-119, September 2012. \n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/christiansen-bjerge-edwards-larsen-towardsamethodologyformodellingandvalidationofanagriculturalvehiclesdynamicsandcontrol-2012\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('christiansen-bjerge-edwards-larsen-towardsamethodologyformodellingandvalidationofanagriculturalvehiclesdynamicsandcontrol-2012')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@INPROCEEDINGS{Christiansen&amp;12a,\n  KEY \t\t= &quot;Christiansen\\&amp;12&quot;,\n  AUTHOR\t= &quot;Martin Peter Christiansen and Kim Bjerge and Gareth Edwards and Peter Gorm Larsen&quot;,\n  TITLE\t\t= &quot;Towards a Methodology for Modelling and Validation of an Agricultural Vehicle&#x27;s Dynamics and Control&quot;,\n  EDITOR    = &quot;Sergio Junco&quot;,\n  PAGES     = &quot;112-119&quot;,\n  YEAR\t\t= &quot;2012&quot;,\n  MONTH\t\t= &quot;September&quot;,\n  BOOKTITLE\t= &quot;{The 6th International Conference on Integrated Modeling and Analysis in Applied Control and Automation}&quot;,\n  SERIES\t= {IMAACA}\n}\n\n%A Rigorous Approach to the Design of Resilient Cyber-physical Systems through Co-Simulation John Fitzgerald, Ken Pierce, Carl Gamble, in Dependable Systems and Networks Workshops (DSN-W) 2012 (WORCS), presented in June 2012, Boston, MA, USA.\n\n</pre>\n</div>\n\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"wolff-scrumgoesformalagilemethodsforsafetycriticalsystems-2012\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  Scrum Goes Formal: Agile Methods for Safety-Critical Systems.\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Wolff, S.\n</span>\n\n  \n\n</span>\n\n  In <i>ICSE 2012: Proceedings of the 34th International Conference on Software Engineering</i>, pages 23–29, June 2012. \n  <span class=\"note\">Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches, FormSERA 2012</span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/wolff-scrumgoesformalagilemethodsforsafetycriticalsystems-2012\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('wolff-scrumgoesformalagilemethodsforsafetycriticalsystems-2012')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@INPROCEEDINGS{Wolff12a,\n  KEY           = &quot;Wolff12&quot;,\n  AUTHOR        = &quot;Sune Wolff&quot;,\n  TITLE         = &quot;{Scrum Goes Formal: Agile Methods for Safety-Critical Systems}&quot;,\n  BOOKTITLE     = &quot;ICSE 2012: Proceedings of the 34th International Conference on Software\n\t\t\t\t   Engineering&quot;,\n  NOTE\t\t\t= &quot;{Workshop on Formal Methods in Software Engineering: Rigorous\n\t\t\t\t   and Agile Approaches, FormSERA 2012}&quot;,\n  YEAR          = &quot;2012&quot;,\n  MONTH         = &quot;June&quot;,\n  PAGES         = &quot;23--29&quot;,\n  SIZE\t\t\t= &quot;7&quot;,\n  ISBN          = &quot;978-1-4673-1906-5&quot;,\n  ANNOTE        = &quot;&quot;,\n  COMMENT       = &quot;&quot;}\n  \n</pre>\n</div>\n\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"nielsen-lausdahl-larsen-combiningvdmwithexecutablecode-2012\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://dx.doi.org/10.1007/978-3-642-30885-7_19\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'nielsen-lausdahl-larsen-combiningvdmwithexecutablecode-2012', 'http://dx.doi.org/10.1007/978-3-642-30885-7_19', event);\">\n    Combining VDM with Executable Code.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Nielsen, C. B.; <a class=\"bibbase author link\" href=\"https://bibbase.org/show?bib=blog.lausdahl.com/wp-content/uploads/publications/lausdahl.bib&proxy=1&groupby=year\">Lausdahl, K.</a>;  and Larsen, P. G.\n</span>\n\n  \n\n</span>\n\n  In Derrick, J.; Fitzgerald, J.; Gnesi, S.; Khurshid, S.; Leuschel, M.; Reeves, S.;  and Riccobene, E., editor(s), <i>Abstract State Machines, Alloy, B, VDM, and Z</i>, volume 7316, of <i>Lecture Notes in Computer Science</i>, pages 266–279, Berlin, Heidelberg,  2012. Springer-Verlag\n  <span class=\"note\">ISBN 978-3-642-30884-0</span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://dx.doi.org/10.1007/978-3-642-30885-7_19\"\n     onclick=\"log_download('nielsen-lausdahl-larsen-combiningvdmwithexecutablecode-2012', 'http://dx.doi.org/10.1007/978-3-642-30885-7_19', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Combining VDM with Executable Code [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/nielsen-lausdahl-larsen-combiningvdmwithexecutablecode-2012\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>2 downloads</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('nielsen-lausdahl-larsen-combiningvdmwithexecutablecode-2012')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@INPROCEEDINGS{Nielsen&amp;12,\n  KEY\t\t\t= &quot;Nielsen\\&amp;12&quot;,\n  AUTHOR\t\t= &quot;Claus Ballegaard Nielsen and Kenneth Lausdahl and Peter Gorm Larsen&quot;,\n  TITLE\t\t\t= &quot;{Combining VDM with Executable Code}&quot;,\n  booktitle  \t= &quot;{Abstract State Machines, Alloy, B, VDM, and Z}&quot;,\n  volume\t\t= {7316},\n  editor\t\t= {Derrick, John and Fitzgerald, John and Gnesi, Stefania and Khurshid, Sarfraz and Leuschel, Michael and Reeves, Steve and Riccobene, Elvinia},\n  YEAR\t\t\t= &quot;2012&quot;,\n  location \t\t= {Pisa, Italy},\n  pages \t\t= {266--279},\n  numpages \t\t= {14},\n  SERIES        = &quot;Lecture Notes in Computer Science&quot;,\n  VOLUME        = &quot;7316&quot;,\n  publisher \t= {Springer-Verlag},\n  address \t\t= {Berlin, Heidelberg},\n  NOTE       \t= &quot;{ISBN 978-3-642-30884-0}&quot;,\n  url \t\t\t= {http://dx.doi.org/10.1007/978-3-642-30885-7_19},\n  }\n  \n</pre>\n</div>\n\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"payne-bryans-fitzgerald-riddle-interfacespecificationforsystemofsystemsarchitectures-2012\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  Interface Specification for System-of-Systems Architectures.\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Payne, R.; Bryans, J.; Fitzgerald, J.;  and Riddle, S.\n</span>\n\n  \n\n</span>\n\n  In <i>Proceedings of the 7th International Conference on System of System Engineering, IEEE SoSE 2012</i>, July 2012. IEEE\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/payne-bryans-fitzgerald-riddle-interfacespecificationforsystemofsystemsarchitectures-2012\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('payne-bryans-fitzgerald-riddle-interfacespecificationforsystemofsystemsarchitectures-2012')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@INPROCEEDINGS{Payne&amp;12a,\n  KEY           = &quot;Payne&amp;12a&quot;,\n  AUTHOR        = &quot;Richard Payne and Jeremy Bryans and John Fitzgerald and Steve Riddle&quot;,\n  TITLE         = &quot;{Interface Specification for System-of-Systems Architectures}&quot;,\n  BOOKTITLE     = &quot;Proceedings of the 7th International Conference on\n                   System of System Engineering, IEEE SoSE 2012&quot;,\n  PUBLISHER     = &quot;{IEEE}&quot;,\n  YEAR          = 2012,\n  MONTH         = &quot;July&quot;}\n  \n</pre>\n</div>\n\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"fitzgerald-bryans-payne-aformalmodelbasedapproachtoengineeringsystemsofsystems-2012\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://dx.doi.org/10.1007/978-3-642-32775-9_6\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'fitzgerald-bryans-payne-aformalmodelbasedapproachtoengineeringsystemsofsystems-2012', 'http://dx.doi.org/10.1007/978-3-642-32775-9_6', event);\">\n    A Formal Model-Based Approach to Engineering Systems-of-Systems.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Fitzgerald, J. S.; Bryans, J.;  and Payne, R.\n</span>\n\n  \n\n</span>\n\n  In Camarinha-Matos, L. M.; Xu, L.;  and Afsarmanesh, H., editor(s), <i>Collaborative Networks in the Internet of Services - 13th IFIP WG 5.5 Working Conference on Virtual Enterprises, PRO-VE 2012, Bournemouth, UK, October 1-3, 2012. Proceedings</i>, volume 380, of <i>IFIP Advances in Information and Communication Technology</i>, pages 53-62,  2012. Springer\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://dx.doi.org/10.1007/978-3-642-32775-9_6\"\n     onclick=\"log_download('fitzgerald-bryans-payne-aformalmodelbasedapproachtoengineeringsystemsofsystems-2012', 'http://dx.doi.org/10.1007/978-3-642-32775-9_6', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"A Formal Model-Based Approach to Engineering Systems-of-Systems [link]\"\n       title=\"Link\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Link</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/fitzgerald-bryans-payne-aformalmodelbasedapproachtoengineeringsystemsofsystems-2012\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>1 download</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('fitzgerald-bryans-payne-aformalmodelbasedapproachtoengineeringsystemsofsystems-2012')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@inproceedings{Fitzgerald&amp;12c,\n  key       = &quot;Fitzgerald\\&amp;12c&quot;,\n  author    = {John S. Fitzgerald and\n               Jeremy Bryans and\n               Richard Payne},\n  title     = {A Formal Model-Based Approach to Engineering\nSystems-of-Systems},\n  editor    = {Luis M. Camarinha-Matos and\n               Lai Xu and\n               Hamideh Afsarmanesh},\n  booktitle = {Collaborative Networks in the Internet of Services - 13th\n               IFIP WG 5.5 Working Conference on Virtual Enterprises,\nPRO-VE 2012, Bournemouth, UK, October 1-3, 2012. Proceedings},\n  publisher = {Springer},\n  series    = {IFIP Advances in Information and Communication Technology},\n  volume    = {380},\n  year      = {2012},\n  pages     = {53-62},\n  ee        = {http://dx.doi.org/10.1007/978-3-642-32775-9_6},\n  bibsource = {DBLP, http://dblp.uni-trier.de}\n}\n\n</pre>\n</div>\n\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"larsen-coleman-fitzgerald-gettingsoftwareengineeringoutofisolation-2012\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  Getting Software Engineering out of Isolation.\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Larsen, P. G.; Coleman, J. W.;  and Fitzgerald, J.\n</span>\n\n  \n\n</span>\n\n  In Petrenko, A. K., editor(s), <i>SYRCoSE Software Engineering Colloquium</i>, Perm, Russia, May 2012. \n  <span class=\"note\">ISBN 978-5-91474-019-8</span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/larsen-coleman-fitzgerald-gettingsoftwareengineeringoutofisolation-2012\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('larsen-coleman-fitzgerald-gettingsoftwareengineeringoutofisolation-2012')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@INPROCEEDINGS{Larsen&amp;12a,\n  KEY           = &quot;Larsen\\&amp;12&quot;,\n  AUTHOR        = &quot;Peter Gorm Larsen and Joey W.\\ Coleman and John Fitzgerald&quot;,\n  EDITOR        = &quot;Alexander K. Petrenko&quot;,\n  TITLE         = &quot;{Getting Software Engineering out of Isolation}&quot;,\n  BOOKTITLE     = &quot;SYRCoSE Software Engineering Colloquium&quot;,\n  ADDRESS       = &quot;Perm, Russia&quot;,\n  YEAR          = &quot;2012&quot;,\n  MONTH         = &quot;May&quot;,\n  NOTE          = &quot;ISBN 978-5-91474-019-8&quot;,\n  PAGES         = &quot;&quot;,\n  ANNOTE        = &quot;&quot;,\n  COMMENT       = &quot;BIB PGL I also have the sources&quot;}\n  \n%2011\n\n</pre>\n</div>\n\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2011\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2011')\"\n      onkeypress=\"toggleGroup('group_2011')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2011</span>\n      <span class=\"bibbase_group_count\">\n        \n        (2)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"lausdahl-larsen-battle-adeterministicinterpretersimulatingadistributedrealtimesystemusingvdm-2011\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://dl.acm.org/citation.cfm?id=2075089.2075107\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'lausdahl-larsen-battle-adeterministicinterpretersimulatingadistributedrealtimesystemusingvdm-2011', 'http://dl.acm.org/citation.cfm?id=2075089.2075107', event);\">\n    A Deterministic Interpreter Simulating A Distributed real time system using VDM.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  <a class=\"bibbase author link\" href=\"https://bibbase.org/show?bib=blog.lausdahl.com/wp-content/uploads/publications/lausdahl.bib&proxy=1&groupby=year\">Lausdahl, K.</a>; Larsen, P. G.;  and Battle, N.\n</span>\n\n  \n\n</span>\n\n  In Qin, S.;  and Qiu, Z., editor(s), <i>Proceedings of the 13th international conference on Formal methods and software engineering</i>, volume 6991, of <i>Lecture Notes in Computer Science</i>, pages 179–194, Berlin, Heidelberg, October 2011. Springer-Verlag\n  <span class=\"note\">ISBN 978-3-642-24558-9</span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://dl.acm.org/citation.cfm?id=2075089.2075107\"\n     onclick=\"log_download('lausdahl-larsen-battle-adeterministicinterpretersimulatingadistributedrealtimesystemusingvdm-2011', 'http://dl.acm.org/citation.cfm?id=2075089.2075107', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"A Deterministic Interpreter Simulating A Distributed real time system using VDM [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/lausdahl-larsen-battle-adeterministicinterpretersimulatingadistributedrealtimesystemusingvdm-2011\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('lausdahl-larsen-battle-adeterministicinterpretersimulatingadistributedrealtimesystemusingvdm-2011')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@INPROCEEDINGS{Lausdahl&amp;11,\n  KEY           = &quot;Lausdahl\\&amp;11&quot;,\n  AUTHOR        = &quot;Kenneth Lausdahl and Peter Gorm Larsen and Nick Battle&quot;,\n  title \t\t= &quot;{A Deterministic Interpreter Simulating A Distributed real time system using VDM}&quot;,\n  booktitle \t= {Proceedings of the 13th international conference on Formal methods and software engineering},\n  series\t\t= {Lecture Notes in Computer Science},\n  volume\t\t= {6991},\n  editor\t\t= {Qin, Shengchao and Qiu, Zongyan},\n  YEAR          = &quot;2011&quot;,\n  MONTH         = &quot;October&quot;,\n  note        \t= &quot;{ISBN 978-3-642-24558-9}&quot;,\n   location \t= {Durham, UK},\n pages \t\t\t= {179--194},\n numpages \t\t= {16},\n url \t\t\t= {http://dl.acm.org/citation.cfm?id=2075089.2075107},\n   publisher \t= {Springer-Verlag},\n address \t\t= {Berlin, Heidelberg},\n  }\n  \n</pre>\n</div>\n\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"pierce-fitzgerald-gamble-modellingfaultsandfaulttolerancemechanismsinapaperpinchcomodel-2011\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  Modelling Faults and Fault Tolerance Mechanisms in a Paper Pinch Co- model.\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Pierce, K.; Fitzgerald, J.;  and Gamble, C.\n</span>\n\n  \n\n</span>\n\n  In <i>Proceedings of the ERCIM/EWICS/Cyber-physical Systems Workshop at SafeComp 2011, Naples, Italy (to appear)</i>, September 2011. ERCIM\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/pierce-fitzgerald-gamble-modellingfaultsandfaulttolerancemechanismsinapaperpinchcomodel-2011\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('pierce-fitzgerald-gamble-modellingfaultsandfaulttolerancemechanismsinapaperpinchcomodel-2011')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@INPROCEEDINGS{Pierce&amp;11,\n  KEY = {Pierce\\&amp;11},\n  AUTHOR = {Ken Pierce and John Fitzgerald and Carl Gamble},\n  TITLE = {Modelling Faults and Fault Tolerance Mechanisms in a Paper Pinch Co- model},\n  BOOKTITLE = {Proceedings of the ERCIM/EWICS/Cyber-physical Systems Workshop at SafeComp 2011, Naples, Italy (to appear)},\n  YEAR = {2011},\n  MONTH = {September},\n  PUBLISHER = {ERCIM}\n}\n\n\n% VDM-SL, VDM++ Simple Reference (in Japanese), Dr. Fuyuki Ishikawa, June 2011.\n\n%VDM specification as Structured Japanese Specification (in Japanese), Shin Sahara, SEC journal, Vol. 26., 31th March, 2011, pp. 23-27, ISSN 1349-8622.\n\n%Answers to Frequently Asked Questions for the Practice of Formal Methods (in Japanese), Dr. Taro Kurita, SEC journal, Vol. 26., 31th March, 2011, pp. 34-39, ISSN 1349-8622.\n\n%2010\n\n</pre>\n</div>\n\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2010\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2010')\"\n      onkeypress=\"toggleGroup('group_2010')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2010</span>\n      <span class=\"bibbase_group_count\">\n        \n        (7)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"larsen-lausdahl-battle-thevdm10languagemanual-2010\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://lausdahl.github.io/overturetool.github.io/files/VDM10_lang_man.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'larsen-lausdahl-battle-thevdm10languagemanual-2010', 'http://lausdahl.github.io/overturetool.github.io/files/VDM10_lang_man.pdf', event);\">\n    The VDM-10 Language Manual.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Larsen, P. G.; Lausdahl, K.;  and Battle, N.\n</span>\n\n  \n\n</span>\n\n  Technical Report TR-2010-06, The Overture Open Source Initiative, April 2010.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://lausdahl.github.io/overturetool.github.io/files/VDM10_lang_man.pdf\"\n     onclick=\"log_download('larsen-lausdahl-battle-thevdm10languagemanual-2010', 'http://lausdahl.github.io/overturetool.github.io/files/VDM10_lang_man.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"The VDM-10 Language Manual [pdf]\"\n       title=\" paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\"> paper</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/larsen-lausdahl-battle-thevdm10languagemanual-2010\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>2 downloads</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('larsen-lausdahl-battle-thevdm10languagemanual-2010')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@TECHREPORT{Larsen&amp;10b,\n  KEY           = &quot;Larsen\\&amp;10&quot;,\n  AUTHOR        = &quot;Peter Gorm Larsen and Kenneth Lausdahl and Nick Battle&quot;,\n  TITLE         = &quot;{The VDM-10 Language Manual}&quot;,\n  INSTITUTION   = &quot;The Overture Open Source Initiative&quot;,\n  YEAR          = &quot;2010&quot;,\n  MONTH         = &quot;April&quot;,\n  NUMBER        = &quot;TR-2010-06&quot;,\n  ANNOTE        = &quot;&quot;,\n  url_Paper = {http://lausdahl.github.io/overturetool.github.io/files/VDM10_lang_man.pdf},\n  COMMENT       = &quot;PGL&quot;}\n  \n%G VDM TOOL\n</pre>\n</div>\n\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"larsen-lausdahl-ribeiro-wolff-battle-overturevdm10toolsupportuserguide-2010\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  Overture VDM-10 Tool Support: User Guide.\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Larsen, P. G.; Lausdahl, K.; Ribeiro, A.; Wolff, S.;  and Battle, N.\n</span>\n\n  \n\n</span>\n\n  Technical Report TR-2010-02, The Overture Initiative, www.overturetool.org, May 2010.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/larsen-lausdahl-ribeiro-wolff-battle-overturevdm10toolsupportuserguide-2010\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('larsen-lausdahl-ribeiro-wolff-battle-overturevdm10toolsupportuserguide-2010')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@TECHREPORT{Larsen&amp;10d,\n  KEY           = &quot;Larsen\\&amp;10&quot;,\n  AUTHOR        = &quot;Peter Gorm Larsen and Kenneth Lausdahl and Augusto Ribeiro and\n                   Sune Wolff and Nick Battle&quot;,\n  TITLE         = &quot;{Overture VDM-10 Tool Support: User Guide}&quot;,\n  INSTITUTION   = &quot;The Overture Initiative&quot;,\n  ADDRESS       = &quot;www.overturetool.org&quot;,\n  YEAR          = &quot;2010&quot;,\n  MONTH         = &quot;May&quot;,\n  NUMBER        = &quot;TR-2010-02&quot;,\n  SIZE          = &quot;103&quot;,\n  ANNOTE        = &quot;&quot;,\n  COMMENT       = &quot;We have the sources PGL&quot;}\n  \n%TR-003: Tutorial for Overture/VDM-SL, P. G. Larsen, J. S. Fitzgerald, S. Wolff, N. Battle, K. G. Lausdahl, A. Ribeiro, K. G. Pierce, S. Riddle, version 2, February 2011\n%TR-004: Tutorial for Overture/VDM++, P. G. Larsen, J. S. Fitzgerald, S. Wolff, N. Battle, K. G. Lausdahl, A. Ribeiro, K. G. Pierce, and S. Riddle, version 2, February 2011\n%TR-005: Tutorial for Overture/VDM-RT, P. G. Larsen, J. S. Fitzgerald, S. Wolff, N. Battle, K. G. Lausdahl, A. Ribeiro, K. G. Pierce, and S. Riddle, version 2, February 2011\n%TR-006: Development Process for Distributed Embedded Systems using VDM, P. G. Larsen, S. Wolff, N. Battle, J. S. Fitzgerald, and K. G. Pierce version 2, February 2011\n%TR-007: VDMJ Tool Support: User Guide, Nick Battle version 1, February 2011\n\n\n%\n% books\n%\n\n%G VDM TUTOR FORMAL\n</pre>\n</div>\n\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"ribeiro-larsen-proofobligationgenerationanddischargingforrecursivedefinitionsinvdm-2010\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  Proof Obligation Generation and Discharging for Recursive Definitions in VDM.\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Ribeiro, A.;  and Larsen, P. G.\n</span>\n\n  \n\n</span>\n\n  In Song, J.;  and Huibiao, editor(s), <i>The 12th International Conference on Formal Engineering Methods (ICFEM 2010)</i>, November 2010. Springer-Verlag\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/ribeiro-larsen-proofobligationgenerationanddischargingforrecursivedefinitionsinvdm-2010\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('ribeiro-larsen-proofobligationgenerationanddischargingforrecursivedefinitionsinvdm-2010')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@INPROCEEDINGS{Ribeiro&amp;10,\n  KEY           = &quot;Ribeiro\\&amp;10&quot;,\n  AUTHOR        = &quot;Augusto Ribeiro and Peter Gorm Larsen&quot;,\n  EDITOR        = &quot;Jin Song and Huibiao&quot;,\n  TITLE         = &quot;{Proof Obligation Generation and Discharging for\n                   Recursive Definitions in {VDM}}&quot;,\n  BOOKTITLE     = &quot;The 12th International Conference on Formal Engineering\n                   Methods (ICFEM 2010)&quot;,\n  PUBLISHER     = &quot;Springer-Verlag&quot;,\n  YEAR          = &quot;2010&quot;,\n  MONTH         = &quot;November&quot;,\n  ANNOTE        = &quot;&quot;,\n  COMMENT       = &quot;I have the sources PGL&quot;}\n  \n</pre>\n</div>\n\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"fitzgerald-larsen-pierce-verhoef-wolff-collaborativemodellingandcosimulationinthedevelopmentofdependableembeddedsystems-2010\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://www.cs.ncl.ac.uk/publications/trs/papers/1213.pdf\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'fitzgerald-larsen-pierce-verhoef-wolff-collaborativemodellingandcosimulationinthedevelopmentofdependableembeddedsystems-2010', 'http://www.cs.ncl.ac.uk/publications/trs/papers/1213.pdf', event);\">\n    Collaborative Modelling and Co-simulation in the Development of Dependable Embedded Systems.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Fitzgerald, J.; Larsen, P. G.; Pierce, K.; Verhoef, M.;  and Wolff, S.\n</span>\n\n  \n\n</span>\n\n  Technical Report CS-TR-1213, School of Computing Science, Newcastle University, July 2010.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://www.cs.ncl.ac.uk/publications/trs/papers/1213.pdf\"\n     onclick=\"log_download('fitzgerald-larsen-pierce-verhoef-wolff-collaborativemodellingandcosimulationinthedevelopmentofdependableembeddedsystems-2010', 'http://www.cs.ncl.ac.uk/publications/trs/papers/1213.pdf', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/pdf.svg\"\n\t     alt=\"Collaborative Modelling and Co-simulation in the Development of Dependable Embedded Systems [pdf]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/fitzgerald-larsen-pierce-verhoef-wolff-collaborativemodellingandcosimulationinthedevelopmentofdependableembeddedsystems-2010\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>3 downloads</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('fitzgerald-larsen-pierce-verhoef-wolff-collaborativemodellingandcosimulationinthedevelopmentofdependableembeddedsystems-2010')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@TECHREPORT{Fitzgerald&amp;10a,\n  KEY           = &quot;Fitzgerald\\&amp;10a&quot;,\n  AUTHOR        = {John Fitzgerald and Peter Gorm Larsen and Ken Pierce and Marcel Verhoef and Sune Wolff},\n  TITLE         = &quot;{Collaborative Modelling and Co-simulation in the Development of Dependable Embedded Systems}&quot;,\n  INSTITUTION   = &quot;School of Computing Science, Newcastle University&quot;,\n  YEAR          = &quot;2010&quot;,\n  MONTH         = &quot;July&quot;,\n  NUMBER        = &quot;{CS-TR-1213}&quot;,\n  URL           = &quot;http://www.cs.ncl.ac.uk/publications/trs/papers/1213.pdf&quot;}\n  \n</pre>\n</div>\n\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"larsen-fitzgerald-wolff-areformalmethodsreadyforagilityarealitycheck-2010\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  Are Formal Methods Ready for Agility? A Reality Check.\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Larsen, P. G.; Fitzgerald, J.;  and Wolff, S.\n</span>\n\n  \n\n</span>\n\n  In Gruner, S.;  and Rumpe, B., editor(s), <i>2nd International Workshop on Formal Methods and Agile Methods</i>, pages 13–25, September 2010. Lecture Notes in Informatics\n  <span class=\"note\">ISSH 1617-5468</span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/larsen-fitzgerald-wolff-areformalmethodsreadyforagilityarealitycheck-2010\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('larsen-fitzgerald-wolff-areformalmethodsreadyforagilityarealitycheck-2010')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@INPROCEEDINGS{Larsen&amp;10g,\n  KEY           = &quot;Larsen\\&amp;10&quot;,\n  AUTHOR        = &quot;Peter Gorm Larsen and John Fitzgerald and Sune Wolff&quot;,\n  EDITOR        = &quot;Stefan Gruner and Bernhard Rumpe&quot;,\n  TITLE         = &quot;Are Formal Methods Ready for Agility? A Reality Check&quot;,\n  BOOKTITLE     = &quot;2nd International Workshop on Formal Methods and Agile\n                   Methods&quot;,\n  PUBLISHER     = &quot;Lecture Notes in Informatics&quot;,\n  PAGES         = &quot;13--25&quot;,\n  YEAR          = &quot;2010&quot;,\n  MONTH         = &quot;September&quot;,\n  NOTE          = &quot;ISSH 1617-5468&quot;,\n  ANNOTE        = &quot;&quot;,\n  COMMENT       = &quot;BIB I have the sources PGL&quot;}\n  \n</pre>\n</div>\n\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"broenink-larsen-verhoef-kleijn-jovanovic-pierce-f-designsupportandtoolingfordependableembeddedcontrolsoftware-2010\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  Design Support and Tooling for Dependable Embedded Control Software.\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Broenink, J. F.; Larsen, P. G.; Verhoef, M.; Kleijn, C.; Jovanovic, D.; Pierce, K.;  and F., W.\n</span>\n\n  \n\n</span>\n\n  In <i>Proceedings of Serene 2010 International Workshop on Software Engineering for Resilient Systems</i>, pages 77–82, April 2010. ACM\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/broenink-larsen-verhoef-kleijn-jovanovic-pierce-f-designsupportandtoolingfordependableembeddedcontrolsoftware-2010\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('broenink-larsen-verhoef-kleijn-jovanovic-pierce-f-designsupportandtoolingfordependableembeddedcontrolsoftware-2010')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@INPROCEEDINGS{Broenink&amp;10,\n  KEY           = &quot;Broenink\\&amp;10&quot;,\n  AUTHOR        = &quot;Broenink, J. F. and Larsen, P. G. and  Verhoef, M. and\n                   Kleijn, C. and  Jovanovic, D. and Pierce, K. and\n                   Wouters F.&quot;,\n  TITLE         = &quot;{Design Support and Tooling for Dependable Embedded Control Software}&quot;,\n  BOOKTITLE     = &quot;Proceedings of Serene 2010 International Workshop on\n                   Software Engineering for Resilient Systems&quot;,\n  PUBLISHER     = &quot;ACM&quot;,\n  YEAR          = &quot;2010&quot;,\n  MONTH         = &quot;April&quot;,\n  PAGES         = &quot;77--82&quot;,\n  ANNOTE        = &quot;&quot;,\n  COMMENT       = &quot;I have the sources (PGL)&quot;}\n  \n% Proving Consistency of VDM models using HOL, Sander D. Vermolen, Jozef Hooman and Peter Gorm Larsen, in Proceedings of the 2010 ACM Symposium on Applied Computing, ACM, March 2010.\n\n% Formal Semantics of a VDM Extension for Distributed Embedded Systems, Jozef Hooman and Marcel Verhoef, in D. Dams and U. Hannemann and M. Steffen (eds): W.P. de Roever Festschrift, LNCS 5930, pp 142-161, 2010.\n\n</pre>\n</div>\n\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"larsen-battle-ferreira-fitzgerald-lausdahl-verhoef-theovertureinitiativeintegratingtoolsforvdm-2010\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://doi.acm.org/10.1145/1668862.1668864\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'larsen-battle-ferreira-fitzgerald-lausdahl-verhoef-theovertureinitiativeintegratingtoolsforvdm-2010', 'http://doi.acm.org/10.1145/1668862.1668864', event);\">\n    The Overture Initiative – Integrating Tools for VDM.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Larsen, P. G.; Battle, N.; Ferreira, M.; Fitzgerald, J.; <a class=\"bibbase author link\" href=\"https://bibbase.org/show?bib=blog.lausdahl.com/wp-content/uploads/publications/lausdahl.bib&proxy=1&groupby=year\">Lausdahl, K.</a>;  and Verhoef, M.\n</span>\n\n  \n\n</span>\n\n  <i>SIGSOFT Softw. Eng. Notes</i>, 35(1): 1–6. January 2010.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://doi.acm.org/10.1145/1668862.1668864\"\n     onclick=\"log_download('larsen-battle-ferreira-fitzgerald-lausdahl-verhoef-theovertureinitiativeintegratingtoolsforvdm-2010', 'http://doi.acm.org/10.1145/1668862.1668864', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"The Overture Initiative – Integrating Tools for VDM [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/larsen-battle-ferreira-fitzgerald-lausdahl-verhoef-theovertureinitiativeintegratingtoolsforvdm-2010\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n  &nbsp;\n  <span class=\"bibbase_stats_paper\" style=\"color: #777;\">\n    <span>1 download</span>\n  </span>\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('larsen-battle-ferreira-fitzgerald-lausdahl-verhoef-theovertureinitiativeintegratingtoolsforvdm-2010')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@ARTICLE{Larsen&amp;10a,\n  KEY           = &quot;Larsen\\&amp;10&quot;,\n  AUTHOR        = &quot;Peter Gorm Larsen and Nick Battle and Miguel Ferreira\n                   and John Fitzgerald and Kenneth Lausdahl and Marcel\n                   Verhoef&quot;,\n  TITLE         = &quot;{The Overture Initiative -- Integrating Tools for VDM}&quot;,\n  JOURNAL       = {SIGSOFT Softw. Eng. Notes},\n  YEAR          = &quot;2010&quot;,\n  MONTH         = &quot;January&quot;,\n  VOLUME        = &quot;35&quot;,\n  NUMBER        = &quot;1&quot;,\n  PAGES         = &quot;1--6&quot;,\n  SIZE          = &quot;6&quot;,\n  ANNOTE        = &quot;&quot;,\n  numpages = {6},\n  issn = {0163-5948},\n  address = {New York, NY, USA},\n  publisher = {ACM},\n  URL\t\t\t= &quot;http://doi.acm.org/10.1145/1668862.1668864&quot;}\n  \n%2009\n\n</pre>\n</div>\n\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2009\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2009')\"\n      onkeypress=\"toggleGroup('group_2009')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2009</span>\n      <span class=\"bibbase_group_count\">\n        \n        (3)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"fitzgerald-larsen-modellingsystemspracticaltoolsandtechniquesinsoftwaredevelopment-2009\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  Modelling Systems – Practical Tools and Techniques in Software Development.\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Fitzgerald, J.;  and Larsen, P. G.\n</span>\n\n  \n\n</span>\n\n  Cambridge University Press, The Edinburgh Building, Cambridge CB2 2RU, UK, Second edition,  2009.\n  <span class=\"note\">ISBN 0-521-62348-0</span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/fitzgerald-larsen-modellingsystemspracticaltoolsandtechniquesinsoftwaredevelopment-2009\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('fitzgerald-larsen-modellingsystemspracticaltoolsandtechniquesinsoftwaredevelopment-2009')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@BOOK{Fitzgerald&amp;09,\n  KEY           = &quot;Fitzgerald\\&amp;09&quot;,\n  AUTHOR        = &quot;John Fitzgerald and Peter Gorm Larsen&quot;,\n  TITLE         = &quot;{Modelling Systems -- Practical Tools and Techniques in\n                    Software Development}&quot;,\n  PUBLISHER     = &quot;Cambridge University Press&quot;,\n  ADDRESS       = &quot;The Edinburgh Building, Cambridge CB2 2RU, UK&quot;,\n  YEAR          = &quot;2009&quot;,\n  EDITION       = &quot;{Second}&quot;,\n  NOTE          = &quot;{ISBN 0-521-62348-0}&quot;,\n  ANNOTE        = &quot;&quot;,\n  COMMENT       = &quot;I have the source PGL&quot;}\n  \n%Formal Specification by VDM++ (in Japanese), Dr. Fuyuki Ishikawa, ISBN-10: 4764904098. (Amazon link).\n\n%2013\n\n% IPA/SEC Investigative Report: Success Stories of Formal Methods in Strict Specification (in Japanese), Hiroshi Sakoh and Tomohiro Oda, January 2013.\n\n%G VDM ALLOY TOOL\n</pre>\n</div>\n\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"larsen-lausdahl-battle-combinatorialtestingforvdm-2009\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  Combinatorial Testing for VDM++.\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Larsen, P. G.; Lausdahl, K.;  and Battle, N.\n</span>\n\n  \n\n</span>\n\n  In <i>Submitted for publication</i>, December 2009. \n  <span class=\"note\">Outdated by i̧teLarsen&10c</span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/larsen-lausdahl-battle-combinatorialtestingforvdm-2009\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('larsen-lausdahl-battle-combinatorialtestingforvdm-2009')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@INPROCEEDINGS{Larsen&amp;09a,\n  KEY           = &quot;Larsen\\&amp;09&quot;,\n  AUTHOR        = &quot;Peter Gorm Larsen and Kenneth Lausdahl and Nick Battle&quot;,\n  TITLE         = &quot;{Combinatorial Testing for VDM++}&quot;,\n  BOOKTITLE     = &quot;Submitted for publication&quot;,\n  YEAR          = &quot;2009&quot;,\n  MONTH         = &quot;December&quot;,\n  NOTE          = &quot;Outdated by \\cite{Larsen&amp;10c}&quot;,\n  ANNOTE        = &quot;&quot;,\n  COMMENT       = &quot;Outdated by \\cite{Larsen&amp;10c}&quot;}\n  \n</pre>\n</div>\n\n\n\n</div>\n\n\n  <div class=\"bibbase_paper\" id=\"verhoef-modelingandvalidatingdistributedembeddedrealtimecontrolsystems-2009\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  Modeling and Validating Distributed Embedded Real-Time Control Systems.\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Verhoef, M.\n</span>\n\n  \n\n</span>\n\n  Ph.D. Thesis, Radboud University Nijmegen,  2009.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/verhoef-modelingandvalidatingdistributedembeddedrealtimecontrolsystems-2009\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('verhoef-modelingandvalidatingdistributedembeddedrealtimecontrolsystems-2009')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@PHDTHESIS{Verhoef09,\n  KEY           = &quot;Verhoef09&quot;,\n  AUTHOR        = &quot;Marcel Verhoef&quot;,\n  TITLE         = &quot;{Modeling and Validating Distributed Embedded Real-Time\n                    Control Systems}&quot;,\n  SCHOOL        = &quot;Radboud University Nijmegen&quot;,\n  YEAR          = &quot;2009&quot;,\n  NUMBER        = &quot;RU. 2009-01&quot;,\n  ANNOTE          = &quot;{ISBN 978-90-9023705-3}&quot;,\n  COMMENT       = &quot;I have a copy PGL&quot;}\n  \n</pre>\n</div>\n\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2007\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2007')\"\n      onkeypress=\"toggleGroup('group_2007')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2007</span>\n      <span class=\"bibbase_group_count\">\n        \n        (1)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"verhoef-larsen-interpretingdistributedsystemarchitecturesusingvdmacasestudy-2007\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  Interpreting Distributed System Architectures Using VDM++ – A Case Study.\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Verhoef, M.;  and Larsen, P. G.\n</span>\n\n  \n\n</span>\n\n  In Sauser, B.;  and Muller, G., editor(s), <i>5th Annual Conference on Systems Engineering Research</i>, March 2007. \n  <span class=\"note\">Available at http://www.stevens.edu/engineering/cser/</span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/verhoef-larsen-interpretingdistributedsystemarchitecturesusingvdmacasestudy-2007\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('verhoef-larsen-interpretingdistributedsystemarchitecturesusingvdmacasestudy-2007')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@INPROCEEDINGS{Verhoef&amp;07,\n  KEY           = &quot;Verhoef\\&amp;07&quot;,\n  AUTHOR        = &quot;Marcel Verhoef and Peter Gorm Larsen&quot;,\n  EDITOR        = &quot;Brian Sauser and Gerrit Muller&quot;,\n  TITLE         = &quot;{Interpreting Distributed System Architectures Using VDM++\n                   -- A Case Study}&quot;,\n  BOOKTITLE     = &quot;5th Annual Conference on Systems Engineering Research&quot;,\n  PUBLISHER     = &quot;&quot;,\n  YEAR          = &quot;2007&quot;,\n  MONTH         = &quot;March&quot;,\n  NOTE          = &quot;{Available at http://www.stevens.edu/engineering/cser/}&quot;,\n  ANNOTE        = &quot;&quot;,\n  COMMENT       = &quot;I have the sources (PGL)&quot;}\n  \n% Modeling and Validating Distributed Embedded Real-Time Systems in VDM++, Marcel Verhoef, Peter Gorm Larsen and Jozef Hooman, in Jayadev Misra, Tobias Nipkow and Emil Sekerinski (Eds.), FM 2006: Formal Methods, Proc. 14th Intl. Symposium on Formal Methods, Lecture Notes in Computer Science 4085, Springer-Verlag, 2006, ISBN: 3-540-37215-6. Slides.\n\n% Adding Syntax Error Repair to a Java-based Parser Generator, P. van der Spek, N. Plat and C. Pronk. ACM SIGPLAN Notices, 40(4):47-50. April 2005.</pre>\n</div>\n\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n  <div class=\"bibbase_group_whole\" id=\"group_2005\">\n    <div class=\"bibbase_group\"\n      onclick=\"toggleGroup('group_2005')\"\n      onkeypress=\"toggleGroup('group_2005')\"\n      tabindex=\"0\">\n      <i class=\"fa fa-angle-down bibbase_group_head_icon\"></i>&nbsp;\n      <span>2005</span>\n      <span class=\"bibbase_group_count\">\n        \n        (1)\n        \n      </span>\n    </div>\n    <div class=\"bibbase_group_body\">\n      \n  \n  <div class=\"bibbase_paper\" id=\"fitzgerald-larsen-mukherjee-plat-verhoef-validateddesignsforobjectorientedsystems-2005\">\n  <span class=\"bibbase_paper_titleauthoryear\">\n\n  \n  <span class=\"bibbase_paper_title\">\n  \n  \n  \n  <a href=\"http://www.vdmbook.com\"\n     onclick=\"return trackOutboundLink('publications', 'click', 'fitzgerald-larsen-mukherjee-plat-verhoef-validateddesignsforobjectorientedsystems-2005', 'http://www.vdmbook.com', event);\">\n    Validated Designs for Object–oriented Systems.\n  </a>\n  \n  \n  \n</span>\n\n  <span class=\"bibbase_paper_author\">\n  Fitzgerald, J.; Larsen, P. G.; Mukherjee, P.; Plat, N.;  and Verhoef, M.\n</span>\n\n  \n\n</span>\n\n  Springer, New York,  2005.\n  <span class=\"note\"></span>\n\n<span class=\"bibbase_note\"></span>\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content dontprint\">\n\n  \n  <a href=\"http://www.vdmbook.com\"\n     onclick=\"log_download('fitzgerald-larsen-mukherjee-plat-verhoef-validateddesignsforobjectorientedsystems-2005', 'http://www.vdmbook.com', event.ctrlKey, event)\">\n    <img src=\"//bibbase.org/img/filetypes/link.svg\"\n\t     alt=\"Validated Designs for Object–oriented Systems [link]\"\n       title=\"Paper\"\n\t     class=\"bibbase_icon\"\n         ><span class=\"bibbase_icon_text\">Paper</span></a>\n  &nbsp;\n  \n\n  \n\n  \n  <a href=\"//bibbase.org/network/publication/fitzgerald-larsen-mukherjee-plat-verhoef-validateddesignsforobjectorientedsystems-2005\"\n     class=\"bibbase bibbase_page link\">link</a>\n  &nbsp;\n  \n\n  <a href=\"#\"\n     onclick=\"showBib(event); return false;\"\n     class=\"bibbase bibtex link\">bibtex\n    <i class=\"fa fa-caret-down\"></i></a>\n\n  \n\n  \n\n  <!-- <a class=\"bibbase read link hidden\" -->\n  <!--    href=\"javascript:toggleRead('fitzgerald-larsen-mukherjee-plat-verhoef-validateddesignsforobjectorientedsystems-2005')\" -->\n  <!--    title=\"Marking this paper as read adds it to your library on BibBase.\" -->\n  <!--    > -->\n  <!--   <i class=\"fa fa-check\"></i>&nbsp; -->\n  <!--   <span>mark as read</span> -->\n  <!-- </a> -->\n\n  &nbsp;\n  \n  \n\n</span>\n\n<div class=\"well well-small bibbase\" data-type=\"bibtex\"\n     style=\"display:none\">\n  <pre style=\"white-space: pre-wrap;\">@BOOK{Fitzgerald&amp;05,\n  KEY           = &quot;Fitzgerald\\&amp;05&quot;,\n  AUTHOR        = &quot;John Fitzgerald and Peter Gorm Larsen and Paul Mukherjee and\n                   Nico Plat and Marcel Verhoef&quot;,\n  TITLE         = &quot;{Validated Designs for Object--oriented Systems}&quot;,\n  PUBLISHER     = &quot;Springer, New York&quot;,\n  YEAR          = &quot;2005&quot;,\n  URL           = &quot;http://www.vdmbook.com&quot;,\n  ISBN          = &quot;1-85233-881-4&quot;,\n  ANNOTE        = &quot;&quot;,\n  COMMENT       = &quot;PGL&quot;}\n  \n% Validated Designs for Object-oriented Systems (in Japanese), Hiroshi Sakoh, 2010, ISBN-10: 479811961X (Amazon link).\n\n%G VDM TUTOR FORMAL\n</pre>\n</div>\n\n\n\n</div>\n\n\n\n\n\n    </div>\n  </div>\n\n\n\n\n  </div>\n\n\n  <!-- Modal -->\n\n  <!-- <iframe id=\"bibbase_network_frame\" -->\n  <!--         src=\"//bibbase.org/network/control\" -->\n  <!--         style=\"display: none;\"> -->\n  <!-- </iframe> -->\n\n</div>\n"}; document.write(bibbase_data.data);