@techreport(Barrett01,
 author       = "Clark Barrett and Aaron Stump and Cesare Tinelli",
 year         = "2010",
 title        = "{The SMT-LIB Standard: Version 2.0}",
 type         = "Technical Report",
 institution  = "Department of Computer Science, The University of Iowa",
 note         = "Available at {\tt www.SMT-LIB.org}",
)
@inproceedings(Barrett00,
 author       = "Clark Barrett and Cesare Tinelli",
 year         = "2007",
 title        = "{CVC3}",
 editor       = "Werner Damm and Holger Hermanns",
 booktitle    = "Proceedings of the $19^{th}$ International Conference on Computer Aided Verification (CAV '07)",
 series       = "Lecture Notes in Computer Science",
 volume       = "4590",
 publisher    = "Springer-Verlag",
 pages        = "298--302",
 note         = "Berlin, Germany",
)
@proceedings(DBLP:conf/icfem/2009,
 editor       = "Karin Breitman and Ana Cavalcanti",
 year         = "2009",
 title        = "Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil, December 9-12, 2009. Proceedings",
 series       = "Lecture Notes in Computer Science",
 volume       = "5885",
 publisher    = "Springer",
 url          = "http://dx.doi.org/10.1007/978-3-642-10373-5",
)
@manual(Cok00,
 author       = "David R. Cok",
 year         = "2011",
 title        = "The {SMT-LIB}v2 Language and Tools: A Tutorial",
 organization = "GrammaTech, Inc.",
)
@(altergo,
 author       = "Sylvain Conchon and Evelyne Contejean",
 title        = "Alt-{E}rgo",
 url          = "http://alt-ergo.lri.fr",
 note         = "Last access: November 2011",
)
@manual(CoqRM,
 author       = "{Coq Development Team}",
 year         = "2008",
 title        = "The {Coq} Proof Assistant Reference Manual, Version 8.2",
 organization = "LogiCal Project",
)
@inproceedings(CristiaSEW2011,
 author       = "Maximiliano Cristi\'{a} and Pablo Albertengo and Claudia Frydman and Brian Pl\"uss and Pablo Rodr\'{\i }guez Monetti",
 year         = "2011",
 title        = "Applying the {T}est {T}emplate {F}ramework to Aerospace Software",
 booktitle    = "Proceedings of the 34th IEEE Annual Software Engineering Workshop",
 publisher    = "IEEE Computer Society",
 address      = "Limerik, Irland",
 note         = "--- to be published",
)
@inproceedings(CristiaARM,
 author       = "Maximiliano Cristi\'a and Pablo Albertengo and Pablo {Rodr\'{\i }guez Monetti}",
 year         = "2010",
 title        = "Pruning Testing Trees in the {T}est {T}emplate {F}ramework by Detecting Mathematical Contradictions",
 editor       = "Jos\'e Luis Fiadeiro and Stefania Gnesi",
 booktitle    = "SEFM",
 publisher    = "IEEE Computer Society",
 pages        = "268--277",
)
@inproceedings(CristiaFTCRL,
 author       = "Maximiliano Cristi{\'a} and Diego Hollmann and Pablo Albertengo and Claudia S. Frydman and Pablo Rodr\'{\i }guez Monetti",
 year         = "2011",
 title        = "A Language for Test Case Refinement in the {T}est {T}emplate {F}ramework",
 editor       = "Shengchao Qin and Zongyan Qiu",
 booktitle    = "ICFEM",
 series       = "Lecture Notes in Computer Science",
 volume       = "6991",
 publisher    = "Springer",
 pages        = "601--616",
 url          = "http://dx.doi.org/10.1007/978-3-642-24559-6_40",
)
@inproceedings(CristiaPluss,
 author       = "Maximiliano Cristi{\'a} and Brian Pl{\"u}ss",
 year         = "2010",
 title        = "Generating Natural Language Descriptions of {Z} Test Cases",
 editor       = "John D. Kelleher and Brian Mac Namee and Ielka van der Sluis and Anja Belz and Albert Gatt and Alexander Koller",
 booktitle    = "INLG",
 publisher    = "The Association for Computer Linguistics",
 pages        = "173--177",
 url          = "http://www.aclweb.org/anthology/W10-4218",
)
@inproceedings(CristiaPRM,
 author       = "Maximiliano Cristi{\'a} and Pablo {Rodr\'{\i }guez Monetti}",
 year         = "2009",
 title        = "Implementing and Applying the {Stocks-Carrington} Framework for Model-Based Testing",
 editor       = "Breitman and Cavalcanti",
 pages        = "167--185",
 url          = "http://dx.doi.org/10.1007/978-3-642-10373-5_9",
)
@inproceedings(CSV,
 author       = "Maximiliano Cristi\'a and Valdivino Santiago and N.L. Vijaykumar",
 year         = "2010",
 title        = "On Comparing and Complementing two {MBT} approaches",
 editor       = "Fabi\'an Vargas and Erika Cota",
 booktitle    = "LATW",
 publisher    = "IEEE Computer Society",
 pages        = "1--6",
)
@(veriT,
 author       = "David D\'eharbe and Pascal Fontaine",
 title        = "The veri{T} Solver",
 url          = "http://www.verit-solver.org",
 note         = "Last access: November 2011",
)
@inproceedings(Dutertre00,
 author       = "Bruno Dutertre and Leonardo de Moura",
 year         = "2006",
 title        = "System Description: {Y}ices 1.0",
 booktitle    = "Proceedings of the 2nd SMT competition, SMT-COMP'06",
 address      = "Seattle, USA",
)
@(CZT,
 author       = "Leo Freitas and Mark Utting and Petra Malik and Tim Miller",
 title        = "Community {Z} {T}ools ({CZT}) Project",
 url          = "http://czt.sourceforge.net",
 note         = "Last access: November 2011",
)
@inproceedings(Galler00,
 author       = "Stefan J. Galler and Bernhard Peischl and Franz Wotawa",
 year         = "2008",
 title        = "Challenging Automatic Test Case Generation Tools with Real World Applications",
 booktitle    = "Proceedings of the IASTED International Conference on Software Engineering and Applications",
 pages        = "21--26",
)
@(SAGE,
 author       = "Patrice Godefroid",
 title        = "SAGE",
 url          = "http://channel9.msdn.com/blogs/peli/automated-whitebox-fuzz-testing-with-sage",
 note         = "Last access: November 2011",
)
@inproceedings(Grieskamp02,
 author       = "Wolfgang Grieskamp and Xiao Qu and Xiangjun Wei and Nicolas Kicillof and Myra B. Cohen",
 year         = "2009",
 title        = "Interaction Coverage Meets Path Coverage by SMT Constraint Solving",
 booktitle    = "Proceedings of the 21st IFIP WG 6.1 International Conference on Testing of Software and Communication Systems and 9th International FATES Workshop",
 series       = "TESTCOM '09/FATES '09",
 publisher    = "Springer-Verlag",
 address      = "Berlin, Heidelberg",
 pages        = "97--112",
 url          = "http://dx.doi.org/10.1007/978-3-642-05031-2\unhbox \voidb@x \kern 0.06em\vbox {\hrule width0.5em}7",
)
@techreport(ZISO,
 author       = "{ISO}",
 year         = "2002",
 title        = "Information {T}echnology -- {Z} {F}ormal {S}pecification {N}otation -- {S}yntax, {T}ype {S}ystem and {S}emantics",
 type         = "Technical Report",
 number       = "ISO/IEC 13568",
 institution  = "International Organization for Standardization",
)
@book(Jackson00,
 author       = "Daniel Jackson",
 year         = "2006",
 title        = "Software Abstractions: Logic, Language, and Analysis",
 publisher    = "The MIT Press",
)
@book(Jacky,
 author       = "Jonathan Jacky",
 year         = "1996",
 title        = "The way of Z: practical programming with formal methods",
 publisher    = "Cambridge University Press",
 address      = "New York, NY, USA",
)
@inproceedings(Kroning00,
 author       = "Daniel Kr{\"o}ning and Philipp R{\"u}mmer and Georg Weissenbacher",
 year         = "2009",
 title        = "A Proposal for a Theory of Finite Sets, Lists, and Maps for the SMT-Lib Standard",
 booktitle    = "Informal proceedings, 7th International Workshop on Satisfiability Modulo Theories at CADE 22",
)
@inproceedings(Malik00,
 author       = "Petra Malik and Mark Utting",
 year         = "2005",
 title        = "{CZT}: A Framework for {Z} Tools",
 editor       = "Helen Treharne and Steve King and Martin C. Henson and Steve A. Schneider",
 booktitle    = "ZB",
 series       = "Lecture Notes in Computer Science",
 volume       = "3455",
 publisher    = "Springer",
 pages        = "65--84",
 url          = "http://dx.doi.org/10.1007/11415787_5",
)
@inproceedings(Bjorner00,
 author       = "Leonardo Mendon\c {c}a de Moura and Nikolaj Bj{\o }rner",
 year         = "2008",
 title        = "Z3: An Efficient SMT Solver",
 editor       = "C. R. Ramakrishnan and Jakob Rehof",
 booktitle    = "TACAS",
 series       = "Lecture Notes in Computer Science",
 volume       = "4963",
 publisher    = "Springer",
 pages        = "337--340",
 url          = "http://dx.doi.org/10.1007/978-3-540-78800-3_24",
)
@article(Nieuwenhuis00,
 author       = "Robert Nieuwenhuis and Albert Oliveras and Cesare Tinelli",
 year         = "2006",
 title        = "Solving {SAT} and {SAT} Modulo Theories: From an abstract {Davis}--{Putnam}--{Logemann}--{Loveland} procedure to {DPLL(T)}",
 journal      = "J. ACM",
 volume       = "53",
 pages        = "937--977",
 url          = "http://doi.acm.org/10.1145/1217856.1217859",
)
@inproceedings(Peleska01,
 author       = "Jan Peleska and Elena Vorobev and Florian Lapschies",
 year         = "2011",
 title        = "Automated test case generation with SMT-solving and abstract interpretation",
 booktitle    = "Proceedings of the Third international conference on NASA Formal methods",
 series       = "NFM'11",
 publisher    = "Springer-Verlag",
 address      = "Berlin, Heidelberg",
 pages        = "298--312",
 url          = "http://dl.acm.org/citation.cfm?id=1986308.1986333",
)
@book(Potter,
 author       = "B. Potter and D. Till and J. Sinclair",
 year         = "1996",
 title        = "An introduction to formal specification and Z",
 publisher    = "Prentice Hall PTR Upper Saddle River, NJ, USA",
)
@inproceedings(ZEVES,
 author       = "Mark Saaltink",
 year         = "1997",
 title        = "The {Z/EVES} {S}ystem",
 editor       = "J.P. Bowen and M.G. Hinchey and D. Till",
 booktitle    = "{ZUM} '97: {T}he {Z} {F}ormal {S}pecification {N}otation",
 pages        = "72--85",
)
@book(Spivey00,
 author       = "J. M. Spivey",
 year         = "1992",
 title        = "The Z notation: a reference manual",
 publisher    = "Prentice Hall International (UK) Ltd.",
 address      = "Hertfordshire, UK, UK",
)
@article(Stocks2,
 author       = "P. Stocks and D. Carrington",
 year         = "1996",
 title        = "A {F}ramework for {S}pecification-{B}ased {T}esting",
 journal      = "IEEE Transactions on Software Engineering",
 volume       = "22",
 number       = "11",
 pages        = "777--793",
)
@(Pex,
 author       = "{The Pex Team}",
 title        = "Pex",
 url          = "http://research.microsoft.com/en-us/projects/pex/",
 note         = "Last access: November 2011",
)
@inproceedings(Veanes01,
 author       = "Margus Veanes and Pavel Grigorenko and Peli de Halleux and Nikolai Tillmann",
 year         = "2009",
 title        = "Symbolic Query Exploration",
 editor       = "Breitman and Cavalcanti",
 pages        = "49--68",
 url          = "http://dx.doi.org/10.1007/978-3-642-10373-5_3",
)