%G VDM APPLI IFADPUB OBJECT VDM++
@INPROCEEDINGS{Agerholm&99,
  KEY           = "Agerholm\&99",
  AUTHOR        = "Sten Agerholm and Wendy Schafer",
  EDITOR        = "John Fitzgerald and Peter Gorm Larsen",
  TITLE         = "{Analyzing SAFER using UML and VDM++}",
  BOOKTITLE     = "VDM in Practice",
  YEAR          = "1999",
  MONTH         = "September",
  PAGES         = "139--141",
  NOTE          = "",
  ANNOTE        = "",
  COMMENT       = "PGL"}

%G VDM VDM++
@INPROCEEDINGS{Andrews&07,
  KEY           = "Andrews\&07",
  AUTHOR        = "Z. H. Andrews and J. S. Fitzgerald and M. Verhoef",
  TITLE         = "{Resilience Modelling through Discrete Event and Continuous Time Co-Simulation}",
  BOOKTITLE     = "{Proc. 37th Annual IFIP/IEEE Intl. Conf. on Dependable Systems and Networks (Supp. Volume)}",
  PUBLISHER     = "IEEE Computer Society",
  YEAR          = "2007",
  MONTH         = "June",
  PAGES         = "350--351"}

%G VDM APPLI VDM++ OBJECT UML
@INPROCEEDINGS{Berg&99a,
  KEY           = "Berg\&99a",
  AUTHOR        = "Manuel van den Berg and Marcel Verhoef and Mark Wigmans",
  EDITOR        = "John Fitzgerald and Peter Gorm Larsen",
  TITLE         = "{Formal Specification of an Auctioning System Using
                    VDM++ and UML -- an Industrial Usage Report}",
  BOOKTITLE     = "VDM in Practice",
  YEAR          = "1999",
  MONTH         = "September",
  PAGES         = "85--93",
  NOTE          = "",
  ANNOTE        = "",
  COMMENT       = "PGL"}

%G VDM++ ADA
@TECHREPORT{vice-mbdf-17,
  KEY           = "Bousquet00",
  AUTHOR        = "Fabian Bousquet",
  TITLE         = "{VDM++ to Ada95 Translation Rules}",
  INSTITUTION   = "Matra BAe Dynamics",
  ADDRESS       = "Rue Grange Dame Rose 20/22, 78141 Velizy-Villacoublay, France",
  YEAR          = "2000",
  NUMBER        = "VICE-MBDF-17",
  ANNOTE        = "",
  COMMENT       = "We have a softcopy PGL"}

%G VDM VDM++
@INPROCEEDINGS{Bryans&07,
  KEY           = "Bryans\&07",
  AUTHOR        = "J. W. Bryans and J. S. Fitzgerald and P.
                   Periorellis",
  TITLE         = "{A Formal Approach to Dependable Evolution of Access
                    Control Policies in Dynamic Collaborations}",
  BOOKTITLE     = "{Proc. 37th Annual IEEE/IFIP Intl. Conf. on
                    Dependable Systems and Networks}",
  YEAR          = "2007",
  MONTH         = "June",
  PAGES         = "352--353",
  NOTE          = "{Also Technical Report CS-TR-1027, School of
                    Computing Science, Newcastle University.}",
  COMMENT       = ""}

%G VDM APPLI VDM++
@TECHREPORT{Bryans&07b,
  KEY           = "Bryans\&07b",
  AUTHOR        = "J. W. Bryans and J. S. Fitzgerald",
  TITLE         = "{Formal Engineering of XAML Access Control Policies
                    in VDM++}",
  INSTITUTION   = "Newcastle University",
  ADDRESS       = "School of Computing Science",
  YEAR          = "2007",
  MONTH         = "June",
  NUMBER        = "CS-TR-1028",
  SIZE          = "20",
  COMMENT       = "To appear in Proceeedings of ICFEM 2007, November
                   2007, Springer-Verlag Lecture notes in Computer Science"}

%G VDM APPLI VDM++
@INPROCEEDINGS{Bryans&07c,
  KEY           = "Bryans\&07",
  AUTHOR        = "J. W. Bryans and J. S. Fitzgerald",
  EDITOR        = "M. Butler and M. Hinchey and M.M. Larrondo-Petrie",
  TITLE         = "{Formal Engineering of XAML Access Control Policies
                    in VDM++}",
  BOOKTITLE     = "ICFEM 2007",
  PUBLISHER     = "Springer-Verlag",
  ADDRESS       = "Berlin Heidelberg",
  YEAR          = "2007",
  MONTH         = "November",
  PAGES         = "37--56",
  ANNOTE        = "",
  COMMENT       = "BIB PGL"}

%G VDM AFRODITE OBJECT VDM++
@TECHREPORT{Durr92a,
  KEY           = "D{\"u}rr92",
  AUTHOR        = "E.H.H.\ D{\"u}rr",
  TITLE         = "Syntactic Description of the VDM++ Language",
  ADDRESS       = "CAP Gemini, P.O.Box 2575, 3500 GN Utrecht, NL",
  YEAR          = "1992",
  MONTH         = "September",
  SIZE          = "38",
  ANNOTE        = "",
  COMMENT       = "BIB. PGL"}

%G VDM++ VDM OBJECT
@PHDTHESIS{Durr94,
   KEY          = "D{\"{u}}rr94",
   AUTHOR       = "Eug\`{e}ne D{\"u}rr",
   TITLE        = "{The Use of Object-oriented Specifications in Physics}",
   SCHOOL       = "Utrecht University",
   ADDRESS      = "Utrecht, The Netherlands",
   YEAR         = "1994",
   MONTH        = oct,
   ANNOTE       = "",
   COMMENT      = "I have a copy PGL"}

%G VDM OBJECT VDM++
@INPROCEEDINGS{Durr&92,
  KEY           = "D{\"u}rr\&92",
  AUTHOR        = "E.\ D{\"u}rr and J.v.\ Katwijk",
  TITLE         = "{VDM++, A Formal Specification Language for Object Oriented
                   Designs}",
  BOOKTITLE     = "{COMP EURO 92}",
  PUBLISHER     = "IEEE",
  YEAR          = "1992",
  MONTH         = "May",
  PAGES         = "214--219",
  ANNOTE        = "",
  COMMENT       = "BIB. PGM"}

%G VDM OBJECT VDM++
@INPROCEEDINGS{Durr&92b,
   KEY          = "D{\"{u}}rr\&92",
   AUTHOR       = "E.H. D{\"u}rr and J. van Katwijk",
   EDITOR       = "Georg Heeg, Boris Magnusson, Bertrand Meyer",
   TITLE        = "{VDM++  -- A Formal Specification Language for
                    Object-oriented Designs}",
   BOOKTITLE    = "Technology of Object-oriented Languages and Systems",
   PUBLISHER    = "Prentice-Hall International",
   NOTE         = "Proceedings of Tools Europe '92",
   PAGES        = "63--78",
   YEAR         = "1992",
   ANNOTE       = "",
   COMMENT      = "NP has a copy PGL"}

%G VDM OBJECT VDM++
@INPROCEEDINGS{Durr&92c,
   KEY          = "D{\"{u}}rr\&92",
   AUTHOR       = "E.H. D{\"u}rr, W. Lourens, J. van Katwijk",
   EDITOR       = "D. Perret-Gallix",
   TITLE        = "{The Use of the Formal Specification Language VDM++ for
                  Data Acquisition Systems}",
   BOOKTITLE    = "New Computing Techniques in Physics Research II",
   PUBLISHER    = "World Scientific Publishing Co.",
   ADDRESS      = "Singapore",
   PAGES        = "47--52",
   NOTE         = "Proceedings of the 2nd CERN Workshop on Software
                   Engineering",
   MONTH        = "January",
   YEAR         = "1992",
   ANNOTE       = "",
   COMMENT      = "NA PGL"}

%G AFRODITE VDM++
@TECHREPORT{Durr&93b,
  KEY           = "D{\"u}rr\&93",
  AUTHOR        = "E.H.\ D{\"u}rr, A.\ Duursma, and N.\ Plat",
  TITLE         = "VDM++ Language Reference Manual",
  INSTITUTION   = "CAP Gemini Innovation",
  YEAR          = "1993",
  MONTH         = "July",
  SIZE          = "65",
  ANNOTE        = "",
  COMMENT       = "PBL has a hard-copy"}

%G VDM++ VDM OBJECT
@INPROCEEDINGS{Durr&93c,
  KEY          = "D{\"{u}}rr\&93",
  AUTHOR       = "E.H. D{\"u}rr and E.M. Dusink",
  TITLE        = "{Principles of Tracking and Tracing in CombiCom}",
  BOOKTITLE    = "Proceedings of the Drive Technical Conference",
  PUBLISHER    = "DG XIII",
  NOTE         = "Brussels, Belgium",
  YEAR         = "1993",
  ANNOTE        = "",
  COMMENT       = "NP has a copy"}

%G VDM++ VDM OBJECT
@MISC{Durr&94,
   KEY          = "D{\"{u}}rr\&94",
   AUTHOR       = "Eug\`{e}ne D{\"u}rr and Stephen Goldsack and Nico Plat",
   TITLE        = "{Rigorous Development of Concurrent and Real-Time
                    Object-oriented Systems}",
   NOTE         = "Tutorial presented at TOOLS Europe '94, Versailles, France",
   YEAR         = "1994",
   MONTH        = mar,
   ANNOTE       = "",
   COMMENT      = "NA PGL"}

%G VDM++ VDM OBJECT RAIL
@INBOOK{Durr&95,
  KEY           = "D{\"{u}}rr\&95",
  AUTHOR        = "Eug\`{e}ne D{\"u}rr, Nico Plat and Michiel de Boer",
  TITLE         = "{Applications of Formal Methods}",
  CHAPTER       = "{CombiCom: Tracking and Tracing Rail Traffic using VDM++}",
  PAGES         = "203--225",
  PUBLISHER     = "Prentice-Hall International",
  YEAR          = "1995",
  NOTE          = "ISBN 0-13-3-366949-1",
  ANNOTE        = "",
  COMMENT       = "I have the book PGL"}

%G VDM++ VDM OBJECT
@MISC{Durr&95b,
   KEY          = "D{\"{u}}rr\&95",
   AUTHOR       = "Eug\`{e}ne D{\"u}rr and Stephen Goldsack",
   TITLE        = "{The Development of Concurrent and Real-Time
                    Systems using VDM++}",
   YEAR         = "1995",
   MONTH        = "June",
   ANNOTE       = "",
   COMMENT      = "NKK"}

%G VDM VDM++ OBJECT REAL-TIME
@INBOOK{Durr&96,
  KEY           = "D{\"{u}}rr\&96",
  AUTHOR        = "Eug\`{e}ne D{\"u}rr and Stephen Goldsack",
  EDITOR        = "S.J. Goldsack and S.J.H. Kent",
  TITLE         = "Formal Methods and Object Technology",
  CHAPTER       = "6 Concurrency and Real-Time in VDM++",
  PAGES         = "86--112",
  PUBLISHER     = "Springer-Verlag",
  ADDRESS       = "London",
  YEAR          = "1996",
  NOTE          = "ISBN 3-540-19977-2",
  ANNOTE        = "",
  COMMENT       = "LIB PGL"}

%G AFRODITE VDM++ VDM OBJECT
@TECHREPORT{AFROCGEDLRM,
  KEY           = "D{\"{u}}rr\&95",
  AUTHOR        = "E.H. D{\"u}rr and N. Plat (editor)",
  TITLE         = "{VDM++ Language Reference Manual}",
  INSTITUTION   = "Cap Volmac",
  YEAR          = "1995",
  MONTH         = "August",
  TYPE          = "Afrodite (ESPRIT-III project number 6500) document",
  NUMBER        = "",
  NOTE          = "Outdated by \cite{LangManPP}",
  ANNOTE        = "",
  NOTE          = "\\Afrodite Doc.id : AFRO/CG/ED/LRM/V11"}


%%%%%%%%%%
%%%%%%%%%% E E E E E E E E E E E E E E E E E E E E E E E E E
%%%%%%%%%%

%G VDM++
@BOOK{Ellenbogen&05,
  KEY           = "Ellenbogen\&05",
  AUTHOR        = "K. A. Ellenbogen and M. A. Wood",
  TITLE         = "{Cardiac Pacing and ICDs}",
  EDITION       = "4th",
  PUBLISHER     = "Blackwell",
  YEAR          = "2005"}

%G VDM VDM++
@TECHREPORT{Fitzgerald&07b,
  KEY           = "Fitzgerald\&07",
  AUTHOR        = "John Fitzgerald and Peter Gorm Larsen and Simon Tjell and
                   Marcel Verhoef",
  TITLE         = "{Validation Support for Distributed Real-Time Embedded
                   Systems in VDM++}",
  INSTITUTION   = "{School of Computing Science, Newcastle University}",
  YEAR          = "2007",
  MONTH         = "April",
  SIZE          = "18",
  NUMBER        = "{CS-TR:1017}"}

%G VDM VDM++
@TECHREPORT{Fitzgerald&07d,
  KEY           = "Fitzgerald\&07d",
  AUTHOR        = "J. S. Fitzgerald and P. G. Larsen and S. Tjell and M. Verhoef",
  TITLE         = "{Validation Support for Real-Time Embedded Systems in VDM++}",
  INSTITUTION   = "School of Computing Science, Newcastle University",
  NUMBER        = "CS-TR-1017",
  MONTH         = "April",
  SIZE          = "18",
  YEAR          = "2007",
  NOTE          = "{Revised version in Proc. 10th IEEE High
                    Assurance Systems Engineering Symposium, November,
                    2007, Dallas, Texas, IEEE}",
  COMMENT       = "I have the source (JSF)"}

%G VDM VDM++
@INPROCEEDINGS{Fitzgerald&07h,
  KEY           = "Fitzgerald\&07h",
  AUTHOR        = "J. S. Fitzgerald and P. G. Larsen and S. Tjell and M. Verhoef",
  TITLE         = "{Validation Support for Real-Time Embedded Systems in VDM++}",
  BOOKTITLE     = "Proc. HASE 2007: 10th IEEE High Assurance Systems Engineering Symposium",
  EDITOR        = "Bojan Cukic and Jing Dong",
  MONTH         = "November",
  PAGES         = "331--340",
  YEAR          = "2007",
  PUBLISHER     = "{IEEE}",
  COMMENT       = "I have the source (JSF)"}

%G AFRODITE VDM OBJECT PROTO VDM++
@TECHREPORT{Fokma93,
  KEY           = "Fokma93",
  TITLE         = "{A VDM++ Code Generator}",
  INSTITUTION   = "CAP Gemini Innovation",
  ADDRESS       = "P.O.Box 2575, 3500 GN Etrecht, NL",
  YEAR          = "1993",
  MONTH         = "May",
  SIZE          = "60",
  ANNOTE        = "",
  COMMENT       = ""}


%G VDM++ VDM OBJECT
@INPROCEEDINGS{Goldsack&95,
  KEY           = "Goldsack\&95",
  AUTHOR        = "Stephen J.\ Goldsack, Eugene D{\"u}rr and Nico Plat",
  EDITOR        = "M.\ Wirsing",
  TITLE         = "Object Reification in VDM++",
  BOOKTITLE     = "{ICSE-17 Workshop on Formal Methods Application in
		   Software Engineering Practice}",
  YEAR          = "1995",
  MONTH         = "24--25 April",
  PAGES         = "194--201",
  ANNOTE        = "",
  COMMENT       = "I have a copy PGL"}

%G VDM VDM++ OBJECT REFIN
@ARTICLE{Goldsack&96,
  KEY           = "Goldsack\&96",
  AUTHOR        = "Stephen Goldsack and Kevin Lano",
  TITLE         = "{Annealing and Data Decomposition in VDM}",
  JOURNAL       = "ACM Sigplan Notices",
  YEAR          = "1996",
  MONTH         = "April",
  VOLUME        = "31",
  NUMBER        = "4",
  PAGES         = "32--38",
  ANNOTE        = "",
  COMMENT       = "We have the journal PGL"}

%G OBJECT FORMAL VDM VDM++
@BOOK{Goldsack&96a,
  KEY           = "Goldsack\&96",
  EDITOR        = "S.J. Goldsack and S.J.H. Kent",
  TITLE         = "Formal Methods and Object Technology",
  PUBLISHER     = "Springer-Verlag",
  ADDRESS       = "London",
  YEAR          = "1996",
  SIZE          = "368",
  NOTE          = "",
  ANNOTE        = "",
  COMMENT       = "LIB PGL"}

%G VDM OBJECT VDM++
@INPROCEEDINGS{Goldsack&99,
  KEY           = "Goldsack\&99",
  AUTHOR        = "Stephen Goldsack and Kevin Lano",
  EDITOR        = "John Fitzgerald and Peter Gorm Larsen",
  TITLE         = "{Invariants as Design Templates in Object-based Systems}",
  BOOKTITLE     = "VDM in Practice",
  YEAR          = "1999",
  MONTH         = "September",
  PAGES         = "13--27",
  NOTE          = "",
  ANNOTE        = "",
  COMMENT       = "PGL"}

%G VDM++ VDM OBJECT
@INPROCEEDINGS{Holzapfel&89,
   KEY          = "Holzapfel\&89",
   AUTHOR       = "R.\ Holzapfel and G.\ Winterstein",
   TITLE        = "{VDM++  -- A Formal Specification Language for
                    Object-oriented Designs}",
   BOOKTITLE    = "Ada in Industry, Proceedings of the Ada-Europe
                   Conference 1988",
   PUBLISHER    = "Cambridge University Press, Great Brittain",
   YEAR         = "1989"}

%G VDM++
@TECHREPORT{CGManPP,
  KEY           = "CGManPP",
  AUTHOR        = "The VDM Tool Group",
  TITLE         = "The VDM++ to C++ Code Generator",
  INSTITUTION   = "CSK Systems",
  YEAR          = "2008",
  MONTH         = "January",
  ANNOTE        = "",
  URL           = "http://www.vdmtools.jp/en/",
  COMMENT       = "ABMN"}

%G VDM++ VDM OBJECT
@TECHREPORT{LangManPP,
  KEY           = "LangManPP",
  AUTHOR        = "The VDM Tool Group",
  TITLE         = "{The IFAD VDM++ Language}",
  INSTITUTION   = "CSK Systems",
  YEAR          = "2008",
  MONTH         = "January",
  ANNOTE        = "",
  URL           = "http://www.vdmtools.jp/en/",
  URL           = "\\ ftp://ftp.ifad.dk/pub/vdmtools/doc/langmanpp\_letter.pdf",
  NOTE          = "\\ ftp://ftp.ifad.dk /pub/vdmtools/doc/langmanpp\_letter.pdf",
  COMMENT       = "ABMN"}

%G VDM++ VDM OBJECT TOOL
@TECHREPORT{UMLMan,
  KEY           = "UMLMan",
  AUTHOR        = "The-VDM-Tool-Group",
  TITLE         = "{The Rose-VDM++ Link}",
  INSTITUTION   = "CSK Systems",
  YEAR          = "2008",
  MONTH         = "January",
  ANNOTE        = "",
  URL           = "http://www.vdmtools.jp/en/",
  COMMENT       = "ABMN"}

%G VDM VDM++
@INPROCEEDINGS{Ishikawa&09,
  KEY           = "Ishikawa\&09",
  AUTHOR        = "Fuyuki Ishikawa and Kenji Taguchi and Shinichi Honiden",
  TITLE         = "{How Top-Level Engineers Learn and Investigate
                    VDM: Experiences in the Top SE Project}",
  NOTE          = "The 7th Overture workshop at FM'09",
  YEAR          = "2009",
  MONTH         = "November",
  ANNOTE        = "",
  COMMENT       = "I have the source (PGL)"}

%G VDM OBJECT VDM++
@INPROCEEDINGS{Katwijk&97,
  KEY           = "Katwijk\&97",
  AUTHOR        = "van Katwijk, J. D{\"u}rr, E. and  Goldsack, S.",
  TITLE         = "Hybrid object-oriented real-time software development with
                   VDM++",
  BOOKTITLE     = "First IEEE International Conference on Formal
                   Engineering Methods",
  ORGANIZATION  = "IEEE",
  PUBLISHER     = "IEEE",
  YEAR          = "1997",
  MONTH         = "November",
  PAGES         = "17-26",
  ANNOTE        = "",
  COMMENT       = "BIB PGL"}

%G VDM VDM++
@MISC{kent&93,
  KEY           = "Kent\&93",
  AUTHOR        = "Stuart Kent and Richard Moore",
  TITLE         = "An Axiomatic Semantics for VDM++: OO Aspects",
  TEXT          = "Kent S.J.H. An axiomatic semantics for vdm++: Oo aspects
                   (version 1). Technical Report AFRO/IC/SK/OOSem/V1,
                   ESPRIT Project 6500 Afrodite, Imperial College,
                   London, May 1993.",
  YEAR          = "1993",
  URL           = "citeseer.ist.psu.edu/kent93axiomatic.html",
  COMMENT       = "BIB PGL" }

%G VDM OBJECT VDM++ APPLI
@ARTICLE{Koumbis&96,
  KEY           = "Koumbis\&96",
  AUTHOR        = "A. Koumbis and Alejandro Moya",
  TITLE         = "{Venus becomes Goddess of the seas?}",
  JOURNAL       = "I\&T Margazine",
  YEAR          = "1996",
  MONTH         = "April",
  NUMBER        = "19",
  PAGES         = "22--25",
  ANNOTE        = "",
  COMMENT       = "We have the journal PGL"}

%G VDMPP VDM++ VDM
@INPROCEEDINGS{Kurita&05,
  KEY           = "Kurita&05",
  AUTHOR        = "Taro Kurita and Toyokazu Oota and Yasumasa Nakatsugawa",
  TITLE         = "{Formal Specification of an Embedded {IC} for Cellular Phones}",
  BOOKTITLE     = "Proceedings of Software Symposium 2005",
  PUBLISHER     = "Software Engineers Associates of Japan",
  YEAR          = "2005",
  MONTH         = "June",
  PAGES         = "73-80",
  NOTE          = "(in Japanese)",
  ISBN		= "ISBN 4-916227-18-2"}

%G VDM VDMPP VDM++ INDUSTR APPLY
@INPROCEEDINGS{Kurita&08,
  KEY           = "Kurita\&08",
  AUTHOR        = "Taro Kurita and Miki Chiba and Yasumasa Nakatsugawa",
  TITLE         = "{Application of a Formal Specification Language in the Development of the ``Mobile FeliCa'' IC Chip Firmware for Embedding in Mobile Phone}",
  BOOKTITLE     = "FM 2008: Formal Methods",
  EDITOR        = "J. Cuellar and T. Maibaum and K. Sere",
  PUBLISHER     = "Springer-Verlag",
  SERIES        = "{Lecture Notes in Computer Science}",
  YEAR          = "2008",
  MONTH         = "May",
  PAGES         = "425--429"
}

%G VDM VDMPP VDM++ INDUSTR APPLY
@ARTICLE{Kurita&09,
  KEY           = "Kurita\&09",
  AUTHOR        = "T. Kurita and Y. Nakatsugawa",
  TITLE         = "{The Application of VDM++ to the Development of Firmware
                   for a Smart Card IC Chip}",
  JOURNAL       = "Intl. Journal of Software and Informatics",
  VOLUME        = "3",
  NUMBER        = "2-3",
  YEAR          = "2009",
  MONTH         = "October"
}

G ABSTRA
@inproceedings{Kurtz80,
	author={Barry L. Kurtz},
	year={1980},
	title={Investigating the relationship between the development of abstract reasoning and performance in an introductory programming class},
	booktitle={SIGCSE '80: Proceedings of the eleventh SIGCSE technical symposium on Computer science education},
	publisher={ACM Press},
	location={Kansas City, Missouri, United States},
	pages={110-117},
	isbn={0-89791-013-3}
}

%G VDM OBJECT VDM++
@INBOOK{Lano&93,
   KEY          = "Lano\&93",
   EDITOR       = "Kevin Lano and Howard Haughton",
   TITLE        = "{Object-oriented Specification Case Studies}",
   CHAPTER      = "6: Object-oriented Specification in VDM++",
   PUBLISHER    = "Prentice-Hall International",
   YEAR         = "1993",
   SERIES       = "Object-oriented Series",
   ANNOTE       = "",
   COMMENT      = "NP has a copy (PGL)"}

%G VDM VDM++ OBJECT
@MISC{Lano94,
  KEY           = "Lano94",
  AUTHOR        = "K. Lano",
  TITLE         = "Reasoning Techniques in VDM++",
  URL           = "citeseer.ist.psu.edu/lano94reasoning.html",
  COMMENT       = "BIB PGL" }

%G VDM VDM++ OBJECT
@MISC{Lano94b,
  KEY           = "Lano94",
  AUTHOR        = "K. Lano",
  TITLE         = "Expressing the Semantics of VDM++ in RTL",
  URL           = "citeseer.ist.psu.edu/lano94expressing.html",
  COMMENT       = "BIB PGL" }

%G REFIN OBJECT VDM VDM++
@INPROCEEDINGS{Lano&94,
  KEY           = "Lano\&94",
  AUTHOR        = "K.Lano, S.Goldsack",
  EDITOR        = "C.Hankin, I.Mackie",
  TITLE         = "Refinement, Subtyping and Subclassing in VDM++",
  BOOKTITLE     = "2nd Theory and Formal Methods Workshop, Cambridge",
  PUBLISHER     = "IC Press",
  YEAR          = "1995",
  ANNOTE        = "",
  COMMENT       = "ABMN"}

%G VDM OBJECT VDM++ VDMRT
@INPROCEEDINGS{Lano95a,
  KEY           = "Lano95",
  AUTHOR        = "K.Lano",
  EDITOR        = "",
  TITLE         = "Distributed System Specification in VDM++",
  BOOKTITLE     = "Proceedings of the 8th International Conference on Formal De                   scription Techniques (FORTE '95)",
  PUBLISHER     = "Chapman and Hall",
  YEAR          = "1995",
  COMMENT       = "ABMN"}

%G OBJECT VDM VDM++
@BOOK{Lano95b,
  KEY           = "Lano95",
  AUTHOR        = "K.Lano",
  TITLE         = "Formal Object-oriented Development",
  PUBLISHER     = "Springer Verlag",
  YEAR          = "1995",
  SERIES        = "Springer Verlag FACIT series",
  SIZE          = "436",
  NOTE          = "",
  ANNOTE        = "",
  COMMENT       = "ABMN"}

%G VDM OBJECT VDM++
@INPROCEEDINGS{Lano&95a,
  KEY           = "Lano\&95",
  AUTHOR        = "K.Lano, S.Goldsack",
  TITLE         = "Discrete Event Process Controller Synthesis in VDM++",
  BOOKTITLE     = "First IEEE International Conference on Engineering of Comple                   x Computer Systems (ICECCS '95)",
  PUBLISHER     = "IEEE Press",
  YEAR          = "1995",
  ANNOTE        = "",
  COMMENT       = "BIB ABMN"}

%G VDM OBJECT VDM++
@INPROCEEDINGS{Lano&95b,
  KEY           = "Lano\&95",
  AUTHOR        = "K.Lano, S.Goldsack",
  TITLE         = "Specifying Discrete Event Systems in VDM++",
  BOOKTITLE     = "International Workshop on Analysis and Design of Event-Drive                   n Operations in Process Systems, London",
  PUBLISHER     = "",
  YEAR          = "1995",
  MONTH         = "April",
  ANNOTE        = "",
  COMMENT       = "ABMN"}

%G VDM++ VDM OBJECT
@INPROCEEDINGS{Lano&96a,
  KEY           = "Lano\&96",
  AUTHOR        = "K.Lano and S.Goldsack",
  TITLE         = "Integrated Formal and Object-oriented Methods: The
                   VDM++ Approach",
  BOOKTITLE     = "In proceedings of Methods Integration Workshop",
  ORGANIZATION  = "Leeds Metropolitan University",
  PUBLISHER     = "(Supported by BCS FACS)",
  YEAR          = "1996",
  MONTH         = "March",
  ANNOTE        = "",
  COMMENT       = "ABMN"}

%G VDM++ VDM OBJECT
@INPROCEEDINGS{Lano&96,
  KEY           = "Lano\&96",
  AUTHOR        = "K.Lano and S.Goldsack",
  EDITOR        = "",
  TITLE         = "Object-oriented Formal Development",
  BOOKTITLE     = "TOOLS Europe'96",
  ORGANIZATION  = "",
  PUBLISHER     = "",
  ADDRESS       = "",
  YEAR          = "1996",
  MONTH         = "",
  PAGES         = "",
  SIZE          = "",
  NOTE          = "",
  ANNOTE        = "",
  COMMENT       = "ABMN"}

%G VDM++ VDM OBJECT
@TECHREPORT{Lano96b,
  KEY           = "Lano96",
  AUTHOR        = "Kevin Lano",
  TITLE         = "{Transforming Sequential Specifications into
                    Concurrent and Distributed Implementations}",
  INSTITUTION   = "Imperial College",
  YEAR          = "1996",
  SIZE          = "20",
  NOTE          = "presented at the 1996 MEDICIS workshop at the
                   University of Barcelona",
  ANNOTE        = "",
  COMMENT       = "BIB PGL"}

%G VDM++ VDM OBJECT
@INPROCEEDINGS{Lano&96b,
  KEY           = "Lano\&96",
  AUTHOR        = "K.Lano and S.Goldsack",
  TITLE         = "Refinement of Distributed Object Systems",
  BOOKTITLE     = "Proceedings of ``Workshop on Formal Methods for Open
                  Object-based Distributed Systems''",
  ORGANIZATION  = "",
  PUBLISHER     = "Chapman and Hall",
  ADDRESS       = "",
  YEAR          = "1996",
  PAGES         = "",
  SIZE          = "",
  NOTE          = "",
  COMMENT       = "ABMN"}

%G VDM VDM++ OBJECT
@INPROCEEDINGS{Lano&96c,
  KEY           = "Lano\&96",
  AUTHOR        = "Kevin Lano, Juan Bicarregui and Stephen Goldsack",
  TITLE         = "Formaling Design Patterns",
  BOOKTITLE     = "Northern Formal Methods Workshop",
  PUBLISHER     = "Springer-Verlag",
  YEAR          = "1996",
  MONTH         = "September",
  SIZE          = "20",
  ANNOTE        = "",
  COMMENT       = "BIB PGL"}

%G FME97 VDM++ VDM OBJECT		
@InProceedings{Lano&97a,
  KEY           = "Lano\&97",
  AUTHOR        = {K. Lano and A. Sanchez},
  TITLE         = {Design of Reactive Control Systems for Event-Driven Operations},
  BOOKTITLE     = {FME'97: Industrial Applications and Strengthened
  Foundations of Formal Methods (Proc. 4th Intl. Symposium of Formal
  Methods Europe, Graz, Austria, September 1997)},
  EDITOR        = {John Fitzgerald and Cliff B. Jones and Peter Lucas},
  VOLUME        = {1313},
  SERIES        = {Lecture Notes in Computer Science},
  PUBLISHER     = {Springer-Verlag},
  YEAR          = {1997},
  MONTH         = {September},
  NOTE          = {ISBN 3-540-63533-5},
  PAGES         = {142-161}}

%G FME97 VDM++ VDM OBJECT B		
@INPROCEEDINGS{Lano&97b,
  KEY           = "Lano\&97",
  AUTHOR        = {K. Lano and J. Bicarregui and J. Fiadeiro and A. Lopes},
  TITLE         = {Specification of Required Non-determinism},
  BOOKTITLE     = {FME'97: Industrial Applications and Strengthened
  Foundations of Formal Methods (Proc. 4th Intl. Symposium of Formal
  Methods Europe, Graz, Austria, September 1997)},
  EDITOR        = {John Fitzgerald and Cliff B. Jones and Peter Lucas},
  VOLUME        = {1313},
  SERIES        = {Lecture Notes in Computer Science},
  PUBLISHER     = {Springer-Verlag},
  YEAR          = {1997},
  MONTH         = {September},
  NOTE          = {ISBN 3-540-63533-5},
  PAGES         = {298--317}}

%G VDM++ VDMRT VDM
@INPROCEEDINGS{Lano&97c,
  KEY           = "Lano\&97",
  AUTHOR        = "Kevin Lano and Stephen Goldsack and Juan Bicarregui and
                   Stuart Kent",
  EDITOR        = "",
  TITLE         = "Integrating VDM++ and Real-Time System Design",
  BOOKTITLE     = "Proceedings of the 10th International Conference of Z
                   Users on The Z Formal Specification Notation ",
  PUBLISHER     = "LNCS",
  YEAR          = "1997",
  MONTH         = "",
  PAGES         = "188 -- 219",
  SIZE          = "",
  NOTE          = "ISBN:3-540-62717-0",
  ANNOTE        = "",
  COMMENT       = "BIB PGL"}

%G VDM VDM++
@ARTICLE{Larsen&08,
  KEY           = "Larsen\&08",
  AUTHOR        = "Peter Gorm Larsen and John S.\ Fitzgerald and Steve Riddle",
  TITLE         = "{Practice-oriented courses in formal methods using VDM++}",
  JOURNAL       = "Formal Aspects of Computing",
  YEAR          = "2008",
  MONTH         = "February",
  VOLUME        = "DOI 10.1007/s00165-008-0068-5",
  ANNOTE        = "",
  COMMENT       = "BIB PGL"}

%G VDM VDM++
@INPROCEEDINGS{Larsen&08a,
  KEY           = "Larsen\&08a",
  AUTHOR        = "P.G. Larsen and J. S. Fitzgerald",
  EDITOR        = "P. Boca and J. P. Bowen",
  BOOKTITLE     = "{Proc. BCS-FACS Workshop on Formal Methods in Industry}",
  TITLE         = "{Recent Industrial Applications of Formal Methods in Japan}",
  PUBLISHER     = "British Computer Society",
  YEAR          = "2008"}

%G VDM VDM++ APPLI
@MASTERSTHESIS{Macedo07a,
  KEY           = "Macedo07",
  AUTHOR        = "Hugo Macedo",
  TITLE         = "{Validating and Understanding Boston Scientific Pacemaker
                   Requirements}",
  SCHOOL        = "Minho University",
  ADDRESS       = "Portugal",
  YEAR          = "2007",
  MONTH         = "October",
  ANNOTE        = "",
  COMMENT       = "I have a copy PGL"}

%G VDM VDM++ APPLI
@MISC{Macedo07b,
  KEY           = "Macedo07",
  AUTHOR        = "Hugo Macedo",
  TITLE         = "{VDM models of the Pacemaker Challenge}",
  NOTE          = "http://www.vdmportal.org/twiki/bin/view/Main/PacemakerCaseStudy",
  YEAR          = "2007",
  ANNOTE        = "",
  COMMENT       = ""}

%G VDM VDM++ APPLI VDMRT
@INPROCEEDINGS{Macedo&08,
  KEY           = "Macedo\&08",
  AUTHOR        = "Hugo Daniel Macedo and Peter Gorm Larsen and John Fitzgerald ",
  TITLE         = "{Incremental Development of a Distributed Real-Time Model
                    of a Cardiac Pacing System using VDM}",
  BOOKTITLE     = "FM 2008: Formal Methods, 15th International Symposium on Formal Methods",
  EDITOR        = "Jorge Cuellar and Tom Maibaum and Kaisa Sere",
  YEAR          = "2008",
  PUBLISHER     = "Springer-Verlag",
  SERIES        = "Lecture Notes in Computer Science",
  VOLUME        = "5014",
  PAGES         = "181--197",
  COMMENT       = ""}

%G VDM++ TEST
@INPROCEEDINGS{Nadeem&06,
  KEY           = "Nadeem\&06",
  AUTHOR        = "Aamer Nadeem and Michael R. Lyu",
  TITLE         = "A Framework for Inheritance Testing from VDM++
                   Specifications",
  BOOKTITLE     = "Dependable Computing, 2006. PRDC '06. 12th Pacific
                   Rim International Symposium on",
  ORGANIZATION  = "INSPEC",
  YEAR          = "2006",
  MONTH         = "December",
  PAGES         = "81-88",
  ANNOTE        = "",
  COMMENT       = "BIB PGL"}

%G VDM TOOL VDM++
@MASTERSTHESIS{Nielsen10b,
  KEY           = "Nielsen10",
  AUTHOR        = "Claus Ballegaard Nielsen",
  TITLE         = "{Dynamic Reconfiguration of Distributed Systems in VDM-RT}",
  SCHOOL        = "Aarhus University",
  YEAR          = "2010",
  MONTH         = "December",
  ANNOTE        = "",
  COMMENT       = "BIB I have a copy (PGL)"}

%G VDM VDM++
@MISC{Overture07,
  KEY           = "Overture07",
  AUTHOR        = "Overture-Core-Team",
  TITLE         = "{Overture Web site}",
  YEAR          = "2007",
  HOWPUBLISHED  = "http://www.overturetool.org",
  ANNOTE        = "",
  COMMENT       = ""}

%G VDM VDM++
@INPROCEEDINGS{Paiva&03,
  KEY           = "Paiva\&03",
  AUTHOR        = "Ana Cristina Paiva, Joao Pascoal Faria, Raul Moreira Vidal",
  TITLE         = "Specification-based Testing of User Interfaces",
  BOOKTITLE     = "The 10th DSV-IS Workshop (Design Specification and
                   Verification of Interactive Systems)",
  ADDRESS       = "Funchal, Madeira",
  YEAR          = "2003",
  MONTH         = "July",
  ANNOTE        = "",
  COMMENT       = "BIB PGL"}

%G AFRODITE VDM++ VDM OBJECT
@TECHREPORT{AFROSTNANPMSAWSpec,
  KEY           = "Plat94",
  AUTHOR        = "Nico Plat",
  TITLE         = "MSAW VDM++ Specification",
  INSTITUTION   = "CAP Volmac",
  YEAR          = "1994",
  MONTH         = "June",
  NOTE          = "\\ Afrodite Doc.id : AFRO/STNA/NP/MSAWSpec/V1"}

%G AFRODITE VDM++ VDM OBJECT
@TECHREPORT{AFROCGNPVPPUM,
  KEY           = "Plat\&95",
  AUTHOR        = "Nico Plat \& Henrik Voss",
  TITLE         = "The VDM++ Toolbox User Manual",
  INSTITUTION   = "CAP Volmac \& IFAD",
  YEAR          = "1995",
  MONTH         = "September",
  NOTE          = "\\ Afrodite Doc.id : AFRO/CG/NP/VPPUM/V5.3"}

%G VDM VDM++
@INPROCEEDINGS{Plat97,
  KEY           = "Plat97",
  AUTHOR        = "Nico Plat",
  TITLE         = "{The Industrial use of VDM++}",
  BOOKTITLE     = "IEE Colloquium on Industrial Use of Formal Methods",
  ORGANIZATION  = "IEE",
  YEAR          = "1997",
  MONTH         = "May",
  ANNOTE        = "",
  COMMENT       = "BIB PGL"}

%G VDM++ VDM OBJECT
@ARTICLE{Rauf&06,
  KEY           = "Rauf\&06",
  AUTHOR        = "Irum Rauf, Aamer Nadeem and Masud Khokhar",
  TITLE         = "Formalizing Object Oriented Design Patterns with Object-Z",
  JOURNAL       = "10th IEEE International Multitopic Conference",
  YEAR          = "2006",
  MONTH         = "December",
  PAGES         = "269-274",
  SIZE          = "5",
  ANNOTE        = "",
  COMMENT       = ""}

%G VDM TEST TOOL VDM++
@MASTERSTHESIS{Santos08,
  KEY           = "Santos08",
  AUTHOR        = "Adriana Sucena Santos",
  TITLE         = "{VDM++ Test Automation Support}",
  SCHOOL        = "{Minho University with exchange to Engineering College of Arhus}",
  YEAR          = "2008",
  MONTH         = "July",
  ANNOTE        = "",
  COMMENT       = "I have the pdf PGL"}

%G VDM VDM++
@INPROCEEDINGS{Sheng&09,
  KEY           = "Sheng\&09",
  AUTHOR        = "Quan Z. Sheng and Jian Yu and Zakaria Maamar and Xitong Li",
  TITLE         = "Compatibility Checking of Heterogeneous Web Service
                   Policies Using VDM++",
  BOOKTITLE     = "2009 World Conference on Services -- I",
  PUBLISHER     = "IEEE",
  ADDRESS       = "Los Angeles, CA",
  YEAR          = "2009",
  MONTH         = "july",
  PAGES         = "821 -- 828",
  ANNOTE        = "",
  COMMENT       = "BIB PGL"}

%G VDM VDM++
@INPROCEEDINGS{Sohail&09,
  KEY           = "Sohail\&09",
  AUTHOR        = "Faheem Sohail and Farooq Zubairi and Nabeel Sabir and
                   Nazir Ahmad Zafar",
  TITLE         = "Designing Verifiable and Reusable Data Access Layer using
                   Formal Methods and Design Patterns",
  BOOKTITLE     = "International Conference on Computer Modeling and
                   Simulation",
  PUBLISHER     = "IEEE",
  YEAR          = "2009",
  MONTH         = "February",
  PAGES         = "167--172",
  ANNOTE        = "",
  COMMENT       = "BIB PGL"}

%G VDM VDM++ VICE
@MASTERSTHESIS{Sorensen&07,
  KEY           = "S\o{}rensen\&07",
  AUTHOR        = "Rasmus Ask S\o{}rensen and Jasper Moltke Nygaard",
  TITLE         = "{Evaluating Distributed Architectures using VDM++
                    Real-Time Modelling with a Proof of Concept Implementation}",
  SCHOOL        = "Enginering College of Aarhus",
  YEAR          = "2007",
  MONTH         = "December",
  ANNOTE        = "",
  COMMENT       = "I have a hard copy (PGL)"}

%G PETRI VDM VDM++
@PHDTHESIS{Tjell09,
  KEY           = "Tjell09",
  AUTHOR        = "Simon Tjell",
  TITLE         = "Formal Requirements Modeling for Reactive Systems
                   with Coloured Petri Nets",
  SCHOOL        = "University of Aarhus",
  ADDRESS       = "Department of Computer Science",
  YEAR          = "2009",
  MONTH         = "January",
  SIZE          = "267",
  ANNOTE        = "",
  COMMENT       = "I have a copy PGL"}

%G VDM VDM++ OML
@TECHREPORT{vanderSpek04a,
  KEY           = "vanderSpek04",
  AUTHOR        = "P. van der Spek",
  TITLE         = "The Overture Project: Towards an open source toolset",
  INSTITUTION        = "Delf University of Technology",
  YEAR          = "2004",
  MONTH         = "January",
  PAGES         = "122",
  NOTE          = "",
  ANNOTE        = "",
  COMMENT       = ""}

%G OML VDM VDM++
@MASTERSTHESIS{vanderSpek04b,
  KEY           = "vanderSpek04",
  AUTHOR        = "P. van der Spek",
  TITLE         = "The Overture Project: Designing an open source tool set",
  SCHOOL        = "Delf University of Technology",
  YEAR          = "2004",
  MONTH         = "August",
  PAGES         = "239",
  NOTE          = "",
  ANNOTE        = "",
  COMMENT       = ""}


%G VDM++
@MISC{VDMTools,
  KEY           = "VDMTools",
  AUTHOR        = "CSK",
  TITLE         = "{VDMTools homepage}",
  YEAR          = "2007",
  MONTH         = "",
  HOWPUBLISHED  = "\textit{http://www.vdmtools.jp/en/}",
  SIZE          = "",
  NOTE          = "",
  ANNOTE        = "",
  COMMENT       = ""}

%G VDMRT VDM VDM++
@ARTICLE{Verhoef05,
  KEY           = "Verhoef05",
  AUTHOR        = "Marcel Verhoef",
  TITLE         = "On the Use of {VDM++} for Specifying Real-Time Systems",
  JOURNAL       = "Proc. First Overture workshop",
  PUBLISHER     = "University of Newcastle-Upon-Tyne, Centre for Software Reliability",
  YEAR          = "2005",
  MONTH         = "November",
  COMMENT       = "I have the proceedings PGL"}

%G VDM VDM++ VDMRT
@INPROCEEDINGS{Verhoef06,
  KEY           = "Verhoef06",
  AUTHOR        = "Marcel Verhoef",
  EDITOR        = "J. S. Fitzgerald and P. G. Larsen and N. Plat",
  TITLE         = "{On the use of VDM++ for Specifying Real-Time Systems}",
  BOOKTITLE     = "{Towards Next Generation Tools for VDM: Contributions to the First International Overture Workshop, Newcastle, July 2005}",
  ADDRESS       = "School of Computing Science, Newcastle University, Technical Report CS-TR-969",
  YEAR          = "2006",
  MONTH         = "June",
  PAGES         = "26--43"
}

%G VDM VDM++ VICE TOOL
@PHDTHESIS{Verhoef08,
  KEY           = "Verhoef08",
  AUTHOR        = "Marcel Verhoef",
  TITLE         = "{Modeling and Validating Distributed Embedded Real-Time
                    Control Systems}",
  SCHOOL        = "Radboud University Nijmegen",
  YEAR          = "2008",
  NUMBER        = "RU. 2009-01",
  NOTE          = "{ISBN 978-90-9023705-3}",
  ANNOTE        = "",
  COMMENT       = "I have a copy PGL"}

%G VDM++ VDM VICE
@TECHREPORT{Verhoef&06,
  KEY           = "Verhoef\&06",
  AUTHOR        = "Marcel Verhoef and Peter Gorm Larsen",
  TITLE         = "{Enhancing VDM++ for Modeling Distributed Embedded Real-time Systems}",
  INSTITUTION   = "Radboud University Nijmegen",
  YEAR          = "2006",
  MONTH         = "March",
  TYPE          = "",
  NUMBER        = "(to appear)",
  SIZE          = "",
  NOTE          = "A preliminary version of this report is available on-line at \textit{http://www.cs.ru.nl/$\sim$marcelv/vdm/}",
  ANNOTE        = "",
  COMMENT       = ""}

%G VDM++ VICE VDM
@INPROCEEDINGS{Verhoef&06b,
  KEY           = "Verhoef\&06",
  AUTHOR        = "Marcel Verhoef and Peter Gorm Larsen and Jozef Hooman",
  EDITOR        = "Jayadev Misra and Tobias Nipkow and Emil Sekerinski",
  TITLE         = "{Modeling and Validating Distributed Embedded
                    Real-Time Systems with VDM++}",
  BOOKTITLE     = "FM 2006: Formal Methods",
  PUBLISHER     = "Lecture Notes in Computer Science 4085",
  YEAR          = "2006",
  PAGES         = "147-162",
  ANNOTE        = "",
  COMMENT       = "I have the sources (PGL)"}

%G VICE VDM VDM++
@INPROCEEDINGS{Verhoef&07,
  KEY           = "Verhoef\&07",
  AUTHOR        = "Marcel Verhoef and Peter Gorm Larsen",
  EDITOR        = "Brian Sauser and Gerrit Muller",
  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)"}

%G VDM VDM++
@INPROCEEDINGS{Verhoef&07b,
  KEY           = "Verhoef\&07",
  AUTHOR        = "Marcel Verhoef and Peter Visser and Jozef Hooman and
                   Jan Broenink",
  TITLE         = "{Co-simulation of Real-time Embedded Control Systems}",
  BOOKTITLE     = "Integrated Formal Methods: Proc. 6th. Intl. Conference",
  EDITOR        = "Jim Davies and Jeremy Gibbons",
  PUBLISHER     = "Springer-Verlag",
  SERIES        = "Lecture Notes in Computer Science 4591",
  PAGES         = "639--658",
  YEAR          = "2007",
  MONTH         = "July",
  ANNOTE        = "",
  COMMENT       = ""}

%G VDM VDM++ PROOF
@MASTERSTHESIS{Vermolen07,
  KEY           = "Vermolen07",
  AUTHOR        = "Sander Vermolen",
  TITLE         = "{Automatically Discharging VDM Proof Obligations using HOL}",
  SCHOOL        = "Radboud University Nijmegen",
  ADDRESS       = "Computer Science Department",
  YEAR          = "2007",
  MONTH         = "August",
  SIZE          = "115",
  ANNOTE        = "",
  COMMENT       = "I have the hard copy PGL"}

%G AFRODITE VDM++
@MANUAL{veri-lov,
  KEY           = "VERILOG",
  AUTHOR        = "VERILOG",
  ORGANIZATION  = "VERILOG",
  TITLE         = "LOV/OMT  Technical Presentation",
  INSTITUTION   = "VERILOG",
  YEAR          = "1995"}

%G AFRODITE VDM++
@MANUAL{veri-oedit-rm,
  KEY           = "VERILOG",
  AUTHOR        = "VERILOG",
  ORGANIZATION  = "VERILOG",
  TITLE         = "LOV/OMT  Object Editor Reference Manual, version 1.2",
  INSTITUTION   = "VERILOG",
  YEAR          = "1995"}

%G AFRODITE VDM++
@MANUAL{veri-oedit-gst,
  KEY           = "VERILOG",
  AUTHOR        = "VERILOG",
  ORGANIZATION  = "VERILOG",
  TITLE         = "LOV/OMT  Object Editor Getting Started, version 1.2",
  INSTITUTION   = "VERILOG",
  YEAR          = 1995}


%G AFRODITE VDM++
@MANUAL{veri-lov-tm,
  KEY           = "VERILOG",
  AUTHOR        = "VERILOG",
  ORGANIZATION  = "VERILOG",
  TITLE         = "Project Organizer Reference Manual, version 1.0",
  INSTITUTION   = "VERILOG",
  YEAR          = "1995"}




%G AFRODITE VDM++
@MANUAL{lovinstall,
  KEY           = "VERILOG93",
  AUTHOR        = "VERILOG",
  ORGANIZATION  = "VERILOG",
  TITLE         = "Installing and Managing VERILOG Products",
  INSTITUTION   = "VERILOG",
  YEAR          = "1993",
  MONTH         = "July",
  NOTE          = "\\ Document reference: D/PUNI/IA/100/327
                   (part of the LOV/OMT distribution)"}

% AFRODITE VDM++ VDM OBJECT
@TECHREPORT{AFROVERILOGPLBUM,
  KEY           = "VERILOG95",
  AUTHOR        = "VERILOG",
  TITLE         = "VENUS; OMT-VDM++ Coupling Module User Manual",
  INSTITUTION   = "VERILOG",
  YEAR          = "1995",
  MONTH         = "August",
  NOTE          = "\\ Afrodite Doc.id : AFRO/VERILOG/PLB/UM/V3.0"}

%G AFRODITE VDM++
@TECHREPORT{AFROIFADPBLAST,
  KEY           = "Voss\&95",
  AUTHOR        = "Henrik Voss, Poul B\o{}gh Lassen \&  Peter Gorm Larsen",
  TITLE         = "Description of the VDM++ Yacc- and Abstract Syntax",
  INSTITUTION   = "IFAD",
  YEAR          = "1995",
  MONTH         = "June",
  NOTE          = "\\ Afrodite Doc.id : AFRO/IFAD/PBL/AST/V13"}

%G VDM OBJECT VDM++
@ARTICLE{vrancken95,
   KEY          = "Vrancken 95",
   AUTHOR       = "Jos Vrancken",
   TITLE        = "{Gedistribueerd real-time systeem is een optelsom
                    van problemen}",
   JOURNAL      = "Automatisering Gids",
   YEAR         = "1995",
   MONTH        = "6 januari",
   PAGES        = "9",
   NOTE         = "(In dutch)",
   COMMENT      = "NP; location:"}

%G VDM TOOL VDM++ OO
@ARTICLE{Weissenbacher01,
  KEY           = "Weissenbacher01",
  AUTHOR        = "Georg Weissenbacher",
  TITLE         = "{VDM++: Lightweight Formal Methods Ohne Beweis}",
  JOURNAL       = "iX",
  YEAR          = "2001",
  MONTH         = "February",
  VOLUME        = "3",
  PAGES         = "157--161",
  NOTE          = "In German",
  ANNOTE        = "",
  COMMENT       = "BIB. PGL"}

%G AFRODITE VDM++ VDM OBJECT
@TECHREPORT{AFROCGAWGD,
  KEY           = "Wijma94",
  AUTHOR        = "Abko Wijma",
  TITLE         = "A Generic Pretty-Printer for VDM++ Specifications",
  INSTITUTION   = "Cap Volmac",
  YEAR          = "1994",
  MONTH         = "June",
  NOTE          = "\\ Afrodite Doc.id : AFRO/CG/AW/GD/V1"}

%G VDM VDM++ APPLY
@MASTERSTHESIS{Wolff08,
  KEY           = "Wolff08",
  AUTHOR        = "Sune Wolff",
  TITLE         = "{Universal Multiprotocol Home Automation Framework}",
  SCHOOL        = "Aarhus University/Engineering College of Aarhus",
  YEAR          = "2008",
  MONTH         = "December",
  SIZE          = "127",
  ANNOTE        = "",
  COMMENT       = "I have a copy PGL"}

%G VDM VDM++ APPLY
@INPROCEEDINGS{Wolff09,
  KEY           = "Wolff09",
  AUTHOR        = "Sune Wolff",
  TITLE         = "{Formalising Concurrent and Distributed Design
                   Patterns with VDM}",
  NOTE          = "The 7th Overture workshop at FM'09",
  YEAR          = "2009",
  MONTH         = "November",
  ANNOTE        = "",
  COMMENT       = "I have the source (PGL)"}

%G VDM VDM++ VICE
@INPROCEEDINGS{Wolff&10,
  KEY           = "Wolff\&10",
  AUTHOR        = "Sune Wolff and Peter Gorm Larsen and Tammy Noergaard",
  TITLE         = "{Development Process for Multi-Disciplinary Embedded
                    Control Systems}",
  BOOKTITLE     = "EuroSim 2010",
  ORGANIZATION  = "EuroSim",
  YEAR          = "2010",
  MONTH         = "September",
  ANNOTE        = "",
  COMMENT       = "BIB I have the sources (PGL)"}

%G FORMAL APPLY VDM VDM++
  @ARTICLE{Woodcock&09,
  KEY           = "Woodcock\&09",
  AUTHOR        = {Woodcock, Jim and Larsen, Peter Gorm and Bicarregui,
                   Juan and Fitzgerald, John},
  TITLE         = "{Formal Methods: Practice and Experience}",
  JOURNAL       = {ACM Computing Surveys},
  VOLUME        = {41},
  NUMBER        = {4},
  YEAR          = {2009},
  MONTH         = {October},
  ISSN          = {0360-0300},
  PAGES         = {1--36},
  DOI           = {http://doi.acm.org/10.1145/1592434.1592436},
  PUBLISHER     = {ACM},
  ADDRESS       = {New York, NY, USA},
  COMMENT       = "PGL I have the sources"}

%G VDM++
@MISC{CskVdmHome,
  KEY           = "CskVdmHome",
  AUTHOR        = "CSK",
  TITLE         = "{VDM} homepage",
  YEAR          = "2005",
  MONTH         = "",
  HOWPUBLISHED  = "\textit{http://www.csk.com/support\_e/vdm/index.html}",
  SIZE          = "",
  NOTE          = "",
  ANNOTE        = "",
  COMMENT       = ""}

@ARTICLE{Tanenbaum&76,
   KEY       = "Tanenbaum\&76",
   AUTHOR    = "A. Tanenbaum",
   TITLE     = "{In Defense of Program Testing or Correctness Proofs Considered Harmful}",
   JOURNAL   = "ACM SIGPLAN Notices",
   MONTH     = "May",
   YEAR      = "1976",
   VOLUME    = "11",
   PAGES     = "64-68",
   ANNOTE    = "{This gives an opinion about how important the test
                 automation is.}"}
@ARTICLE{Petrenko02,
   KEY       = "Petrenko02",
   AUTHOR    = "A.A. Koptelov, V.V. Kuliamin, A.K. Petrenko",
   TITLE     = "{Vdm++ TesK: Testing of VDM++ programs}",
   MONTH     = "July",
   YEAR      = 2002
}
@book{devjavasoft,
  key = "devjavasoft",
  author = "Russel Winder and Graham Roberts",
  title = "{Developing Java Software, 3rd Edition}",
  year = 2006,
  publisher = "John Wiley \& Sons, Inc.",
  address = "New York, NY, USA"
}
@TECHREPORT{VDMToolMan,
  KEY = "VDMToolMan",
  AUTHOR = "CSK Systems Corporation",
  TITLE = "{VDMTools User Manual (VDM++) 1.2}",
  INSTITUTION = "CSK",
  YEAR = "2007",
  URL = "\\ http://www.vdmtools.jp/uploads/manuals/usermanpp_a4E.pdf"
}

@ARTICLE{MuJava,
  KEY="MuJava",
  AUTHOR = "Y.Ma, J.Offutt, Y.Kwon",
  TITLE = " MuJava : An Automated Class Mutation System",
  YEAR = 2005,
  MONTH = "June"
}