@book(DBLP:books/daglib/0015096,
 author       = "Jean-Raymond Abrial",
 year         = "2005",
 title        = "The B-book - assigning programs to meanings",
 publisher    = "Cambridge University Press",
)
@article(AbrialBHHMV10,
 author       = "Jean-Raymond Abrial and Michael Butler and Stefan Hallerstede and Thai Son Hoang and Farhad Mehta and Laurent Voisin",
 year         = "2010",
 title        = "Rodin: an open toolset for modelling and reasoning in {Event-B}",
 journal      = "STTT",
 volume       = "12",
 number       = "6",
 pages        = "447--466",
 url          = "http://dx.doi.org/10.1007/s10009-010-0145-y",
)
@inproceedings(DBLP:conf/cav/BarrettCDHJKRT11,
 author       = "Clark Barrett and Christopher L. Conway and Morgan Deters and Liana Hadarean and Dejan Jovanovic and Tim King and Andrew Reynolds and Cesare Tinelli",
 year         = "2011",
 title        = "CVC4",
 booktitle    = "CAV",
 pages        = "171--177",
 url          = "http://dx.doi.org/10.1007/978-3-642-22110-1_14",
)
@article(DBLP:journals/tsi/BendispostoLLS08,
 author       = "Jens Bendisposto and Michael Leuschel and O. Ligot and Mireille Samia",
 year         = "2008",
 title        = "La validation de mod{\`e}les Event-B avec le plug-in ProB pour RODIN",
 journal      = "Technique et Science Informatiques",
 volume       = "27",
 number       = "8",
 pages        = "1065--1084",
 url          = "http://dx.doi.org/10.3166/tsi.27.1065-1084",
)
@manual(AtelierB,
 organization = "ClearSy System Engineering",
 address      = "Aix-en-Provence",
 title        = "Atelier B - User Manual",
 url          = "http://www.atelierb.eu/manuels/manuel-utilisateur-atelier-b-4.0-en.pdf",
)
@inproceedings(DBLP:conf/asm/DeharbeFGV12,
 author       = "David D{\'e}harbe and Pascal Fontaine and Yoann Guyot and Laurent Voisin",
 year         = "2012",
 title        = "SMT Solvers for Rodin",
 booktitle    = "ABZ",
 pages        = "194--207",
 url          = "http://dx.doi.org/10.1007/978-3-642-30885-7_14",
)
@misc(ProB_Manual,
 author       = "Michael Leuschel",
 year         = "2011",
 title        = "User Manual",
 url          = "http://www.stups.uni-duesseldorf.de/ProB/index.php5/User\_Manual",
)
@inproceedings(DBLP:dblp_conf/fm/LeuschelB03,
 author       = "Michael Leuschel and Michael J. Butler",
 year         = "2003",
 title        = "ProB: A Model Checker for B.",
 booktitle    = "FME",
 pages        = "855--874",
 url          = "http://dx.doi.org/10.1007/978-3-540-45236-2_46",
)
@article(LiBeLe07_219,
 author       = "Olivier Ligot and Jens Bendisposto and Michael Leuschel",
 year         = "2007",
 title        = "Debugging Event-B Models using the ProB Disprover Plug-in",
 journal      = "Proceedings AFADL'07",
)
@inproceedings(Valerio_SBMF2012,
 author       = "Val\'{e}rio G. Medeiros{\ }Jr. and David D\'{e}harbe",
 year         = "2012",
 title        = "{E}xperience in {M}odeling a {M}icrocontroller {I}nstruction {S}et {U}sing {B}",
 booktitle    = "Brazilian Symposium on Formal Methods",
 organization = "SBMF",
 address      = "Natal - RN",
)
@inproceedings(DBLP:conf/tacas/MouraB08,
 author       = "Leonardo Mendon\c {c}a de Moura and Nikolaj Bj{\o }rner",
 year         = "2008",
 title        = "Z3: An Efficient SMT Solver",
 booktitle    = "TACAS",
 pages        = "337--340",
 url          = "http://dx.doi.org/10.1007/978-3-540-78800-3_24",
)
@inproceedings(DBLP:conf/fm/PlaggeL12,
 author       = "Daniel Plagge and Michael Leuschel",
 year         = "2012",
 title        = "Validating B, Z and TLA + Using ProB and Kodkod",
 booktitle    = "FM",
 pages        = "372--386",
 url          = "http://dx.doi.org/10.1007/978-3-642-32759-9_31",
)