myLibrary.bib

@Article{ IEEEexample:blackboard_systems,
	author = "J.W. McManus and W.L. Bynum",
	title = "Design and analysis techniques for concurrent blackboard systems",
	journal = "Systems, Man and Cybernetics",
	volume = "26",
	month = Nov,
	year = "1996",
	pages = "669--680"
}

@Article{ IEEEexample:articledualmonths,
	author = "Y. Okada and K. Dejima and T. Ohishi",
	title = "Analysis and Comparison of {PM} Synchronous Motor and Induction Motor Type Magnetic Bearings",
	journal = IEEE_J_IA,
	volume = "31",
	month = sep # "/" # oct,
	year = "1995",
	pages = "1047--1053"
}

@Electronic{ LHCb,
	title = "Large {H}adron {C}ollider beauty experiment",
	url = "http://lhcb-public.web.cern.ch/lhcb-public"
}

@Article{ ProcessesWithData,
	title = "Model-checking processes with data",
	author = "J.F. Groote and T.A.C. Willemse",
	journal = "Science of Computer Programming",
	year = "2005",
	number = "3",
	volume = "56",
	pages = "251--273"
}

@InProceedings{ DIRAC_CommGridSolution,
	title = "{DIRAC}: A Community Grid Solution",
	publisher = "IOP Publishing",
	author = "A. Tsaregorodtsev and M. Bargiotti and N. Brook and A. Ramo Casajus and G. Castellani and Ph. Charpentier and C. Cioffi and J. Closier and R. Graciani Diaz and G. Kuznetsov and Y. Y Li and R. Nandakumar and R. Paterson and A.C. Smith and M. Seco Miguelez and S. Gomez Jimenez",
	volume = "119",
	number = "2",
	booktitle = "Proc. Computing in High Energy Physics ({CHEP} 2007)"
}

@InProceedings{ DIRAC_ReliableDataMaangement,
	title = "{DIRAC}: Reliable Data Management for {LHC}b",
	publisher = "IOP Publishing",
	author = "A.C. Smith and A. Tsaregorodtsev",
	volume = "119",
	number = "2",
	booktitle = "Proc. Computing in High Energy Physics ({CHEP} 2007)"
}

@Misc{ FormalLanguagemCRL2,
	title = "The formal specification language m{CRL}2",
	booktitle = "In Proceedings of the Dagstuhl Seminar",
	author = "J.F. Groote and A. Mathijssen and M. Reniers and Y. Usenko and M. Van Weerdenburg",
	year = "2007"
}

@TechReport{ mCRL2Toolset,
	title = "The m{CRL}2 toolset",
	author = "J.F. Groote and others",
	institution = "Eindhoven University of Technology",
	location = "Dept. of Mathematics and Computer Science",
	year = "2008"
}

@Book{ process_algebra,
	author = "T. Basten and J.C.M Baeten and M.A. Reniers",
	title = "Process Algebra: Equational Theories of Communicating Processes",
	publisher = "Cambridge University Press",
	address = "NY, USA",
	year = "2009"
}

@InProceedings{ SPIN_case_study,
	title = "Verifying protocols by model checking: a case study of the wireless application protocol and the model checker {SPIN}",
	publisher = "IBM Press",
	author = "Y.T. He and R. Janicki",
	booktitle = "Proc. CASCON 2004"
}

@TechReport{ sessionMgmtMasterThesis,
	title = "Verification of the session management protocol",
	author = "K. Palmskog",
	institution = "Royal Institute of Technology",
	type = "Master’s Thesis",
	department = "School of Computer Science and Communication",
	year = "2006"
}

@Book{ desing_validation_protocols,
	author = "G.J. Holzmann",
	title = "Design and validation of computer protocols",
	publisher = "Prentice-Hall Inc.",
	address = "Upper Saddle River, NJ, USA",
	year = "1990"
}

@Book{ protocol_verification_muCRL,
	author = "W. Fokkink",
	title = "Modelling Distributed Systems: Protocol Verification with $\mu${CRL}",
	publisher = "Springer",
	edition = "2",
	year = "2011"
}

@InProceedings{ SLAMToolkit,
	title = "The {SLAM} Toolkit",
	pages = "260--264",
	publisher = "Springer-Verlag",
	author = "T. Ball and S.K. Rajamani",
	booktitle = "Proc. Computer Aided Verification ({CAV} 2001) "
}

@Article{ SlidingWindowProtocol,
	title = "Verification of a sliding window protocol in $\mu${CRL} and {PVS}",
	author = "B. Badban and W. Fokkink and J.F. Groote and J. Pang and J. Vande Pol",
	journal = "Formal Aspects of Computing",
	year = "2005",
	month = "October",
	number = "3",
	volume = "17"
}

@Article{ DHCP_SPIN,
	title = "Modeling and Formal Verification of {DHCP} Using {SPIN}",
	author = "S.M.S. Islam and M.H. Sqalli and S. Khan",
	journal = "IJCSA",
	year = "2006",
	month = "May"
}

@Misc{ CMS_LHC,
	title = "Analysing the Control Software of the {C}ompact {M}uon {S}olenoid Experiment at the {L}arge {H}adron {C}ollider",
	publisher = "Springer-Verlag",
	author = "J.L. Hwon and  and V.J.J. Kuster and T.A.C. Willemse",
	booktitle = "FSEN 2011",
	note = "in press"
}

@Article{ Linux_driver,
	title = "Behavioural Analysis of an {I2C} Linux Driver",
	publisher = "Springer-Verlag",
	author = "D. Bo\v{s}na\v{c}ki and A. Mathijssen and Y.S. Usenko",
	journal = "Proc. FMICS 2009"
}

@Article{ SystemC_processAlgebra,
	title = "Formal Analysis of {S}ystem{C} Designs in Process Algebra",
	publisher = "IOS Press",
	author = "H. Hojjat and M.R. Mousavi and M. Sirjani",
	journal = "Fundamenta Informaticae",
	year = "2011",
	pages = "19--42"
}

@InProceedings{ Java_PathFinder,
	title = "Model Checking Programs with {J}ava {PathFinder}",
	author = "V. Visser and P.C. Mehlitz",
	booktitle = "Proc. SPIN (2005)"
}

@TechReport{ ACS_mCRL2,
	title = "Analysis of {ACS} using m{CRL}2",
	author = "B. Ploeger",
	institution = "Technische Universiteit Eindhoven",
	type = "CS-Report 09-11",
	year = "2009"
}

@InProceedings{ DISET,
	title = "{DIRAC} distributed secure framework",
	publisher = "IOP Publishing",
	author = "A. Casajus and R. Graciani Diaz",
	booktitle = "Proc. Computing in High Energy Physics ({CHEP} 2010)"
}

@Electronic{ gLite,
	title = "gLite - {L}ightweight {M}iddleware for {G}rid {C}omputing",
	url = "http://glite.cern.ch"
}

@InProceedings{ DIRAC_pilot_WMS,
	title = "{DIRAC} Pilot Framework and the {DIRAC} {W}orkload {M}anagement {S}ystem",
	publisher = "IOP Publishing",
	author = "A. Casajus and R. Graciani Diaz and S. Paterson and A. Tsaregorodtsev",
	booktitle = "Proc. Computing in High Energy Physics ({CHEP} 2010)"
}

@Electronic{ ProductionShifterGuide,
	title = "Grid Production Shifter Guide for {LHC}b",
	url = "https://twiki.cern.ch/twiki/bin/view/LHCb/ProductionShifterGuide"
}

@Article{ DBLP:journals/computer/Parnas10,
	author = "D.L. Parnas",
	title = "Really Rethinking 'Formal Methods'",
	journal = "IEEE Computer",
	volume = "43",
	number = "1",
	year = "2010",
	pages = "28--34",
	ee = "http://doi.ieeecomputersociety.org/10.1109/MC.2010.22",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

@InProceedings{ Musuvathi04modelchecking,
	author = "M. Musuvathi and D.R. Engler",
	title = "Model Checking Large Network Protocol Implementations",
	booktitle = "In Proceedings of the First Symposium on Networked Systems Design and Implementation",
	year = "2004",
	pages = "155--168"
}

@InProceedings{ Hatcliff99slicingsoftware,
	author = "John Hatcliff and Matthew B. Dwyer and Hongjun Zheng",
	title = "Slicing Software for Model Construction",
	booktitle = "Higher-order and Symbolic Computation",
	year = "1999",
	pages = "105--118"
}

@Misc{ Groote_specificationguidelines,
	author = "J. F. Groote and T. W. D. M. Kouters and A. A. H. Osaiweran",
	title = "Specification Guidelines to avoid the State Space Explosion Problem",
	year = ""
}

@InProceedings{ Pelánek08fightingstate,
	author = "Radek Pel{\'a}nek",
	title = "Fighting state space explosion: Review and evaluation",
	booktitle = "In Proc. of Formal Methods for Industrial Critical Systems (FMICS’08",
	year = "2008"
}

@Electronic{ svn_mcrl2,
	title = "m{CRL2} {SVN} Repository",
	url = "https://svn.win.tue.nl/viewvc/MCRL2/trunk/examples/"
}

@Electronic{ frama_c,
	title = "Frama-C software suite",
	url = "http://frama-c.com"
}

@Electronic{ codeSurfer,
	title = "CodeSurfer",
	url = "http://www.grammatech.com/products/codesurfer"
}

@InProceedings{ Corbett00bandera,
	author = "James C. Corbett and Matthew B. Dwyer and John Hatcliff and Shawn Laubach and Corina S. Pasareanu and Hongjun Zheng",
	title = "Bandera: Extracting Finite-state Models from Java Source Code",
	booktitle = "Proc. 22nd International Conference on Software Engineering",
	year = "2000",
	pages = "439--448",
	publisher = "ACM Press"
}

@Electronic{ DiaGraphica,
	title = "DiaGraphica",
	url = "http://www.comp.leeds.ac.uk/scsajp/applications/diagraphica"
}

@TechReport{ LTSmin,
	title = "{LTS}min : Distributed and Symbolic Reachability",
	author = "S. Blom and J. Van de Pol and M. Weber",
	institution = "Formal Methods and Tools, University of Twente, The Netherlands"
}

@Electronic{ DAS4,
	title = "The {D}istributed {ASCI} {S}upercomputer 4",
	url = "http://www.cs.vu.nl/das4/"
}