%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 =        sep,
  pages =        "139--141",
  comment =      "PGL",
}

%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 =        sep,
  pages =        "85--93",
  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",
  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 =        jun,
  pages =        "352--353",
  note =         "{Also Technical Report CS-TR-1027, School of Computing
                 Science, Newcastle University.}",
}

%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 =        jun,
  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 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 =        sep,
  size =         "38",
  comment =      "BIB. KDB",
}

COMMENT      = "NP has a copy PGL"}

% IDERSINT AFRODITE
}

@TechReport{AFROCGTA,
  key =          "Durr93",
  author =       "Eugene Durr",
  title =        "Afrodite Project, Technical Annex",
  institution =  "Cap Volmac",
  year =         "1993",
}

%G VDM++ VDM OBJECT
}

@PhdThesis{Durr94,
  key =          "D{{\"}}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,
  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",
  comment =      "BIB. PGM",
}

%G VDM OBJECT VDM++
}

@InProceedings{Durr&92b,
  key =          "D{{\"}}rr\&92",
  author =       "E. H. D{\"u}rr and J. van Katwijk",
  editor =       "Bertrand Meyer {Georg Heeg, Boris Magnusson}",
  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",
  comment =      "NP has a copy PGL",
}

%G VDM OBJECT VDM++
}

@InProceedings{Durr&92c,
  key =          "D{{\"}}rr\&92",
  author =       "J. van Katwijk {E.H. D{\"u}rr, W. Lourens}",
  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 =        jan,
  year =         "1992",
  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 =        jul,
  size =         "65",
  comment =      "PBL has a hard-copy",
}

%G VDM++ VDM OBJECT
}

@InProceedings{Durr&93c,
  key =          "D{{\"}}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",
  comment =      "NP has a copy",
}

%G VDM++ VDM OBJECT
}

@Misc{Durr&94,
  key =          "D{{\"}}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,
  comment =      "NA PGL",
}

%G VDM++ VDM OBJECT RAIL
}

@InBook{Durr&95,
  key =          "D{{\"}}rr\&95",
  author =       "Nico Plat Eug\`{e}ne D{\"u}rr 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",
  comment =      "I have the book PGL",
}

%G VDM++ VDM OBJECT
}

@Misc{Durr&95b,
  key =          "D{{\"}}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 =        jun,
  comment =      "NKK",
}

%G VDM VDM++ OBJECT REAL-TIME
}

@InBook{Durr&96,
  key =          "D{{\"}}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",
  comment =      "LIB PGL",
}

%G AFRODITE VDM++ VDM OBJECT
}

@TechReport{AFROCGEDLRM,
  key =          "D{{\"}}rr\&95",
  author =       "E. H. D{\"u}rr and N. Plat (editor)",
  title =        "{VDM++ Language Reference Manual}",
  institution =  "Cap Volmac",
  year =         "1995",
  month =        aug,
  type =         "Afrodite (ESPRIT-III project number 6500) document",
  note =         "Outdated by \cite{LangManPP}",
  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 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 =        apr,
  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 =        apr,
  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 =        nov,
  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",
}

%G VDM++ VDM OBJECT
}

@InProceedings{Goldsack&95,
  key =          "Goldsack\&95",
  author =       "Eugene D{\"u}rr Stephen J.\ Goldsack 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 " # apr,
  pages =        "194--201",
  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 =        apr,
  volume =       "31",
  number =       "4",
  pages =        "32--38",
  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",
  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 =        sep,
  pages =        "13--27",
  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 =        jan,
  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 =        jan,
  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 =        jan,
  URL =          "http://www.vdmtools.jp/en/",
  comment =      "ABMN",
}

%G VDM OBJECT VDM++
}

@InProceedings{Katwijk&97,
  key =          "Katwijk\&97",
  author =       "E. {van Katwijk, J. D{\"u}rr} and S. Goldsack",
  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 =        nov,
  pages =        "17--26",
  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 =        apr,
  number =       "19",
  pages =        "22--25",
  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 =        jun,
  pages =        "73--80",
  note =         "(in Japanese)",
  ISBN =         "ISBN 4-916227-18-2",
}

%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",
  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 =       "S. Goldsack K. Lano",
  editor =       "I. Mackie C. Hankin",
  title =        "Refinement, Subtyping and Subclassing in {VDM}++",
  booktitle =    "2nd Theory and Formal Methods Workshop, Cambridge",
  publisher =    "IC Press",
  year =         "1995",
  comment =      "ABMN",
}

%G VDM OBJECT VDM++ VDMRT
}

@InProceedings{Lano95a,
  key =          "Lano95",
  author =       "K. Lano",
  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",
  comment =      "ABMN",
}

%G VDM OBJECT VDM++
}

@InProceedings{Lano&95a,
  key =          "Lano\&95",
  author =       "S. Goldsack K. Lano",
  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",
  comment =      "BIB ABMN",
}

%G VDM OBJECT VDM++
}

@InProceedings{Lano&95b,
  key =          "Lano\&95",
  author =       "S. Goldsack K. Lano",
  title =        "Specifying Discrete Event Systems in {VDM}++",
  booktitle =    "International Workshop on Analysis and Design of
                 Event-Drive n Operations in Process Systems, London",
  year =         "1995",
  month =        apr,
  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 =        mar,
  comment =      "ABMN",
}

%G VDM++ VDM OBJECT
}

@InProceedings{Lano&96,
  key =          "Lano\&96",
  author =       "K. Lano and S. Goldsack",
  title =        "Object-oriented Formal Development",
  booktitle =    "TOOLS Europe'96",
  year =         "1996",
  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",
  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''",
  publisher =    "Chapman and Hall",
  year =         "1996",
  comment =      "ABMN",
}

%G VDM VDM++ OBJECT
}

@InProceedings{Lano&96c,
  key =          "Lano\&96",
  author =       "Juan Bicarregui Kevin Lano and Stephen Goldsack",
  title =        "Formaling Design Patterns",
  booktitle =    "Northern Formal Methods Workshop",
  publisher =    "Springer-Verlag",
  year =         "1996",
  month =        sep,
  size =         "20",
  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 =        sep,
  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 =        sep,
  note =         "ISBN 3-540-63533-5",
  pages =        "298--317",
}

%G VDM++ VDMRT
}

@InProceedings{Lano&97c,
  key =          "Lano\&97",
  author =       "Kevin Lano and Stephen Goldsack and Juan Bicarregui
                 and Stuart Kent",
  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",
  pages =        "188--219",
  note =         "ISBN:3-540-62717-0",
  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 =        feb,
  volume =       "DOI 10.1007/s00165-008-0068-5",
  comment =      "BIB PGL",
}

%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 =        oct,
  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",
}

%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 =        dec,
  pages =        "81--88",
  comment =      "BIB PGL",
}

%G VDM VDM++
}

@Misc{Overture07,
  key =          "Overture07",
  author =       "Overture-Core-Team",
  title =        "{Overture Web site}",
  year =         "2007",
  howpublished = "http://www.overturetool.org",
}

%G VDM VDM++
}

@InProceedings{Paiva&03,
  key =          "Paiva\&03",
  author =       "Raul Moreira Vidal {Ana Cristina Paiva, Joćo Pascoal
                 Faria}",
  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 =        jul,
  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 =        jun,
  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 =        sep,
  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,
  comment =      "BIB PGL",
}

%G VDM++
}

@Misc{VDMTools,
  key =          "VDMTools",
  author =       "CSK",
  title =        "{VDMTools homepage}",
  year =         "2007",
  howpublished = "\textit{http://www.vdmtools.jp/en/}",
}

%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 =        nov,
  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 =        jun,
  pages =        "26--43",
}

%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 =        mar,
  number =       "(to appear)",
  note =         "A preliminary version of this report is available
                 on-line at
                 \textit{http://www.cs.ru.nl/$\sim$marcelv/vdm/}",
}

%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",
  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",
  year =         "2007",
  month =        mar,
  note =         "{Available at
                 http://www.stevens.edu/engineering/cser/}",
  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 =        jul,
}

%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 =        aug,
  size =         "115",
  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 =        jul,
  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 =        aug,
  note =         "\\ Afrodite Doc.id : AFRO/VERILOG/PLB/UM/V3.0",
}

%G AFRODITE VDM++
}

@TechReport{AFROIFADPBLAST,
  key =          "Voss\&95",
  author =       "Poul B\o{}gh Lassen \& Peter Gorm Larsen {Henrik
                 Voss}",
  title =        "Description of the {VDM}++ Yacc- and Abstract Syntax",
  institution =  "IFAD",
  year =         "1995",
  month =        jun,
  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 =        feb,
  volume =       "3",
  pages =        "157--161",
  note =         "In German",
  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 =        jun,
  note =         "\\ Afrodite Doc.id : AFRO/CG/AW/GD/V1",
}

%G VDM++
}

@Misc{CskVdmHome,
  key =          "CskVdmHome",
  author =       "CSK",
  title =        "{VDM} homepage",
  year =         "2005",
  howpublished = "\textit{http://www.csk.com/support\_e/vdm/index.html}",
}
