/branches/compiler/cSharp/ooasCompiler/doc/papers.bib - OoasTools - MoMuT Open Source Repository

root / branches / compiler / cSharp / ooasCompiler / doc / papers.bib @ 3

       % This file was created with JabRef 2.5.
       % Encoding: UTF-8
       @INPROCEEDINGS{Aichernig2009b,
         author = {Bernhard K. Aichernig and Harald Brandl and Elisabeth J{\"o}bstl
       	and Willibald Krenn},
         title = {Model-Based Mutation Testing of Hybrid Systems},
         booktitle = {FMCO},
         year = {2009},
         pages = {228-249},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://dx.doi.org/10.1007/978-3-642-17071-3_12}
+      }
       @INPROCEEDINGS{Alfaro2003,
         author = {Luca de Alfaro},
         title = {Game Models for Open Systems},
         booktitle = {Verification: Theory and Practice},
         year = {2003},
         pages = {269-289},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/birthday/2003manna},
         ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2772{\&}spage=269},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Alur1998,
         author = {Rajeev Alur and Thomas A. Henzinger and Orna Kupferman and Moshe
       	Y. Vardi},
         title = {Alternating Refinement Relations},
         booktitle = {CONCUR},
         year = {1998},
         pages = {163-178},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/concur/1998},
         ee = {http://link.springer.de/link/service/series/0558/bibs/1466/14660163.htm},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Bacherini2006,
         author = {Stefano Bacherini and Alessandro Fantechi and Matteo Tempestini and
       	Niccol{\`o} Zingoni},
         title = {A Story About Formal Methods Adoption by a Railway Signaling Manufacturer},
         booktitle = {FM},
         year = {2006},
         pages = {179-189},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/fm/2006},
         ee = {http://dx.doi.org/10.1007/11813040_13},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Baker2002,
         author = {Paul Baker and Paul Bristow and Clive Jervis and David J. King and
       	Bill Mitchell},
         title = {Automatic Generation of Conformance Tests from Message Sequence Charts},
         booktitle = {SAM},
         year = {2002},
         pages = {170-198},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/sam/2002},
         ee = {http://link.springer.de/link/service/series/0558/bibs/2599/25990170.htm},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Ball2006,
         author = {Thomas Ball and Ella Bounimova and Byron Cook and Vladimir Levin
       	and Jakob Lichtenberg and Con McGarvey and Bohus Ondrusek and Sriram
       	K. Rajamani and Abdullah Ustuner},
         title = {Thorough static analysis of device drivers},
         booktitle = {EuroSys},
         year = {2006},
         pages = {73-85},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/eurosys/2006},
         ee = {http://doi.acm.org/10.1145/1217935.1217943},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Bigot2003,
         author = {C{\'e}line Bigot and Alain Faivre and Jean-Pierre Gallois and Arnault
       	Lapitre and David Lugato and Jean-Yves Pierron and Nicolas Rapin},
         title = {Automatic Test Generation with AGATHA},
         booktitle = {TACAS},
         year = {2003},
         pages = {591-596},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/tacas/2003},
         ee = {http://link.springer.de/link/service/series/0558/bibs/2619/26190591.htm},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Blackburn2002,
         author = {Mark R. Blackburn and Robert Busser and Aaron Nauman and Robert Knickerbocker
       	and Richard Kasuda},
         title = {Mars Polar Lander Fault Identification Using Model-based Testing},
         booktitle = {ICECCS},
         year = {2002},
         pages = {163-},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/iceccs/2002},
         ee = {http://csdl.computer.org/comp/proceedings/iceccs/2002/1757/00/17570163abs.htm},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Blom2004,
         author = {Johan Blom and Anders Hessel and Bengt Jonsson and Paul Pettersson},
         title = {Specifying and Generating Test Cases Using Observer Automata},
         booktitle = {FATES},
         year = {2004},
         pages = {125-139},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/fates/2004},
         ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3395{\&}spage=125},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Blom2003,
         author = {Johan Blom and Bengt Jonsson},
         title = {Automated test generation for industrial Erlang applications},
         booktitle = {Erlang Workshop},
         year = {2003},
         pages = {8-14},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/erlang/2003},
         ee = {http://doi.acm.org/10.1145/940880.940882},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Bohnenkamp2005,
         author = {Henrik C. Bohnenkamp and Axel Belinfante},
         title = {Timed Testing with TorX},
         booktitle = {FM},
         year = {2005},
         pages = {173-188},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/fm/2005},
         ee = {http://dx.doi.org/10.1007/11526841_13},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Boonstoppel2008,
         author = {Peter Boonstoppel and Cristian Cadar and Dawson R. Engler},
         title = {RWset: Attacking Path Explosion in Constraint-Based Test Generation},
         booktitle = {TACAS},
         year = {2008},
         pages = {351-366},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/tacas/2008},
         ee = {http://dx.doi.org/10.1007/978-3-540-78800-3_27},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Bozga2004,
         author = {Marius Bozga and Susanne Graf and Ileana Ober and Iulian Ober and
       	Joseph Sifakis},
         title = {The IF Toolset},
         booktitle = {SFM},
         year = {2004},
         pages = {237-267},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/sfm/2004},
         ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3185{\&}spage=237},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Brandl2008c,
         author = {Harald Brandl and Gordon Fraser and Franz Wotawa},
         title = {Coverage-based Testing Using Qualitative Reasoning Models},
         booktitle = {SEKE},
         year = {2008},
         pages = {393-398},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/seke/2008}
+      }
       @INPROCEEDINGS{Braspenning,
         author = {N.C.W.M. Braspenning and J.M. van de Mortel-Fronczak and H.A.J. Neerhof
       	and J.E. Rooda},
         title = {Model-based integration and testing in practice},
         booktitle = {Tangram: Model-based integration and testing of complex high-tech
       	systems},
         note = {chapter 7},
         crossref = {Tangram2007},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Brucker2009,
         author = {Achim D. Brucker and Burkhart Wolff},
         title = {hol-TestGen},
         booktitle = {FASE},
         year = {2009},
         pages = {417-420},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/fase/2009},
         ee = {http://dx.doi.org/10.1007/978-3-642-00593-0_28},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Brucker2004,
         author = {Achim D. Brucker and Burkhart Wolff},
         title = {Symbolic Test Case Generation for Primitive Recursive Functions},
         booktitle = {FATES},
         year = {2004},
         pages = {16-32},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/fates/2004},
         ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3395{\&}spage=16},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Cadar2006,
         author = {Cristian Cadar and Vijay Ganesh and Peter M. Pawlowski and David
       	L. Dill and Dawson R. Engler},
         title = {EXE: automatically generating inputs of death},
         booktitle = {ACM Conference on Computer and Communications Security},
         year = {2006},
         pages = {322-335},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/ccs/2006usa},
         ee = {http://doi.acm.org/10.1145/1180405.1180445},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Calame2006,
         author = {Jens R. Calame and Nicolae Goga and Natalia Ioustinova and Jaco van
       	de Pol},
         title = {TTCN-3 Testing of Hoorn-Kersenboogerd Railway Interlocking},
         booktitle = {CCECE},
         year = {2006},
         pages = {620-623},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/ccece/2006},
         ee = {http://dx.doi.org/10.1109/CCECE.2006.277762},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Caspi2003,
         author = {Paul Caspi and Adrian Curic and Aude Maignan and Christos Sofronis
       	and Stavros Tripakis},
         title = {Translating Discrete-Time Simulink to Lustre},
         booktitle = {EMSOFT},
         year = {2003},
         pages = {84-99},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/emsoft/2003},
         ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2855{\&}spage=84},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Cheon2007a,
         author = {Yoonsik Cheon},
         title = {Automated Random Testing to Detect Specification-Code Inconsistencies},
         booktitle = {SETP},
         year = {2007},
         pages = {112-119},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/setp/2007},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Cheon2007,
         author = {Yoonsik Cheon and Carlos E. Rubio-Medrano},
         title = {Random Test Data Generation for Java Classes Annotated with JML Specifications},
         booktitle = {Software Engineering Research and Practice},
         year = {2007},
         pages = {385-391},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/serp/2007-2},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Clarke2002,
         author = {Duncan Clarke and Thierry J{\'e}ron and Vlad Rusu and Elena Zinovieva},
         title = {STG: A Symbolic Test Generation Tool},
         booktitle = {TACAS},
         year = {2002},
         pages = {470-475},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/tacas/2002},
         ee = {http://link.springer.de/link/service/series/0558/bibs/2280/22800470.htm},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Constant2007,
         author = {Camille Constant and Bertrand Jeannet and Thierry J{\'e}ron},
         title = {Automatic Test Generation from Interprocedural Specifications},
         booktitle = {TestCom/FATES},
         year = {2007},
         pages = {41-57},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/pts/2007},
         ee = {http://dx.doi.org/10.1007/978-3-540-73066-8_4},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Csallner2008,
         author = {Christoph Csallner and Nikolai Tillmann and Yannis Smaragdakis},
         title = {DySy: dynamic symbolic execution for invariant inference},
         booktitle = {ICSE},
         year = {2008},
         pages = {281-290},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/icse/2008},
         ee = {http://doi.acm.org/10.1145/1368088.1368127},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Dauchy1991,
         author = {Pierre Dauchy and Bruno Marre},
         title = {Test Data Selection From Algebraic Specifications: Application to
       	an Automatic Subway Module},
         booktitle = {ESEC},
         year = {1991},
         pages = {80-100},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/esec/1991},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Dulz2003,
         author = {Winfried Dulz and Fenhua Zhen},
         title = {MaTeLo - Statistical Usage Testing by Annotated Sequence Diagrams,
       	Markov Chains and TTCN-3},
         booktitle = {QSIC},
         year = {2003},
         pages = {336-342},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/qsic/2003},
         ee = {http://csdl.computer.org/comp/proceedings/qsic/2003/2015/00/20150336abs.htm},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Faivre2007,
         author = {Alain Faivre and Christophe Gaston and Pascale Le Gall},
         title = {Symbolic Model Based Testing for Component Oriented Systems},
         booktitle = {TestCom/FATES},
         year = {2007},
         pages = {90-106},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/pts/2007},
         ee = {http://dx.doi.org/10.1007/978-3-540-73066-8_7},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Fritzson1998,
         author = {Peter Fritzson},
         title = {Modelica - A Language for Equation-Based Physical Modeling and High
       	Performance Simulation},
         booktitle = {PARA},
         year = {1998},
         pages = {149-160},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/para/1998},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Garavel2007,
         author = {Hubert Garavel and Radu Mateescu and Fr{\'e}d{\'e}ric Lang and Wendelin
       	Serwe},
         title = {CADP 2006: A Toolbox for the Construction and Analysis of Distributed
       	Processes},
         booktitle = {CAV},
         year = {2007},
         pages = {158-163},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/cav/2007},
         ee = {http://dx.doi.org/10.1007/978-3-540-73368-3_18},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Gaston2006,
         author = {Christophe Gaston and Pascale Le Gall and Nicolas Rapin and Assia
       	Touil},
         title = {Symbolic Execution Techniques for Test Purpose Definition},
         booktitle = {TestCom},
         year = {2006},
         pages = {1-18},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/pts/2006},
         ee = {http://dx.doi.org/10.1007/11754008_1},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Godefroid2005,
         author = {Patrice Godefroid and Nils Klarlund and Koushik Sen},
         title = {{DART}: directed automated random testing},
         booktitle = {PLDI},
         year = {2005},
         pages = {213-223},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/pldi/2005},
         ee = {http://doi.acm.org/10.1145/1065010.1065036},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Goga2001,
         author = {Nicolae Goga},
         title = {Comparing TorX, Autolink, TGV and UIO Test Algorithms},
         booktitle = {SDL Forum},
         year = {2001},
         pages = {379-402},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/sdl/2001},
         ee = {http://link.springer.de/link/service/series/0558/bibs/2078/20780379.htm},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Hackner2008,
         author = {Daniel R. Hackner and Atif M. Memon},
         title = {Test case generator for GUITAR},
         booktitle = {ICSE Companion},
         year = {2008},
         pages = {959-960},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/icse/2008c},
         ee = {http://doi.acm.org/10.1145/1370175.1370207},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Hartman2004a,
         author = {A. Hartman and K. Nagin},
         title = {The AGEDIS tools for model based testing},
         booktitle = {ISSTA},
         year = {2004},
         pages = {129-132},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/issta/2004},
         ee = {http://doi.acm.org/10.1145/1007512.1007529},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Hessel2008,
         author = {Anders Hessel and Kim Guldstrand Larsen and Marius Mikucionis and
       	Brian Nielsen and Paul Pettersson and Arne Skou},
         title = {Testing Real-Time Systems Using UPPAAL},
         booktitle = {Formal Methods and Testing},
         year = {2008},
         pages = {77-117},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/fortest/2008},
         ee = {http://dx.doi.org/10.1007/978-3-540-78917-8_3},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Hessel2006,
         author = {Anders Hessel and Paul Pettersson},
         title = {Model-Based Testing of a WAP Gateway: An Industrial Case-Study},
         booktitle = {FMICS/PDMC},
         year = {2006},
         pages = {116-131},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/fmics/2006},
         ee = {http://dx.doi.org/10.1007/978-3-540-70952-7_8},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Jeannet2005,
         author = {Bertrand Jeannet and Thierry J{\'e}ron and Vlad Rusu and Elena Zinovieva},
         title = {Symbolic Test Selection Based on Approximate Analysis},
         booktitle = {TACAS},
         year = {2005},
         pages = {349-364},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/tacas/2005},
         ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3440{\&}spage=349},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Julius2007,
         author = {A. Agung Julius and Georgios E. Fainekos and Madhukar Anand and Insup
       	Lee and George J. Pappas},
         title = {Robust Test Generation and Coverage for Hybrid Systems},
         booktitle = {HSCC},
         year = {2007},
         pages = {329-342},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/hybrid/2007},
         ee = {http://dx.doi.org/10.1007/978-3-540-71493-4_27},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Koch1998,
         author = {Beat Koch and Jens Grabowski and Dieter Hogrefe and Michael Schmitt
       	II},
         title = {Autolink: A Tool for Automatic Test Generation from SDL Specifications},
         booktitle = {WIFT},
         year = {1998},
         pages = {114-},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/wift/1998},
         ee = {http://csdl.computer.org/comp/proceedings/wift/1998/0081/00/00810114abs.htm},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Longuet2009,
         author = {Delphine Longuet and Marc Aiguier},
         title = {Integration Testing from Structured First-Order Specifications via
       	Deduction Modulo},
         booktitle = {ICTAC},
         year = {2009},
         pages = {261-276},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/ictac/2009},
         ee = {http://dx.doi.org/10.1007/978-3-642-03466-4_17},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Lugato2004,
         author = {David Lugato and Fr{\'e}d{\'e}ric Maraux and Yves Le Traon and V{\'e}ronique
       	Normand and Hubert Dubois and Jean-Yves Pierron and Jean-Pierre Gallois
       	and Cl{\'e}mentine Nebut},
         title = {Automated Functional Test Case Synthesis from THALES industrial Requirements},
         booktitle = {IEEE Real-Time and Embedded Technology and Applications Symposium},
         year = {2004},
         pages = {104-111},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/rtas/2004},
         ee = {http://csdl.computer.org/comp/proceedings/rtas/2004/2148/00/21480104abs.htm},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Marre1995,
         author = {Bruno Marre},
         title = {LOFT: A Tool for Assisting Selection of Test Data Sets from Algebraic
       	Specifications},
         booktitle = {TAPSOFT},
         year = {1995},
         pages = {799-800},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/tapsoft/1995},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Moser2007,
         author = {Andreas Moser and Christopher Kr{\"u}gel and Engin Kirda},
         title = {Exploring Multiple Execution Paths for Malware Analysis},
         booktitle = {IEEE Symposium on Security and Privacy},
         year = {2007},
         pages = {231-245},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/sp/2007},
         ee = {http://dx.doi.org/10.1109/SP.2007.17},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Moura2008,
         author = {Leonardo Mendon\c{c}a de Moura and Nikolaj Bj{\o}rner},
         title = {Z3: An Efficient SMT Solver},
         booktitle = {TACAS},
         year = {2008},
         pages = {337-340},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/tacas/2008},
         ee = {http://dx.doi.org/10.1007/978-3-540-78800-3_24},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Nicola2005,
         author = {Giuseppe De Nicola and Pasquale di Tommaso and Rosaria Esposito and
       	Francesco Flammini and Pietro Marmo and Antonio Orazzo},
         title = {A Grey-Box Approach to the Functional Testing of Complex Automatic
       	Train Protection Systems},
         booktitle = {EDCC},
         year = {2005},
         pages = {305-317},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/edcc/2005},
         ee = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3463{\&}spage=305},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{N'unez2005,
         author = {Manuel N{\'u}{\~n}ez and Ismael Rodr\'{\i}guez},
         title = {Conformance Testing Relations for Timed Systems},
         booktitle = {FATES},
         year = {2005},
         pages = {103-117},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/fates/2005},
         ee = {http://dx.doi.org/10.1007/11759744_8},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Osch2006,
         author = {Michiel van Osch},
         title = {Hybrid Input-Output Conformance and Test Generation},
         booktitle = {FATES/RV},
         year = {2006},
         pages = {70-84},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/fates/2006},
         ee = {http://dx.doi.org/10.1007/11940197_5},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Petrenko2005,
         author = {Alexandre Petrenko and Nina Yevtushenko},
         title = {Conformance Tests as Checking Experiments for Partial Nondeterministic
       	FSM},
         booktitle = {FATES},
         year = {2005},
         pages = {118-133},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/fates/2005},
         ee = {http://dx.doi.org/10.1007/11759744_9},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Rusu2000,
         author = {Vlad Rusu and Lydie du Bousquet and Thierry J{\'e}ron},
         title = {An Approach to Symbolic Test Generation},
         booktitle = {IFM},
         year = {2000},
         pages = {338-357},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/ifm/2000},
         ee = {http://link.springer.de/link/service/series/0558/bibs/1945/19450338.htm},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Schieferdecker2008,
         author = {Ina Schieferdecker and Jens Grabowski and Theofanis Vassiliou-Gioles
       	and George Din},
         title = {The Test Technology TTCN-3},
         booktitle = {Formal Methods and Testing},
         year = {2008},
         pages = {292-319},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/fortest/2008},
         ee = {http://dx.doi.org/10.1007/978-3-540-78917-8_10},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Sen2006,
         author = {Koushik Sen and Gul Agha},
         title = {CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-Checking
       	Tools},
         booktitle = {CAV},
         year = {2006},
         pages = {419-423},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/cav/2006},
         ee = {http://dx.doi.org/10.1007/11817963_38},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Tillmann2008,
         author = {Nikolai Tillmann and Jonathan de Halleux},
         title = {Pex-White Box Test Generation for .NET},
         booktitle = {TAP},
         year = {2008},
         pages = {134-153},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/tap/2008},
         ee = {http://dx.doi.org/10.1007/978-3-540-79124-9_10},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Tretmans1993,
         author = {Jan Tretmans},
         title = {A Formal Approach to Conformance Testing},
         booktitle = {Protocol Test Systems},
         year = {1993},
         pages = {257-276},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/pts/1993},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Veanes2009,
         author = {Margus Veanes and Nikolaj Bj{\o}rner},
         title = {Input-Output Model Programs},
         booktitle = {ICTAC},
         year = {2009},
         pages = {322-335},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/ictac/2009},
         ee = {http://dx.doi.org/10.1007/978-3-642-03466-4_21},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Veanes2008,
         author = {Margus Veanes and Colin Campbell and Wolfgang Grieskamp and Wolfram
       	Schulte and Nikolai Tillmann and Lev Nachmanson},
         title = {Model-Based Testing of Object-Oriented Reactive Systems with Spec
       	Explorer},
         booktitle = {Formal Methods and Testing},
         year = {2008},
         pages = {39-76},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/fortest/2008},
         ee = {http://dx.doi.org/10.1007/978-3-540-78917-8_2},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Weiglhofer2009,
         author = {Martin Weiglhofer and Franz Wotawa},
         title = {Asynchronous Input-Output Conformance Testing},
         booktitle = {COMPSAC (1)},
         year = {2009},
         pages = {154-159},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         crossref = {DBLP:conf/compsac/2009},
         ee = {http://dx.doi.org/10.1109/COMPSAC.2009.194}
+      }
       @MISC{(OMG),
         author = {The Object Management Group (OMG)},
         title = {OMG Systems Modeling Language},
         owner = {harald},
         timestamp = {2009.09.18},
         url = {http://www.omgsysml.org}
+      }
       @ARTICLE{Abrial2007,
         author = {Jean-Raymond Abrial},
         title = {Formal Methods: Theory Becoming Practice},
         journal = {J. UCS},
         year = {2007},
         volume = {13},
         pages = {619-628},
         number = {5},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://www.jucs.org/jucs_13_5/formal_methods_theory_becoming},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{Abrial1996,
         title = {The B-book: assigning programs to meaningsp},
         publisher = {Cambridge University Press},
         year = {1996},
         author = {J.-R. Abrial},
         address = {New York, NY, USA},
         isbn = {0-521-49619-5},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @TECHREPORT{Acree1979,
         author = {A. T. Acree and T. A. Budd and R. A. DeMillo and R. J. Lipton and
       	F. G. Sayward},
         title = {Mutation Analysis},
         institution = {School of Information and Computer Science, Georgia Inst. of Technology,
       	Atlanta, Ga.},
         year = {1979},
         month = {Sept.},
         owner = {gordon},
         timestamp = {2006.04.10}
+      }
       @ARTICLE{Aichernig2006a,
         author = {Aichernig, Bernhard and Delgado, Carlo },
         title = {From Faults Via Test Purposes to Test Cases: On the Fault-Based Testing
       	of Concurrent Systems},
         journal = {Fundamental Approaches to Software Engineering},
         year = {2006},
         pages = {324--338},
         abstract = {Fault-based testing is a technique where testers anticipate errors
       	in a system under test in order to assess or generate test cases.
       	The idea is to have enough test cases capable of detecting these
       	anticipated errors. This paper presents a theory and technique for
       	generating fault-based test cases for concurrent systems. The novel
       	idea is to generate test purposes from faults that have been injected
       	into a model of the system under test. Such test purposes form a
       	specification of a more detailed test case that can detect the injected
       	fault. The theory is based on the notion of refinement. The technique
       	is automated using the TGV test case generator and an equivalence
       	checker of the CADP tools. A case study of testing web servers demonstrates
       	the practicability of the approach.},
         citeulike-article-id = {2637989},
         doi = {10.1007/11693017\_24},
         keywords = {bibtex-import, tug},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/fase06.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:41},
         priority = {2},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/10.1007/11693017\_24}
+      }
       @ARTICLE{Aichernig2003,
         author = {Bernhard K. Aichernig},
         title = {Mutation Testing in the Refinement Calculus},
         journal = {Formal Aspects of Computing Journal},
         year = {2003},
         volume = {15},
         pages = {280--295},
         number = {2},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Aichernig2001,
         author = {Bernhard K.~Aichernig},
         title = {Test-Design through Abstraction: a Systematic Approach Based on the
       	Refinement Calculus},
         journal = {Journal of Universal Computer Science},
         year = {2001},
         volume = {7},
         pages = {710--735},
         number = {8},
         month = aug,
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Aichernig2011,
         author = {Bernhard K. Aichernig and Harald Brandl and Elisabeth J\"obstl and
       	Willibald Krenn},
         title = {Efficient Mutation Killers in Action},
         booktitle = {Proceedings of the fourth IEEE International Conference on Software
       	Testing, Verification and Validation (ICST)},
         year = {2011},
         month = {March},
         note = {in press}
+      }
       @INPROCEEDINGS{Aichernig2010a,
         author = {Bernhard K. Aichernig and Harald Brandl and Elisabeth J\"obstl and
       	Willibald Krenn},
         title = {{UML} in Action: A Two-Layered Interpretation for Testing},
         booktitle = {UML\&FM},
         year = {2010},
         series = {ACM Software Engineering Notes (SEN)},
         note = {in press}
+      }
       @CONFERENCE{Aichernig2009c,
         author = {Bernhard K. Aichernig and Harald Brandl and Willibald Krenn},
         title = {Qualitative Action Systems},
         booktitle = {ICFEM},
         year = {2009},
         editor = {Karin Breitman and Ana Cavalcanti},
         volume = {5885},
         series = {LNCS},
         publisher = {Springer},
         longbooktitle = {Formal Methods and Software Engineering, 11th International Conference
       	on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brasil,
       	December 9-12, 2009. Proceedings}
+      }
       @TECHREPORT{Aichernig2009a,
         author = {Bernhard K. Aichernig and Harald Brandl and Willibald Krenn and Rudolf
       	Schlatte},
         title = {Model-Based Test Case Generation Techniques: A Survey},
         institution = {Institute for Software Technology, TU Graz},
         year = {2009},
         owner = {harald},
         timestamp = {2010.10.31}
+      }
       @ARTICLE{Aichernig2009,
         author = {Aichernig, Bernhard K. and Brandl, Harald and Wotawa, Franz},
         title = {Conformance Testing of Hybrid Systems with Qualitative Reasoning
       	Models},
         journal = {Electron. Notes Theor. Comput. Sci.},
         year = {2009},
         volume = {253},
         pages = {53--69},
         number = {2},
         address = {Amsterdam, The Netherlands, The Netherlands},
         doi = {http://dx.doi.org/10.1016/j.entcs.2009.09.051},
         issn = {1571-0661},
         publisher = {Elsevier Science Publishers B. V.}
+      }
       @INPROCEEDINGS{Aichernig2006,
         author = {Bernhard K. Aichernig and Carlo Corrales Delgado},
         title = {From Faults Via Test Purposes to Test Cases: On the Fault-Based Testing
       	of Concurrent Systems.},
         booktitle = {Proceedings of the 9th International Conference on Fundamental Approaches
       	to Software Engineering},
         year = {2006},
         volume = {3922},
         series = {LNCS},
         pages = {324-338},
         publisher = {Springer},
         abstract = {This paper discusses how to use a fault based approach for test purpose
       	generation. The authors generate test purposes by generating a mutant
       	from the specification. Therfore they apply one of 27 mutation operators
       	to the specification. Afterwards, they generate the labeled transition
       	systems of the specification and the mutant. By doing an equivalence
       	check between the two LTSs the authors generate a discriminating
       	sequence. This sequence is used as new test purpose on the specification.},
         comment = {p,r},
         file = {aichernig2006faults.pdf:aichernig2006faults.pdf:PDF},
         keywords = {mutation, test purpose generation, lts, refinement,},
         owner = {martin},
         timestamp = {2007.07.27}
+      }
       @ARTICLE{Aichernig2007b,
         author = {Aichernig, Bernhard K. and He, Jifeng },
         title = {Mutation Testing in UTP},
         journal = {Under consideration for publication in Formal Aspects of Computing},
         year = {2007},
         abstract = {This paper presents a theory of testing that integrates into Hoare
       	and He's Unifying Theory of Programming (UTP).We give test cases
       	a denotational semantics by viewing them as specification predicates.
       	This reformulation of test cases allows for relating test cases via
       	refinement to specifications and programs. Having such a refinement
       	order that integrates test cases, we develop a testing theory for
       	fault-based testing. Fault-based testing uses test data designed
       	to demonstrate the absence of a set of pre-specified faults. A well-known
       	fault-based technique is mutation testing. In mutation testing, first,
       	faults are injected into a program by altering (mutating) its source
       	code. Then, test cases that can detect these errors are designed.
       	The assumption is that other faults will be caught, too. In this
       	paper, we apply the mutation technique to both, specifications and
       	programs. Using our theory of testing, two new test case generation
       	laws for detecting injected (anticipated) faults are presented: one
       	is based on the semantic level of UTP design predicates, the other
       	on the algebraic properties of a small programming language. Keywords:
       	specification-based testing; fault-based testing; mutation testing;
       	Unifying Theories of Programming; refinement calculus; algebra of
       	programming.},
         citeulike-article-id = {2637991},
         keywords = {bibtex-import, mutation-testing, reading-group-testing, softnet, tug},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/facj08.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:41},
         priority = {2},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Aichernig2005,
         author = {Bernhard K. Aichernig and Percy Antonio {Pari Salas}},
         title = {Test Case Generation by {OCL} Mutation and Constraint Solving},
         booktitle = {{QSIC 2OO5}, Proceedings of the Fifth International Conference on
       	Quality Software, Melbourne, Australia, September 19-21, 2005},
         year = {2005},
         editor = {Kai-Yuan Cai and Atsushi Ohnishi and M.F. Lau},
         pages = {64--71},
         publisher = {IEEE Computer Society Press},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Aichernig2007a,
         author = {Bernhard K. Aichernig and Bernhard Peischl and Martin Weiglhofer
       	and Franz Wotawa},
         title = {Protocol Conformance Testing a {SIP} Registrar: An Industrial Application
       	of Formal Methods},
         booktitle = {Proceedings of the 5th IEEE International Conference on Software
       	Engineering and Formal Methods},
         year = {2007},
         editor = {Mike Hinchey and Tiziana Margaria},
         pages = {215--224},
         address = {London, UK},
         publisher = {IEEE},
         comment = {a},
         file = {aichernig2007protocol.pdf:aichernig2007protocol.pdf:PDF},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Aichernig19-20Sept.2005,
         author = {Aichernig, B. K. and Salas, P. A. P. },
         title = {Test case generation by OCL mutation and constraint solving},
         journal = {Quality Software, 2005. (QSIC 2005). Fifth International Conference
       	on},
         year = {19-20 Sept. 2005},
         pages = {64--71},
         citeulike-article-id = {2637988},
         doi = {10.1109/QSIC.2005.63},
         keywords = {bibtex-import, case, constraint, fault, fault-based, formal, generation,
       	language, languages, mutation, ocl, problem, program, programming,
       	satisfaction, semantics, software, solving, specification, state-based,
       	test, testing, theory, tolerance, tug},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/01579121.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:41},
         priority = {2},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/10.1109/QSIC.2005.63}
+      }
       @INPROCEEDINGS{Aichernig2007,
         author = {Aichernig, Bernhard K. and Weiglhofer, Martin and Peischl, Bernhard
       	and Wotawa, Franz },
         title = {Test purpose generation in an industrial application},
         booktitle = {A-MOST '07: Proceedings of the 3rd international workshop on Advances
       	in model-based testing},
         year = {2007},
         pages = {115--125},
         address = {New York, NY, USA},
         publisher = {ACM},
         citeulike-article-id = {2637993},
         doi = {http://doi.acm.org/10.1145/1291535.1291547},
         keywords = {bibtex-import, tug},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/amost2007.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:41},
         priority = {2},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/10.1145/1291535.1291547}
+      }
       @ARTICLE{Aichernig2008,
         author = {Bernhard K. Aichernig and Martin Weiglhofer and Franz Wotawa},
         title = {Improving Fault-based Conformance Testing},
         journal = {Electronic Notes in Theoretical Computer Science},
         year = {2008},
         note = {to appear},
         comment = {a},
         file = {aichernig2008improving.pdf:aichernig2008improving.pdf:PDF},
         owner = {martin},
         timestamp = {2008.05.20}
+      }
       @INPROCEEDINGS{Alur1990,
         author = {Rajcev Alur and Costas Courcoubetis and David Dill},
         title = {Model-{C}hecking for {R}eal-{T}ime {S}ystems},
         booktitle = {Proceedings of the {F}ifth {A}nnual {IEEE} {S}ymposium on {L}ogic
       	in {C}omputer {S}cience ({LICS} 90)},
         year = {1990},
         pages = {414-425},
         owner = {gordon},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Alur2000,
         author = {Rajeev Alur and Radu Grosu and Yerang Hur and Vijay Kumar and Insup
       	Lee},
         title = {Modular Specification of Hybrid Systems in CHARON},
         booktitle = {HSCC '00: Proceedings of the Third International Workshop on Hybrid
       	Systems: Computation and Control},
         year = {2000},
         pages = {6--19},
         address = {London, UK},
         publisher = {Springer-Verlag},
         isbn = {3-540-67259-1},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Ammann1999,
         author = {Paul Ammann and Paul E. Black},
         title = {A {S}pecification-{B}ased {C}overage {M}etric to {E}valuate {T}est
       	{S}ets.},
         booktitle = {{HASE} '99: The 4th {IEEE} International Symposium on High-Assurance
       	Systems Engineering},
         year = {1999},
         pages = {239--248},
         address = {Washington, DC, USA},
         publisher = {IEEE Computer Society},
         isbn = {0-7695-0418-3},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Back1988,
         author = {R. J. R. Back and F. Kurki-Suonio},
         title = {Distributed cooperation with action systems},
         journal = {ACM Trans. Program. Lang. Syst.},
         year = {1988},
         volume = {10},
         pages = {513--554},
         number = {4},
         address = {New York, NY, USA},
         doi = {http://doi.acm.org/10.1145/48022.48023},
         issn = {0164-0925},
         owner = {harald},
         publisher = {ACM},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Back1983,
         author = {Back, Ralph-Johan and Kurki-Suonio, Reino},
         title = {Decentralization of Process Nets with Centralized Control},
         booktitle = {Proceedings of the 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed
       	Computing},
         year = {1983},
         pages = {131-142},
         address = {Montreal, Quebec, Canada},
         organization = {ACM},
         project = {actions distributed}
+      }
       @ARTICLE{Back2001,
         author = {Back, Ralph-Johan and Petre, Luigia and Porres, Ivan},
         title = {Continuous Action Systems as a Model for Hybrid Systems},
         journal = {Nordic Journal of Computing},
         year = {2001},
         volume = {8},
         pages = {2--21},
         number = {1},
         timestamp = {2009.04.01}
+      }
       @ARTICLE{Back1991,
         author = {Back, Ralph-Johan and Sere, Kaisa},
         title = {Stepwise Refinement of Action Systems},
         journal = {Structured Programming},
         year = {1991},
         volume = {12},
         pages = {17--30}
+      }
       @INPROCEEDINGS{Back1994,
         author = {Back, Ralph-Johan and von Wright, Joakim},
         title = {Trace Refinement of Action Systems},
         booktitle = {CONCUR-94:Concurrency Theory},
         year = {1994},
         editor = {Jonsson, B and Parrow, J.},
         volume = {836},
         series = {Lecture Notes in Computer Science},
         pages = {367-384},
         address = {Uppsala, Sweden},
         month = {Aug},
         publisher = {Springer-Verlag}
+      }
       @BOOK{Back1998,
         title = {Refinement Calculus, a Systematic Introduction},
         publisher = {Springer},
         year = {1998},
         author = {Ralph-Johan Back and Joakim von Wright},
         series = {Graduate Texts in Computer Science},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Backus1978,
         author = {John W. Backus},
         title = {Can Programming Be Liberated From the von Neumann Style? A Functional
       	Style and its Algebra of Programs},
         journal = {Commun. ACM},
         year = {1978},
         volume = {21},
         pages = {613-641},
         number = {8},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Badban2006,
         author = {Bahareh Badban and Martin Fr\"{a}nzle and Jan Peleska and Tino Teige},
         title = {Test automation for hybrid systems},
         booktitle = {SOQUA '06: Proceedings of the 3rd international workshop on Software
       	quality assurance},
         year = {2006},
         pages = {14--21},
         address = {New York, NY, USA},
         publisher = {ACM},
         doi = {http://doi.acm.org/10.1145/1188895.1188902},
         isbn = {1-59593-584-3},
         location = {Portland, Oregon},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @MASTERSTHESIS{Bakker2006,
         author = {Elinor Bakker},
         title = {Qualitative models of population dynamics},
         school = {University of Amsterdam},
         year = {2006},
         owner = {harald},
         timestamp = {2010.08.31}
+      }
       @ARTICLE{Balcer1989,
         author = {M. Balcer and W. Hasling and T. Ostrand},
         title = {Automatic generation of test scripts from formal test specifications},
         journal = {SIGSOFT Softw. Eng. Notes},
         year = {1989},
         volume = {14},
         pages = {210--218},
         number = {8},
         address = {New York, NY, USA},
         doi = {http://doi.acm.org/10.1145/75309.75332},
         issn = {0163-5948},
         owner = {harald},
         publisher = {ACM},
         timestamp = {2009.09.18}
+      }
       @TECHREPORT{Ball2004,
         author = {Ball, Thomas },
         title = {A Theory of Predicate-Complete Test Coverage and Generation},
         institution = {Microsoft Research},
         year = {2004},
         abstract = {Consider a program with m statements and n predicates, where the predicates
       	are derived from the conditional state- ments and assertions in a
       	program, as well as from implicit run-time safety checks. An observable
       	state is an evaluation of the n predicates under some state at a
       	program statement. The goal of predicate-complete testing (PCT) is
       	to cover every reachable observable state (at most m x 2n of them)
       	in a program. PCT coverage is a new form of coverage motivated by
       	the observation that certain errors in a pro- gram only can be exposed
       	by considering the complex depen- dences between the predicates in
       	a program and the state- ments whose execution they control. PCT
       	coverage sub- sumes many existing control-flow coverage criteria
       	and is incomparable to path coverage. To support the generation of
       	tests to achieve high PCT coverage, we show how to define an upper
       	bound U and lower bound L to the (unknown) set of reachable observable
       	states R. These bounds are constructed automatically using Boolean
       	(predicate) abstraction over modal transition sys- tems and can be
       	used to guide test generation via symbolic execution. We define a
       	static coverage metric as |L|/|U |, which measures the ability of
       	the Boolean abstraction to achieve high PCT coverage. Finally we
       	show how to in- crease this ratio by the addition of new predicates.},
         citeulike-article-id = {2638017},
         keywords = {bibtex-import},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/TR-2004-28.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:45},
         priority = {2},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{BANDELJ2002,
         author = {Aleksander Bandelj and Ivan Bratko and Dorian Šuc},
         title = {Qualitative simulation with {CLP}},
         booktitle = {In Proc. of 16th International Workshop on Qualitative Reasoning
       	(QR’02},
         year = {2002}
+      }
       @INPROCEEDINGS{Barbey1994,
         author = {S. Barbey and D. Buchs},
         title = {Testing {Ada} abstract data types using formal specifications.},
         booktitle = {1st Int. Eurospace-Ada-Europe Symposium},
         year = {1994},
         volume = {887},
         series = {Lecture Notes in Computer Science},
         pages = {76--89},
         publisher = {Springer-Verlag},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{Barnes2003,
         title = {High Integrity Software: The SPARK Approach to Safety and Security},
         publisher = {Addison-Wesley Longman Publishing Co., Inc.},
         year = {2003},
         author = {John Barnes},
         address = {Boston, MA, USA},
         isbn = {0321136160},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INCOLLECTION{Barnett2005,
         author = {Mike Barnett and K. Rustan M. Leino and Wolfram Schulte},
         title = {The {Spec\#} Programming System: An Overview},
         booktitle = {Construction and Analysis of Safe, Secure, and Interoperable Smart
       	Devices},
         publisher = {Springer-Verlag},
         year = {2005},
         volume = {3362},
         series = {Lecture Notes in Computer Science},
         pages = {49--69},
         keywords = {survey, testing},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Bauer2007,
         author = {Bauer, A. and Pister, M. and Tautschnig, M. },
         title = {Tool-support for the analysis of hybrid systems and models},
         booktitle = {Design, Automation \& Test in Europe Conference \& Exhibition, 2007.
       	DATE '07},
         year = {2007},
         pages = {1--6},
         abstract = {This paper introduces a method and tool-support for the automatic
       	analysis and verification of hybrid and embedded control systems,
       	whose continuous dynamics are often modelled using MATLAB/Simulink.
       	The method is based upon converting system models into the uniform
       	input language of our efficient multi-domain constraint solving library,
       	ABSOLVER, which is then used for subsequent analysis. Basically,
       	ABSOLVER is an extensible SMT-solver which addresses mixed Boolean
       	and (nonlinear) arithmetic constraint problems as they appear in
       	the design of hybrid control systems. It allows the integration and
       	semantic connection of various domain specific solvers via a logical
       	circuit, such that almost arbitrary multi-domain constraint problems
       	can be formulated and solved. Its design has been tailored for extensibility,
       	and thus facilitates the reuse of expert knowledge, in that the most
       	appropriate solver for a given task can be integrated and used. As
       	such the only constraint over the problem domain is the capability
       	of the employed solvers. Our approach to systems verification has
       	been validated in an industrial case study using the model of a car's
       	steering control system. However, additional benchmarks show that
       	other hard instances of problems could also be solved by ABSOLVER
       	in respectable time, and that for some instances, ABsOLVER's approach
       	was the only means of solving a problem at all},
         citeulike-article-id = {2721207},
         doi = {10.1109/DATE.2007.364411},
         journal = {Design, Automation \& Test in Europe Conference \& Exhibition, 2007.
       	DATE '07},
         keywords = {mogentes, sat, smt, testing},
         owner = {harald},
         posted-at = {2008-05-05 12:40:32},
         priority = {2},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/10.1109/DATE.2007.364411}
+      }
       @INPROCEEDINGS{Beckman2008,
         author = {Nels E. Beckman and Aditya V. Nori and Sriram K. Rajamani and Robert
       	J. Simmons},
         title = {Proofs from Tests},
         booktitle = {Poceedings of the International Symposium on Software Testing and
       	Analysis},
         year = {2008},
         note = {to appear},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Belinfante2010,
         author = {Axel Belinfante},
         title = {{JT}or{X}: A Tool for On-Line Model-Driven Test Derivation and Execution},
         booktitle = {TACAS},
         year = {2010},
         pages = {266-270},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://dx.doi.org/10.1007/978-3-642-12002-2_21}
+      }
       @INPROCEEDINGS{Belinfante2004,
         author = {Axel Belinfante and Lars Frantzen and Christian Schallhart},
         title = {Tools for Test Case Generation},
         booktitle = {Model-Based Testing of Reactive Systems},
         year = {2004},
         pages = {391-438},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://dx.doi.org/10.1007/11498490_18},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Bernard2004,
         author = {Eddy Bernard and Bruno Legeard and Xavier Luck and Fabien Peureux},
         title = {Generation of test sequences from formal specifications: GSM 11-11
       	standard case study},
         journal = {Softw., Pract. Exper.},
         year = {2004},
         volume = {34},
         pages = {915-948},
         number = {10},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://dx.doi.org/10.1002/spe.597},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Bernot1991a,
         author = {Bernot, Gilles},
         title = {Testing Against Formal Specifications: A Theoretical View},
         booktitle = {TAPSOFT '91: Proceedings of the International Joint Conference on
       	Theory and Practice of Software Development, Volume 2: Advances in
       	Distributed Computing (ADC) and Colloquium on Combining Paradigms
       	for Software Developmemnt (CCPSD)},
         year = {1991},
         pages = {99--119},
         address = {London, UK},
         publisher = {Springer-Verlag},
         isbn = {3-540-53981-6}
+      }
       @ARTICLE{Bernot1991,
         author = {G. Bernot and M.-C. Gaudel and B. Marre},
         title = {Software testing based on formal specifications: a theory and a tool.},
         journal = {Software Engineering Journal},
         year = {1991},
         volume = {6},
         pages = {387--405},
         number = {6},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Berry1992,
         author = {Gerard Berry and Georges Gonthier},
         title = {The Esterel Synchronous Programming Language: Design, Semantics,
       	Implementation},
         journal = {Science of Computer Programming},
         year = {1992},
         volume = {19},
         pages = {87-152},
         number = {2},
         owner = {harald},
         timestamp = {2009.09.18},
         url = {citeseer.ist.psu.edu/berry92esterel.html}
+      }
       @ARTICLE{Beyer2004,
         author = {Beyer, Dirk and Chlipala, Adam J. and Henzinger, Thomas A. and Jhala,
       	Ranjit and Majumdar, Rupak },
         title = {Generating Tests from Counterexamples},
         journal = {icse},
         year = {2004},
         volume = {0},
         pages = {326--335},
         abstract = {We have extended the software model checker BLAST to automatically
       	generate test suites that guarantee full coverage with respect to
       	a given predicate. More precisely, given a C program and a target
       	predicate, BLAST determines the set  of program locations which
       	program execution can reach with true, and automatically generates
       	a set of test vectors that exhibit the truth of at all locations
       	in . We have used BLAST to generate test suites and to detect dead
       	code in C programs with up to 30 K lines of code. The analysis and
       	test-vector generation is fully automatic (no user intervention)
       	and exact (no false positives).},
         address = {Los Alamitos, CA, USA},
         citeulike-article-id = {2638016},
         doi = {http://doi.ieeecomputersociety.org/10.1109/ICSE.2004.1317455},
         keywords = {bibtex-import},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/2004-ICSE.Generating\_Tests\_from\_Counterexamples.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:45},
         priority = {2},
         publisher = {IEEE Computer Society},
         timestamp = {2009.09.18},
         url = {http://doi.ieeecomputersociety.org/10.1109/ICSE.2004.1317455}
+      }
       @ARTICLE{Biere2003,
         author = {Armin Biere and Alessandro Cimatti and Edmund M. Clarke and Ofer
       	Strichman and Yunshan Zhu},
         title = {Bounded model checking},
         journal = {Advances in Computers},
         year = {2003},
         volume = {58},
         pages = {118-149},
         bibsource = {DBLP, http://dblp.uni-trier.de}
+      }
       @INPROCEEDINGS{Black2000,
         author = {Paul E. Black and Vadim Okun and Yaacov Yesha},
         title = {Mutation {O}perators for {S}pecifications},
         booktitle = {Proceedings of the {F}ifteenth {IEEE} {I}nternational {C}onference
       	on {A}utomated {S}oftware {E}ngineering ({ASE}'00)},
         year = {2000},
         address = {Washington, DC, USA},
         publisher = {IEEE Computer Society},
         owner = {gordon},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Blackburn1996,
         author = {Blackburn, MR and Busser, RD},
         title = {{T-VEC: a tool for developing critical systems}},
         journal = {Computer Assurance, 1996. COMPASS'96,'Systems Integrity. Software
       	Safety. Process Security'. Proceedings of the Eleventh Annual Conference
       	on},
         year = {1996},
         pages = {237--249},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Bohn2002,
         author = {J. Bohn and W. Damm and J. Klose and A. Moik and H. Wittke},
         title = {Modeling and validating train system applications using Statemate
       	and Live Sequence Charts},
         booktitle = {Proceedings of the Conference on Integrated Design and Process Technology
       	(IDPT2002)},
         year = {2002},
         editor = {H. Ehrig and B. J. Kramer and A. Ertas},
         owner = {harald},
         timestamp = {2009.09.18},
         url = {citeseer.ist.psu.edu/bohn02modeling.html}
+      }
       @INPROCEEDINGS{Bonsangue1998,
         author = {Marcello M. Bonsangue and Joost N. Kok and Kaisa Sere},
         title = {An Approach to Object-Orientation in Action Systems},
         booktitle = {Mathematics of Program Construction, LNCS 1422},
         year = {1998},
         pages = {68--95},
         publisher = {Springer},
         owner = {wkrenn},
         timestamp = {2010.02.04}
+      }
       @ARTICLE{Borras2006,
         author = {Cari Borr\'as},
         title = {{Overexposure of Radiation Therapy Patients in Panama: Problem Recognition
       	and Follow-Up Measures}},
         journal = {{Rev Panam Salud Publica}},
         year = {2006},
         volume = {20},
         pages = {173-187},
         number = {2/3},
         file = {:home/elisabeth/Diplomarbeit/Literatur/PDFs/panama.pdf:PDF},
         keywords = {http://journal.paho.org/uploads/1162234952.pdf},
         owner = {elisabeth},
         timestamp = {2009.09.08},
         url = {http://journal.paho.org/uploads/1162234952.pdf}
+      }
       @ARTICLE{Boug'e1985,
         author = {L. Boug\'{e}},
         title = {A contribution to the theory of program testing},
         journal = {Theoretical Computer Science},
         year = {1985},
         volume = {37},
         pages = {151--181},
         number = {2},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PHDTHESIS{Boug'e1982,
         author = {L. Boug\'{e}},
         title = {Mod\'{e}lisation de la notion de test de programmes, application
       	\`{a} la production de jeux de test},
         school = {Universit\'{e} de Paris 6},
         year = {1982},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Boug'e1986,
         author = {L. Boug\'{e} and N. Choquet and L. Fribourg and M.-C. Gaudel},
         title = {Test set generation from algebraic specifications using logic programming.},
         journal = {Journal of Systems and Software},
         year = {1986},
         volume = {6},
         pages = {343--360},
         number = {4},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Bouissou2008,
         author = {Bouissou, Olivier and Martel, Matthieu},
         title = {Abstract interpretation of the physical inputs of embedded programs},
         booktitle = {VMCAI'08: Proceedings of the 9th international conference on Verification,
       	model checking, and abstract interpretation},
         year = {2008},
         pages = {37--51},
         address = {Berlin, Heidelberg},
         publisher = {Springer-Verlag},
         isbn = {3-540-78162-5, 978-3-540-78162-2},
         location = {San Francisco, USA}
+      }
       @INPROCEEDINGS{Bouissou2008a,
         author = {Bouissou, Olivier and Martel, Matthieu},
         title = {A hybrid denotational semantics for hybrid systems},
         booktitle = {ESOP'08/ETAPS'08: Proceedings of the Theory and practice of software,
 th European conference on Programming languages and systems},
         year = {2008},
         pages = {63--77},
         address = {Berlin, Heidelberg},
         publisher = {Springer-Verlag},
         isbn = {3-540-78738-0, 978-3-540-78738-9},
         location = {Budapest, Hungary}
+      }
       @ARTICLE{Bourque2004,
         author = {Bourque, P. and Dupuis, R.},
         title = {Guide to the Software Engineering Body of Knowledge 2004 Version},
         journal = {Guide to the Software Engineering Body of Knowledge, 2004. SWEBOK},
         year = {2004},
         month = { }
+      }
       @MANUAL{Bouwer2005,
         title = {User Manual for Single-User Version of QR Workbench},
         author = {Bouwer, A. and Liem, J. and Bredeweg, B.},
         organization = {Naturnet-Redime, STREP project co-funded by the European Commission
       	within the Sixth Framework Programme (2002-2006)},
         year = {2005},
         note = {Project no. 004074. Project deliverable D4.2.1.},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Boyapati2002,
         author = {Boyapati, Chandrasekhar and Khurshid, Sarfraz and Marinov, Darko
       	},
         title = {Korat: automated testing based on Java predicates},
         booktitle = {ISSTA '02: Proceedings of the 2002 ACM SIGSOFT international symposium
       	on Software testing and analysis},
         year = {2002},
         pages = {123--133},
         address = {New York, NY, USA},
         publisher = {ACM},
         abstract = {This paper presents Korat, a novel framework for automated testing
       	of Java programs. Given a formal specification for a method, Korat
       	uses the method precondition to automatically generate all (nonisomorphic)
       	test cases up to a given small size. Korat then executes the method
       	on each test case, and uses the method postcondition as a test oracle
       	to check the correctness of each output. To generate test cases for
       	a method, Korat constructs a Java predicate (i.e., a method that
       	returns a boolean) from the method's precondition. The heart of Korat
       	is a technique for automatic test case generation: given a predicate
       	and a bound on the size of its inputs, Korat generates all (nonisomorphic)
       	inputs for which the predicate returns true. Korat exhaustively explores
       	the bounded input space of the predicate but does so efficiently
       	by monitoring the predicate's executions and pruning large portions
       	of the search space. This paper illustrates the use of Korat for
       	testing several data structures, including some from the Java Collections
       	Framework. The experimental results show that it is feasible to generate
       	test cases from Java predicates, even when the search space for inputs
       	is very large. This paper also compares Korat with a testing framework
       	based on declarative specifications. Contrary to our initial expectation,
       	the experiments show that Korat generates test cases much faster
       	than the declarative framework.},
         citeulike-article-id = {2638005},
         doi = {http://doi.acm.org/10.1145/566172.566191},
         keywords = {bibtex-import, boundingsymbolic, execution, loop},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/p123-boyapati.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:44},
         priority = {2},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/10.1145/566172.566191}
+      }
       @INCOLLECTION{Bozga1998,
         author = {Bozga, Marius and Daws, Conrado and Maler, Oded and Olivero, Alfredo
       	and Tripakis, Stavros and Yovine, Sergio},
         title = {Kronos: A model-checking tool for real-time systems},
         booktitle = {Formal Techniques in Real-Time and Fault-Tolerant Systems},
         publisher = {Springer Berlin / Heidelberg},
         year = {1998},
         editor = {Ravn, Anders and Rischel, Hans},
         volume = {1486},
         series = {Lecture Notes in Computer Science},
         pages = {298-302},
         note = {10.1007/BFb0055357},
         affiliation = {Verimag, Centre équation 2 avenue de Vignate 38610 Gières France 2
       	avenue de Vignate 38610 Gières France},
         url = {http://dx.doi.org/10.1007/BFb0055357}
+      }
       @INPROCEEDINGS{Brandl2009,
         author = {Harald Brandl},
         title = {Testing of Hybrid Systems using Qualitative Models},
         year = {2009},
         editor = {MohammadReza Mousavi and Emil Sekerinski},
         volume = {Proceedings of Formal Methods 2009 Doctoral Symposium},
         pages = {46--52},
         month = {11},
         owner = {harald},
         timestamp = {2010.10.09},
         url = {http://www.win.tue.nl/~mousavi/fm09ds.pdf}
+      }
       @INPROCEEDINGS{Brandl2008,
         author = {Harald Brandl and Gordon Fraser and Franz Wotawa},
         title = {A report on {QR}-based testing},
         booktitle = {22nd International Workshop on Qualitative Reasoning},
         year = {2008},
         pages = {1--9},
         location = {Boulder, CO},
         url = {www.cs.colorado.edu/~lizb/qr08/papers/Brandl.pdf}
+      }
       @INPROCEEDINGS{Brandl2008b,
         author = {Harald Brandl and Gordon Fraser and Franz Wotawa},
         title = {{QR}-model based testing},
         booktitle = {AST '08: Proceedings of the 3rd international workshop on Automation
       	of software test},
         year = {2008},
         pages = {17--20},
         address = {New York, NY, USA},
         publisher = {ACM},
         doi = {http://doi.acm.org/10.1145/1370042.1370046},
         isbn = {978-1-60558-030-2},
         location = {Leipzig, Germany},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Brandl2010,
         author = {Harald Brandl and Martin Weiglhofer and Bernhard K. Aichernig},
         title = {Automated Conformance Verification of Hybrid Systems},
         journal = {Quality Software, International Conference on},
         year = {2010},
         volume = {0},
         pages = {3-12},
         address = {Los Alamitos, CA, USA},
         doi = {http://doi.ieeecomputersociety.org/10.1109/QSIC.2010.53},
         issn = {1550-6002},
         publisher = {IEEE Computer Society}
+      }
       @INPROCEEDINGS{Brandl2008a,
         author = {Harald Brandl and Franz Wotawa},
         title = {Test Case Generation from {QR} Models},
         booktitle = {21st International Conference on Industrial, Engineering \& Other
       	Applications of Applied Intelligent Systems},
         year = {2008},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Braspenning2006,
         author = {N. C. W. M. Braspenning and J. M. van de Mortel-Fronczak and J. E.
       	Rooda},
         title = {A Model-based Integration and Testing Method to Reduce System Development
       	Effort},
         journal = {Electr. Notes Theor. Comput. Sci.},
         year = {2006},
         volume = {164},
         pages = {13-28},
         number = {4},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://dx.doi.org/10.1016/j.entcs.2006.09.003},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Bredeweg2006,
         author = {Bert Bredeweg and Anders Bouwer and Jelmer Jellema and Dirk Bertels
       	and Floris Floris Linnebank and Jochem Liem},
         title = {Garp3 - A new Workbench for Qualitative Reasoning and Modelling},
         booktitle = {Proceedings of 20th International Workshop on Qualitative Reasoning
       	(QR-06)},
         year = {2006},
         pages = {21-28},
         address = {Hannover, New Hampshire, USA},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @MANUAL{Bredeweg2005,
         title = {Curriculum for learning about QR modelling},
         author = {Bredeweg, B. and Liem, J. and Bouwer, A. and Salles, P},
         organization = {Naturnet-Redime, STREP project co-funded by the European Commission
       	within the Sixth Framework Programme (2002-2006)},
         year = {2005},
         note = {Project no. 004074. Project deliverable D6.9.1.},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Brinksma1988,
         author = {Ed Brinksma},
         title = {A theory for the derivation of tests},
         booktitle = {Protocol Specification, Testing, and Verification VIII},
         year = {1988},
         editor = {S. Aggarwal and K. Sabnani},
         pages = {402--416},
         publisher = {North-Holland}
+      }
       @INPROCEEDINGS{Brinksma1995,
         author = {Brinksma, Ed and Scollo, Giuseppe and Steenbergen, Chris},
         title = {Lotos specifications, their implementations and their tests},
         booktitle = {Conformance testing methodologies and architectures for OSI protocols},
         year = {1995},
         editor = {Richard Jerry Linn and M. {\"U}mit Uyar},
         pages = {468--479},
         address = {Los Alamitos, CA, USA},
         publisher = {IEEE Computer Society Press},
         isbn = {0-8186-5352-3}
+      }
       @INPROCEEDINGS{Brinksma2000,
         author = {Ed Brinksma and Jan Tretmans},
         title = {Testing Transition Systems: An Annotated Bibliography},
         booktitle = {MOVEP},
         year = {2000},
         pages = {187-195},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://link.springer.de/link/service/series/0558/bibs/2067/20670187.htm},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Broy1999,
         author = {Manfred Broy and Franz Huber and Bernhard Sch{\"a}tz},
         title = {AutoFocus - Ein Werkzeugprototyp zur Entwicklung eingebetteter Systeme},
         journal = {Inform., Forsch. Entwickl.},
         year = {1999},
         volume = {14},
         pages = {121-134},
         number = {3},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://link.springer.de/link/service/journals/00450/bibs/9014003/90140121.htm},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Brucker2008,
         author = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
         title = {Verifying Test-Hypotheses -- An Experiment in Test and Proof},
         booktitle = {Model-based Testing (MBT 2008)},
         year = {2008},
         editor = {Bernd Finkbeiner and Yuri Gurevich and Alexander K. Petrenko},
         series = j-entcs,
         address = {Budapest, Hungary},
         publisher = {Elsevier Science Publishers},
         note = {To appear.},
         abstract = {\testgen is a specification and test case generation environment extending
       	the interactive theorem prover Isabelle/\acs{hol}. The \testgen method
       	is two-staged: first, the original formula, called \emph{test specification},
       	is partitioned into \emph{test cases} by transformation into a normal
       	form called \emph{test theorem}. Second, the test cases are analyzed
       	for ground instances (the \emph{test data}) satisfying the constraints
       	of the test cases. Particular emphasis is put on the control of explicit
       	test hypotheses which can be proven over concrete programs. As such,
       	explicit test hypotheses establish a logical link between validation
       	by test and by proof. Since \testgen generates explicit test hypotheses
       	and makes them amenable to formal proof, the system is in a unique
       	position to explore the relations between them at an example.},
         categories = {holtestgen},
         classification = {workshop},
         file = {brucker.ea-verifying-2008.pdf:http\://www.brucker.ch/bibliography/download/2008/brucker.ea-verifying-2008.pdf:PDF;brucker.ea-verifying-2008.ps.gz:http\://www.brucker.ch/bibliography/download/2008/brucker.ea-verifying-2008.ps.gz:PostScript},
         keywords = {symbolic test case generations, black box testing, theorem proving,
       	formal verification, Isabelle/HOL},
         language = {USenglish},
         owner = {harald},
         public = {yes},
         timestamp = {2009.09.18},
         url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-verifying-2008}
+      }
       @ARTICLE{Bryant1986,
         author = {Randal E. Bryant},
         title = {Graph-based algorithms for Boolean function manipulation},
         journal = {IEEE Trans. Comput.},
         year = {1986},
         volume = {35},
         pages = {677--691},
         number = {8},
         address = {Washington, DC, USA},
         issn = {0018-9340},
         owner = {harald},
         publisher = {IEEE Computer Society},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Budd1985,
         author = {Timothy Alan Budd and Ajei Sarat Gopal},
         title = {Program Testing by Specification Mutation},
         journal = {Computer Languages},
         year = {1985},
         volume = {10},
         pages = {63-73},
         owner = {wkrenn},
         timestamp = {2009.09.17}
+      }
       @ARTICLE{Burdy2005,
         author = {Lilian Burdy and Yoonsik Cheon and David R. Cok and Michael D. Ernst
       	and Joseph R. Kiniry and Gary T. Leavens and K. Rustan M. Leino and
       	Erik Poll},
         title = {An overview of JML tools and applications},
         journal = {STTT},
         year = {2005},
         volume = {7},
         pages = {212-232},
         number = {3},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://dx.doi.org/10.1007/s10009-004-0167-4},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Callahan1996,
         author = {John Callahan and Francis Schneider and Steve Easterbrook},
         title = {Automated {S}oftware {T}esting {U}sing {M}odel-{C}hecking},
         booktitle = {Proceedings 1996 {SPIN} {W}orkshop},
         year = {1996},
         month = {August},
         note = {Also WVU Technical Report NASA-IVV-96-022.},
         owner = {gordon},
         timestamp = {2009.09.18}
+      }
       @TECHREPORT{Campbell,
         author = {Campbell, Colin and Grieskamp, Wolfgang and Nachmanson, Lev and Schulte,
       	Wolfram and Tillmann, Nikolai and Veanes, Margus },
         title = {Model-Based Testing of Object-Oriented Reactive Systems with Spec
       	Explorer},
         abstract = {Testing is one of the costliest aspects of commercial software development.
       	Model-based testing is a promising approach addressing these deficits.
       	At Microsoft, model-based testing technology developed by the Foundations
       	of Software Engineering group in Microsoft Research has been used
       	since 2003. The second generation of this tool set, Spec Explorer,
       	deployed in 2004, is now used on a daily basis by Microsoft product
       	groups for testing operating system components, .NET framework components
       	and other areas. This paper provides a comprehensive survey of the
       	concepts of the tool and their foundations.},
         citeulike-article-id = {2626080},
         keywords = {microsoft, spec, testing},
         owner = {harald},
         posted-at = {2008-04-07 15:41:30},
         priority = {0},
         school = {Microsoft Research},
         timestamp = {2009.09.18},
         url = {ftp://ftp.research.microsoft.com/pub/tr/TR-2005-59.pdf}
+      }
       @INPROCEEDINGS{Cavalcanti2007,
         author = {Cavalcanti, Ana and Gaudel, Marie-Claude},
         title = {Testing for refinement in CSP},
         booktitle = {ICFEM'07: Proceedings of the formal engineering methods 9th international
       	conference on Formal methods and software engineering},
         year = {2007},
         pages = {151--170},
         address = {Berlin, Heidelberg},
         publisher = {Springer-Verlag},
         isbn = {3-540-76648-0, 978-3-540-76648-3},
         location = {Boca Raton, FL, USA}
+      }
       @UNPUBLISHED{Cengarle,
         author = {Maria Victoria Cengarle and Armando Martin Haeberer},
         title = {Towards an epistemology-based methodology for verification and validation
       	testing},
         note = {Technical report, Ludwig-Maximilians-Universit\"at M\"{u}nchen, unpublished
       	draft of March 2, 2000},
         libnum = {195},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Cengarle2000,
         author = {Maria Victoria Cengarle and Armando Martin Haeberer},
         title = {{A formal approach to specification-based black-box testing}},
         booktitle = {{Proceedings of the Workshop on Modelling Software System Structures
       	in a Fastly Moving Scenario, June 13-16, 2000, Santa Margherita Ligure,
       	Italia}},
         year = {2000},
         libnum = {196},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Chen2001,
         author = {H.Y. Chen and T.H. Tse and T.Y. Chen},
         title = {{TACCLE}: a methodology for object-oriented software testing at the
       	class and cluster levels},
         journal = {ACM Transactions on Software Engineering and Methodology},
         year = {2001},
         volume = {10},
         pages = {56--109},
         number = {1},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Cheng1993,
         author = {Kwang-Ting Cheng and A. S. Krishnakumar},
         title = {Automatic Functional Test Generation Using the Extended Finite State
       	Machine Model},
         booktitle = {DAC},
         year = {1993},
         pages = {86-91},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://doi.acm.org/10.1145/157485.164585},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Cheon2008,
         author = {Yoonsik Cheon and Antonio Cortes and Martine Ceberio and Gary T.
       	Leavens},
         title = {Integrating Random Testing with Constraints for Improved Efficiency
       	and Diversity},
         booktitle = {Proceedings of the International Conference on Software Engineering
       	and Knowledge Engineering},
         year = {2008},
         month = {February},
         organization = {Department of Computer Science, The University of Texas at El Paso},
         note = {to appear},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Cimatti1999,
         author = {Alessandro Cimatti and Edmund M. Clarke and Fausto Giunchiglia and
       	Marco Roveri},
         title = {N{USMV}: {A} {N}ew {S}ymbolic {M}odel {V}erifier},
         booktitle = {C{AV} '99: {P}roceedings of the 11th {I}nternational {C}onference
       	on {C}omputer {A}ided {V}erification},
         year = {1999},
         pages = {495--499},
         address = {London, UK},
         publisher = {Springer-Verlag},
         isbn = {3-540-66202-2},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Claessen2002,
         author = {Koen Claessen and John Hughes},
         title = {Testing monadic code with QuickCheck},
         journal = {SIGPLAN Notices},
         year = {2002},
         volume = {37},
         pages = {47-59},
         number = {12},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://doi.acm.org/10.1145/636517.636527},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Claessen2000,
         author = {Koen Claessen and John Hughes},
         title = {QuickCheck: a lightweight tool for random testing of Haskell programs},
         booktitle = {ICFP},
         year = {2000},
         pages = {268-279},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://doi.acm.org/10.1145/351240.351266},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Claessen2000a,
         author = {K. Claessen and J. Hughes},
         title = {{Quickcheck}: a lightweight tool for random testing of {Haskell}
       	programs},
         booktitle = {Fifth ACM SIGPLAN International Conference on Functional Programming},
         year = {2000},
         pages = {268--279},
         publisher = {ACM Press},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Clarke2000,
         author = {Clarke, Edmund and Grumberg, Orna and Jha, Somesh and Lu, Yuan and
       	Veith, Helmut},
         title = {Counterexample-Guided Abstraction Refinement},
         booktitle = {Computer Aided Verification, 12th International Conference},
         year = {2000},
         pages = {154--169},
         journal = {Computer Aided Verification},
         owner = {wkrenn},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/10.1007/10722167_15}
+      }
       @INPROCEEDINGS{Clarke2004,
         author = { Clarke, Edmund and Kroening, Daniel and Lerda, Flavio },
         title = { A Tool for Checking {ANSI-C} Programs },
         booktitle = { Tools and Algorithms for the Construction and Analysis of Systems
       	(TACAS 2004) },
         year = { 2004 },
         editor = { Kurt Jensen and Andreas Podelski },
         volume = { 2988 },
         series = { Lecture Notes in Computer Science },
         pages = { 168--176 },
         publisher = { Springer },
         isbn = { 3-540-21299-X },
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Clarke1982,
         author = {Edmund M. Clarke and E. Allen Emerson},
         title = {Design and Synthesis of Synchronization Skeletons Using Branching-Time
       	Temporal Logic},
         booktitle = {Logic of Programs, Workshop},
         year = {1982},
         pages = {52--71},
         address = {London, UK},
         publisher = {Springer-Verlag},
         isbn = {3-540-11212-X},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Clarke1976,
         author = {Clarke, L. A. },
         title = {A System to Generate Test Data and Symbolically Execute Programs},
         journal = {IEEE Transactions on Software Engineering},
         year = {1976},
         volume = {2},
         pages = {215--222},
         number = {3},
         abstract = {This paper describes a system that attempts to generate test data
       	for programs written in ANSI Fortran. Given a path, the system symbolically
       	executes the path and creates a set of constraints on the program's
       	input variables. If the set of constraints is linear, linear pro-
       	gramming techniques are employed to obtain a solution. A solution
       	to the set of constraints is test data that will drive execution
       	down the given path. If it can be determined that the set of constraints
       	is incon- sistent, then the given path is shown to be nonexecutable.
       	To increase the chance of detecting some of the more common programming
       	errors, artificial constraints are temporarily created that simulate
       	error condi- tions and then an attempt is made to solve each augmented
       	set of constraints. A symbolic representation of the program's output
       	vari- ables in terms of the program's input variables is also created.
       	The symbolic representation is in a human readable form that facilitates
       	error detection as weUl as being a possible aid in assertion generation
       	and automatic program documentation.},
         address = {Los Alamitos, CA, USA},
         citeulike-article-id = {2638013},
         doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.1976.233817},
         keywords = {bibtex-import, execution, generationsymbolic, test, vector},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/01702368.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:45},
         priority = {2},
         publisher = {IEEE Computer Society},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/http://doi.ieeecomputersociety.org/10.1109/TSE.1976.233817}
+      }
       @ARTICLE{Clarke1989,
         author = {L. A. Clarke and A. Podgurski and D. J. Richardson and S. J. Zeil},
         title = {A Formal Evaluation of Data Flow Path Selection Criteria},
         journal = {IEEE Trans. Softw. Eng.},
         year = {1989},
         volume = {15},
         pages = {1318--1332},
         number = {11},
         address = {Piscataway, NJ, USA},
         doi = {http://dx.doi.org/10.1109/32.41326},
         issn = {0098-5589},
         owner = {harald},
         publisher = {IEEE Press},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Cleaveland1991,
         author = {R. Cleaveland and A. E. Zwarico},
         title = {A Theory of Testing for Real-Time},
         booktitle = {Proc.\ of the Sixth Annual IEEE Symposium on Logic in Computer Science},
         year = {1991},
         pages = {110-119},
         address = {Amsterdam, The Netherlands},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Craggs2003,
         author = {Ian Craggs and Manolis Sardis and Thierry Heuillard},
         title = {AGEDIS Case Studies: Model-Based Testing in Industry},
         booktitle = {Proceedings of the 1st European Conference on Model Driven Software
       	Engineering},
         year = {2003},
         pages = {106--117},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{D'Silva2008,
         author = {D'Silva, Vijay and Kroening, Daniel and Weissenbacher, Georg },
         title = {A Survey of Automated Techniques for Formal Software Verification},
         journal = {A Survey of Automated Techniques for Formal Software Verification},
         year = {2008},
         abstract = {<p>The quality and the correctness of software is often the greatest
       	<br />concern in electronic systems. Formal verification tools can
       	provide a<br />guarantee that a design is free of specific flaws.
       	This paper surveys<br />algorithms that perform automatic, static
       	analysis of software to detect<br />programming errors or prove their
       	absence. The three techniques considered<br />are static analysis
       	with abstract domains, model checking, and bounded model<br />checking.
       	A short tutorial on these techniques is provided, highlighting<br
       	/>their differences when applied to practical problems. The paper
       	also surveys<br />the tools that are available implementing these
       	techniques, and describes<br />their merits and shortcomings.</p>},
         citeulike-article-id = {2762806},
         keywords = {mogentes},
         owner = {harald},
         posted-at = {2008-05-06 21:09:47},
         priority = {2},
         publisher = {IEEE},
         timestamp = {2009.09.18},
         url = {http://www.kroening.com/publications/view-publications-dkw2008.html}
+      }
       @INPROCEEDINGS{Dan2004,
         author = {Li Dan and Bernhard K. Aichernig},
         title = {Combining Algebraic and Model-based Test Case Generation},
         booktitle = {Proceedings of First International Colloquium on Theoretical Aspects
       	of Computing, Guiyang, China 20-24 September 2004},
         year = {2004},
         volume = {3407},
         series = {Lecture Notes in Computer Science},
         pages = {250--264},
         publisher = {Springer-Verlag},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Dang2008,
         author = {Dang, Thao and Nahhal, Tarik},
         title = {Using Disparity to Enhance Test Generation for Hybrid Systems},
         booktitle = {TestCom '08 / FATES '08: Proceedings of the 20th IFIP TC 6/WG 6.1
       	international conference on Testing of Software and Communicating
       	Systems},
         year = {2008},
         pages = {54--69},
         address = {Berlin, Heidelberg},
         publisher = {Springer-Verlag},
         doi = {http://dx.doi.org/10.1007/978-3-540-68524-1_6},
         isbn = {978-3-540-68514-2},
         location = {Tokyo, Japan}
+      }
       @ARTICLE{Dauchy1993,
         author = {Pierre Dauchy and Marie-Claude Gaudel and Bruno Marre},
         title = {Using algebraic specifications in software testing: A case study
       	on the software of an automatic subway},
         journal = {Journal of Systems and Software},
         year = {1993},
         volume = {21},
         pages = {229-244},
         number = {3},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://dx.doi.org/10.1016/0164-1212(93)90025-S},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Daws1995,
         author = {Conrado Daws and Alfredo Olivero and Sergio Yovine},
         title = {Verifying ET-LOTOS programmes with KRONOS},
         booktitle = {Proceedings of the 7th IFIP WG6.1 International Conference on Formal
       	Description Techniques VII},
         year = {1995},
         pages = {227--242},
         address = {London, UK, UK},
         publisher = {Chapman \& Hall, Ltd.},
         isbn = {0-412-64450-9},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{DeJong2004,
         author = {De Jong, Hidde},
         title = {Qualitative simulation and related approaches for the analysis of
       	dynamic systems},
         journal = {Knowl. Eng. Rev.},
         year = {2004},
         volume = {19},
         pages = {93--132},
         number = {2},
         address = {New York, NY, USA},
         doi = {http://dx.doi.org/10.1017/S0269888904000177},
         issn = {0269-8889},
         publisher = {Cambridge University Press}
+      }
       @ARTICLE{DeMillo1978,
         author = {Richard A. DeMillo and Richard J. Lipton and Frederick G. Sayward},
         title = {Hints on {T}est {D}ata {S}election: {H}elp for the {P}racticing {P}rogrammer},
         journal = {Computer},
         year = {1978},
         volume = {11},
         pages = {34-41},
         owner = {gordon},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Derksen2007,
         author = {Derksen, Roger and van der Wouden, Huub and Heath, Paul},
         title = {Testing The Heathrow Terminal 5 Baggage Handling System - Before
       	It Is Built},
         year = {2007},
         month = {November},
         abstract = {London Heathrow Terminal 5 will open in March 2008. This new core
       	terminal building and two satellites will handle 30 million passengers
       	a year, and all of these passengers will expect their baggage to
       	accompany them on their flights. To achieve this, a new baggage handling
       	system is being constructed that will handle more than 70,000 bags
       	a day. Maintaining customer confidence in the reliability of the
       	baggage handling system is vital to the successful delivery of the
       	project. The challenge for the baggage control system designers was
       	how best to integrate and test the software systems of such a large
       	and complex system within a limited time to test the software in
       	its actual site environment. This article explains the vital role
       	that software emulation testing techniques played in factory integration
       	testing. The advantages and limitations of these techniques are covered
       	along with explanations of what can (and cannot) be achieved in the
       	factory environment.},
         citeulike-article-id = {2802474},
         keywords = {mogentes, testing},
         owner = {harald},
         posted-at = {2008-05-15 19:54:12},
         priority = {3},
         timestamp = {2009.09.18}
+      }
       @BOOK{DeRoever1999,
         title = {Data Refinement: Model-Oriented Proof Methods and Their Comparison},
         publisher = {Cambridge University Press},
         year = {1999},
         author = {DeRoever,, W. and Engelhardt,, Kai},
         address = {New York, NY, USA},
         isbn = {0521641705},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Dick1993a,
         author = {Jeremy Dick and Alain Faivre},
         title = {Automating the Generation and Sequencing of Test Cases from Model-Based
       	Specifications},
         booktitle = {Proceedings of FME'93: Industrial-Strength Formal Methods, International
       	Symposium of Formal Methods Europe, April 1993, Odense, Denmark},
         year = {1993},
         editor = {J.C.P. Woodcock and P.G. Larsen},
         pages = {268--284},
         month = {April},
         publisher = {Springer-Verlag},
         libnum = {7},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Dick1993,
         author = {Dick, Jeremy and Faivre, Alain },
         title = {Automating the Generation and Sequencing of Test Cases from Model-Based
       	Specifications},
         booktitle = {FME '93: Proceedings of the First International Symposium of Formal
       	Methods Europe on Industrial-Strength Formal Methods},
         year = {1993},
         pages = {268--284},
         address = {London, UK},
         publisher = {Springer-Verlag},
         citeulike-article-id = {2649305},
         isbn = {3540566627},
         keywords = {model, mogentes, testing},
         owner = {harald},
         posted-at = {2008-04-10 14:43:12},
         priority = {2},
         timestamp = {2009.09.18},
         url = {http://portal.acm.org/citation.cfm?id=647535.729387}
+      }
       @BOOK{Dijkstra1990,
         title = {Predicate Calculus and Program Semantics},
         publisher = {Springer-Verlag},
         year = {1990},
         author = {E.W. Dijkstra and C.S. Scholten},
         series = {Texts and Monographs in Computer Science},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Dill1990,
         author = {D. L. Dill},
         title = {Timing assumptions and verification of finite-state concurrent systems},
         booktitle = {Proceedings of the international workshop on Automatic verification
       	methods for finite state systems},
         year = {1990},
         pages = {197--212},
         address = {New York, NY, USA},
         publisher = {Springer-Verlag New York, Inc.},
         isbn = {0-387-52148-8},
         location = {Grenoble, France},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Dong1994,
         author = {R.K. Dong and Ph.G. Frankl},
         title = {The {ASTOOT} approach to testing object-oriented programs},
         journal = {ACM Transactions on Software Engineering and Methodology},
         year = {1994},
         volume = {3},
         pages = {103--130},
         number = {2},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Dowson1997,
         author = {Mark Dowson},
         title = {{The ARIANE 5 Software Failure}},
         journal = {{ACM SIGSOFT Software Engineering Notes}},
         year = {1997},
         volume = {22},
         pages = {84},
         number = {2},
         address = {New York, NY, USA},
         file = {:home/elisabeth/Diplomarbeit/Literatur/PDFs/ariane5.pdf:PDF},
         issn = {0163-5948},
         publisher = {ACM},
         url = {http://portal.acm.org/citation.cfm?id=251992}
+      }
       @INPROCEEDINGS{Durrieu2004,
         author = {Guy Durrieu and Odile Laurent and Christel Seguin and Virginie Wiels},
         title = {Formal Proof and Test Case Generation for Critical Embedded Systems
       	Using Scade},
         booktitle = {Building the Information Society, IFIP 18th World Computer Congress},
         year = {2004},
         editor = {Ren{\'e} Jacquart},
         volume = {156/2004},
         series = {IFIP International Federation for Information Processing},
         pages = {499--504},
         publisher = {Springer Boston},
         doi = {10.1007/978-1-4020-8157-6_44},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @MISC{Dutertre2006,
         author = {Dutertre, B. and de Moura, L.},
         title = {The Yices SMT solver},
         howpublished = {Tool paper at http://yices.csl.sri.com/tool-paper.pdf},
         month = {August},
         year = {2006},
         citeulike-article-id = {2639925},
         keywords = {sat-solvers},
         organization = {SRI International},
         posted-at = {2008-04-08 04:25:43},
         priority = {2}
+      }
       @INPROCEEDINGS{Emerson1982,
         author = {E. Allen Emerson and Joseph Y. Halpern},
         title = {Decision procedures and expressiveness in the temporal logic of branching
       	time},
         booktitle = {STOC '82: Proceedings of the fourteenth annual ACM symposium on Theory
       	of computing},
         year = {1982},
         pages = {169--180},
         address = {New York, NY, USA},
         publisher = {ACM Press},
         doi = {10.1145/800070.802190},
         isbn = {0-89791-070-2},
         location = {San Francisco, California, United States},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Emerson1987,
         author = {E. Allen Emerson and Chin-Laung Lei},
         title = {Modalities for model checking: branching time logic strikes back},
         journal = {Sci. Comput. Program.},
         year = {1987},
         volume = {8},
         pages = {275--306},
         number = {3},
         address = {Amsterdam, The Netherlands, The Netherlands},
         doi = {http://dx.doi.org/10.1016/0167-6423(87)90036-0},
         issn = {0167-6423},
         owner = {harald},
         publisher = {Elsevier North-Holland, Inc.},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Engels1997,
         author = {Andr\'{e} Engels and Loe Feijs and Sjouke Mauw},
         title = {Test Generation for Intelligent Networks Using ModelChecking},
         booktitle = {Proceedings of the Third International Workshop on Tools and Algorithms
       	for the Construction and Analysis of Systems. (TACAS'97)},
         year = {1997},
         editor = {Ed Brinksma},
         volume = {1217},
         series = {Lecture Notes in Computer Science},
         address = {Enschede, the Netherlands},
         month = {April},
         publisher = {Springer-Verlag},
         optnote = {personal copy in Test 1},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Esposito2004,
         author = {Esposito, J.M.},
         title = {Randomized test case generation for hybrid systems: metric selection},
         journal = {System Theory, 2004. Proceedings of the Thirty-Sixth Southeastern
       	Symposium on System Theory},
         year = {2004},
         pages = {236-240},
         doi = {10.1109/SSST.2004.1295655},
         keywords = {computational complexity, control system analysis, path planning,
       	randomised algorithms, reachability analysis control systems, hybrid
       	state space, hybrid systems, metric selection, randomized approach,
       	robotic path planning, test case generation},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @MISC{Farquhar1993,
         author = {Adam Farquhar and Benjamin Kuipers and Jeff Rickel and David Throop
       	and The Qualitative Reasoning Group},
         title = {{QSIM}: The Program and its Use},
         month = {July},
         year = {1993},
         owner = {harald},
         timestamp = {2010.08.11}
+      }
       @INPROCEEDINGS{Floyd1967,
         author = {Robert W. Floyd},
         title = {Assigning meanings to programs},
         booktitle = {{P}roc. {A}mer. {M}ath. {S}oc. {S}ymposia in {A}pplied {M}athematics},
         year = {1967},
         volume = {19},
         pages = {19--32},
         publisher = {Amer. Math. Soc.},
         owner = {harald},
         timestamp = {2009.09.18},
         url = {http://www.ams.org/mathscinet-getitem?mr=235771}
+      }
       @ARTICLE{Forbus1984,
         author = {Kenneth D. Forbus},
         title = {Qualitative Process Theory},
         journal = {Artif. Intell.},
         year = {1984},
         volume = {24},
         pages = {85-168},
         number = {1-3},
         bibsource = {DBLP, http://dblp.uni-trier.de}
+      }
       @INPROCEEDINGS{Foster2007,
         author = {Howard Foster and Wolfgang Emmerich and Jeff Kramer and Jeff Magee
       	and David S. Rosenblum and Sebasti{\'a}n Uchitel},
         title = {Model Checking Service Compositions under Resource Constraints},
         booktitle = {Proceedings of the 6th joint meeting of the European Software Engineering
       	Conference and the ACM SIGSOFT International Symposium on Foundations
       	of Software Engineering ({ESEC/SIGSOFT FSE})},
         year = {2007},
         editor = {Ivica Crnkovic and Antonia Bertolino},
         pages = {225--234},
         publisher = {ACM},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Frantzen2006,
         author = {Lars Frantzen and Jan Tretmans and Tim A. C. Willemse},
         title = {A Symbolic Framework for Model-Based Testing},
         booktitle = {1st Combined International Workshops on Formal Approaches to Software
       	Testing and Runtime Verification},
         year = {2006},
         volume = {4262},
         series = {LNCS},
         pages = {40--54},
         publisher = {Springer},
         comment = {p,r},
         ee = {http://dx.doi.org/10.1007/11940197_3},
         file = {frantzen2006symbolic.pdf:frantzen2006symbolic.pdf:PDF},
         owner = {martin},
         timestamp = {2007.10.24}
+      }
       @ARTICLE{Fraser2007a,
         author = {Fraser, Gordon and Aichernig, Bernhard K. and Wotawa, Franz },
         title = {Handling Model Changes: Regression Testing and Test-Suite Update
       	with Model-Checkers},
         journal = {Electronic Notes in Theoretical Computer Science},
         year = {2007},
         volume = {190},
         pages = {33--46},
         number = {2},
         abstract = {Several model-checker based methods to automated test-case generation
       	have been proposed recently. The performance and applicability largely
       	depends on the complexity of the model in use. For complex models,
       	the costs of creating a full test-suite can be significant. If the
       	model is changed, then in general the test-suite is completely regenerated.
       	However, only a subset of a test-suite might be invalidated by a
       	model change. Creating a full test-suite in such a case would therefore
       	waste time by unnecessarily recreating valid test-cases. This paper
       	investigates methods to reduce the effort of recreating test-suites
       	after a model is changed. This is also related to regression testing,
       	where the number of test-cases necessary after a change should be
       	minimized. This paper presents and evaluates methods to identify
       	obsolete test-cases, and to extend any given test-case generation
       	approach based on model-checkers in order to create test-cases for
       	test-suite update or regression testing.},
         citeulike-article-id = {2637990},
         keywords = {automated, bibtex-import, change, generation, model, model-checkers,
       	regression, test-case, testing, test-suite, tug, update, with},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/mbt07.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:41},
         priority = {2},
         timestamp = {2009.09.18},
         url = {http://www.sciencedirect.com/science/article/B75H1-4PHSRDB-4/2/320e4bc91ad12d87ea9ded2f18cc69f9}
+      }
       @INPROCEEDINGS{Fraser2008b,
         author = {Gordon Fraser and Martin Weiglhofer and Franz Wotawa},
         title = {Using Observer Automata to Select Test Cases for Test Purposes},
         booktitle = {Proceedings of the 20th International Conference on Software Engineering
       	and Knowledge Engineering},
         year = {2008},
         note = {to appear},
         comment = {a},
         file = {fraser2008using.pdf:fraser2008using.pdf:PDF},
         owner = {martin},
         timestamp = {2008.05.20}
+      }
       @INPROCEEDINGS{Fraser2008c,
         author = {Gordon Fraser and Martin Weiglhofer and Franz Wotawa},
         title = {Coverage Based Testing with Test Purposes},
         booktitle = {Proceedings of the 8th International Conference on Quality Software},
         year = {2008},
         note = {to appear},
         comment = {a},
         owner = {martin},
         timestamp = {2008.05.20}
+      }
       @INPROCEEDINGS{Fraser2007,
         author = {Fraser, Gordon and Wotawa, Franz},
         title = {Test-Case Generation and Coverage Analysis for Nondeterministic Systems
       	Using Model-Checkers},
         booktitle = {ICSEA '07: Proceedings of the International Conference on Software
       	Engineering Advances},
         year = {2007},
         pages = {45},
         address = {Washington, DC, USA},
         publisher = {IEEE Computer Society},
         doi = {http://dx.doi.org/10.1109/ICSEA.2007.71},
         isbn = {0-7695-2937-2},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Fraser2008,
         author = {Gordon Fraser and Franz Wotawa and Paul E. Ammann},
         title = {Testing with model checkers: a survey},
         journal = {Software Testing, Verification and Reliability},
         year = {2008},
         month = {December},
         note = {accepted for publication},
         doi = {10.1002/stvr.402},
         owner = {martin},
         timestamp = {2009.05.15}
+      }
       @INPROCEEDINGS{Friedman2002,
         author = {G. Friedman and A. Hartman and K. Nagin and T. Shiran},
         title = {Projected state machine coverage for software testing},
         booktitle = {ISSTA},
         year = {2002},
         pages = {134-143},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://doi.acm.org/10.1145/566172.566192},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Futatsugi1995,
         author = {K.~Futatsugi and J.A.~Goguen and J.P.~Jouannaud and J.~Meseguer},
         title = {Principles of {OBJ2}},
         booktitle = {Proceedings of the 12th ACM Symposium on Principles of Programming
       	Languages, New Orleans},
         year = {1995},
         pages = {52--66},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{Gotz2009,
         title = {iX Studie Modellbasiertes Testen},
         publisher = {Heise Verlag},
         year = {2009},
         author = {Helmut G"{o}tz and Markus Nickolaus and Thomas Ro"sner and Knut Salomon},
         owner = {wkrenn},
         timestamp = {2009.09.17}
+      }
       @TECHREPORT{Galler2008a,
         author = {Galler, Stefan J. and K\"{o}nigshofer, Robert and Peischl, Bernhard
       	and Unterberger, Robert and Wotawa, Franz },
         title = {Automatic Test Generation Tools for Java based on Design-by-Contract(tm):
       	A survey},
         institution = {Competence Networt Softnet Austria},
         year = {2008},
         month = {May},
         abstract = {Since testing counts for more than 40\% of total cost of software
       	development, automating the software testing process becomes more
       	and more important. Therefore, a more formal specification of the
       	expected behavior of software components is necessary. The Eiffel
       	programming language is the first programming language with built-in
       	formal specification of method pre-conditions, post-conditions and
       	class invariants, called Design-by-Contract. This technical report
       	should give an overview of currently available Design-by-Contract
       	specification languages for Java. The focus here is on the practical
       	usability of those languages in an real-world industrial project.},
         citeulike-article-id = {2805308},
         keywords = {java, mogentes, testing},
         owner = {harald},
         posted-at = {2008-05-16 14:59:10},
         priority = {2},
         timestamp = {2009.09.18}
+      }
       @TECHREPORT{Galler2008,
         author = {Galler, Stefan J. and Peischl, Bernhard and Wotawa, Franz},
         title = {Formal Specification Languages for Design-by-Contract in Java: A
       	survey},
         institution = {Competence Network Softnet Austria},
         year = {2008},
         key = {SNA-TR-2007-1P3},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Gannon1981,
         author = {John Gannon and Paul McMullin and Richard Hamlet},
         title = {Data abstraction implementation, specification and testing},
         journal = {ACM Transactions on Programming Languages and Systems},
         year = {1981},
         volume = {3},
         pages = {211--223},
         number = {3},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Garavel2002,
         author = {Hubert Garavel and Fr{\'e}d{\'e}ric Lang and Radu Mateescu},
         title = {An overview of {CADP} 2001},
         journal = {European Association for Software Science and Technology Newsletter},
         year = {2002},
         volume = {4},
         pages = {13-24},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{697560,
         author = {Gaudel, Marie-Claude},
         title = {Testing Can Be Formal, Too},
         booktitle = {TAPSOFT '95: Proceedings of the 6th International Joint Conference
       	CAAP/FASE on Theory and Practice of Software Development},
         year = {1995},
         pages = {82--96},
         address = {London, UK},
         publisher = {Springer-Verlag},
         isbn = {3-540-59293-8}
+      }
       @INPROCEEDINGS{Gaudel1995,
         author = {Marie-Claude Gaudel},
         title = {Testing can be formal too},
         booktitle = {TAPSOFT'95: Theory and Practice of Software Development, 6th International
       	Joint Conference CAAP/FASE},
         year = {1995},
         volume = {915},
         series = {Lecture Notes in Computer Science},
         pages = {82--96},
         month = {May},
         publisher = {Springer-Verlag},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Gaudel2008,
         author = {Marie-Claude Gaudel and Pascale Le Gall},
         title = {Testing Data Types Implementations from Algebraic Specifications},
         booktitle = {Formal Methods and Testing 2008},
         year = {2008},
         editor = {Robert M. Hierons and Jonathan P. Bowen and Mark Harman},
         volume = {4949},
         series = {LNCS},
         pages = {209--239},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Gaudel1998,
         author = {Marie-Claude Gaudel and Perry R.~James},
         title = {Testing Algebraic Data Types and Processes: a Unifying Theory},
         journal = {Formal Aspects of Computing},
         year = {1998},
         volume = {10},
         pages = {436--451},
         number = {5 \& 6},
         libnum = {140},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{Glymour1980,
         title = {Theory and Evidence},
         publisher = {Princeton University Press},
         year = {1980},
         author = {Clarke Glymour},
         address = {New Jersey},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Glymour1980a,
         author = {Clarke Glymour},
         title = {Hypothetico-deductivism is hopeless},
         journal = {Philosophy of science},
         year = {1980},
         volume = {47},
         pages = {322--325},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Gnesi2004,
         author = {Gnesi, Stefania and Latella, Diego and Massink, Mieke},
         title = {Formal Test-Case Generation for {UML} Statecharts},
         booktitle = {ICECCS '04: Proc. of the 9th IEEE Int. Conf. on Engineering Complex
       	Computer Systems Navigating Complexity in the e-Engineering Age},
         year = {2004},
         pages = {75--84},
         publisher = {IEEE Computer Society}
+      }
       @TECHREPORT{Godefroid2007,
         author = {Godefroid, Patrice and Levin, Michael and Molnar, David },
         title = {Automated Whitebox Fuzz Testing},
         institution = {Microsoft Research},
         year = {2007},
         number = {MSR-TR-2007-58},
         month = {May},
         abstract = {{\\em Fuzz testing} is an effective technique for finding security
       	vulnerabilities in software. Traditionally, fuzz testing tools apply
       	random mutations to well-formed inputs and test the program on the
       	resulting values. We present an alternative {\\em whitebox fuzz testing}
       	approach inspired by recent advances in symbolic execution and dynamic
       	test generation. Our approach records an actual run of a program
       	under test on a well-formed input, symbolically evaluates the recorded
       	trace, and generates constraints capturing how the program uses its
       	inputs. The generated constraints are used to produce new inputs
       	which cause the program to follow different control paths. This process
       	is repeated with the help of a code-coverage maximizing heuristic
       	designed to find defects as fast as possible. We have implemented
       	this algorithm in SAGE (\\emph{Scalable, Automated, Guided Execution}),
       	a new tool employing x86 instruction-level tracing and emulation
       	for whitebox fuzzing of arbitrary file-reading Windows applications.
       	We describe key optimizations needed to make dynamic test generation
       	scale to large input files and long execution traces with hundreds
       	of millions of instructions. We then present detailed experiments
       	with several Windows applications. Notably, without any format-specific
       	knowledge, SAGE detects the MS07-017 ANI vulnerability, which was
       	missed by extensive blackbox fuzzing and static analysis tools. Furthermore,
       	while still in an early stage of development, SAGE has already discovered
 + new bugs in large shipped Windows applications including image
       	processors, media players, and file decoders. Several of these bugs
       	are potentially exploitable memory access violations.},
         citeulike-article-id = {2284715},
         keywords = {bibtex-import},
         owner = {harald},
         posted-at = {2008-01-24 13:13:45},
         priority = {0},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Gotlieb1998,
         author = {Gotlieb, Arnaud and Botella, Bernard and Rueher, Michel },
         title = {Automatic test data generation using constraint solving techniques},
         journal = {SIGSOFT Softw. Eng. Notes},
         year = {1998},
         volume = {23},
         pages = {53--62},
         number = {2},
         abstract = {Automatic test data generation leads to identify input values on which
       	a selected point in a procedure is ex- ecuted. This paper introduces
       	a new method for this problem based on constraint solving techniques.
       	First, we statically transform a procedure into a constraint system
       	by using well-known "Static Single Assignment" form and control-dependencies.
       	Second, we solve this system to check whether at least one feasible
       	control flow path going through the selected point exists and to
       	generate test data that correspond to one of these paths. The key
       	point of our approach is to take advantage of current advances in
       	constraint techniques when solving the generated constraint system.
       	Global constraints are used in a preliminary step to detect some
       	of the non fea- sible paths. Partial consistency techniques are employed
       	to reduce the domains of possible values of the test data. A prototype
       	implementation has been developped on a restricted subset of the
       	C language. Advantages of our approach are illustrated on a non-trivial
       	example.},
         address = {New York, NY, USA},
         citeulike-article-id = {2638008},
         doi = {http://doi.acm.org/10.1145/271775.271790},
         keywords = {bibtex-import, execution, generation, symbolic, test, vector},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/p53-gotlieb.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:44},
         priority = {2},
         publisher = {ACM},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/10.1145/271775.271790}
+      }
       @TECHREPORT{Grabowski1999,
         author = {Jens Grabowski and Dieter Hogrefe},
         title = {{The Standardization of Core INAP CS-2 by ETSI}},
         institution = {Technical Report A-99-02, Medical University of L\"{u}beck, Schriftenreihe
       	der Institute f\"{u}r Mathematik/Informatik, L\"{u}beck, February
 },
         year = {1999},
         month = feb,
         keywords = {SDL, MSC, TTCN, ASN.1, conformance testing, automatic test generation,
       	standardization, ETSI, ITU-T},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Grieskamp2010,
         author = {Wolfgang Grieskamp and Nicolas Kicillof and Keith Stobie and Victor
       	Braberman},
         title = {Model-based quality assurance of protocol documentation: tools and
       	methodology},
         journal = {Software Testing, Verification and Reliability (STVR)},
         year = {2010},
         owner = {harald},
         timestamp = {2011.01.11}
+      }
       @ARTICLE{Grieskamp2006,
         author = {Wolfgang Grieskamp and Nicolas Kicillof and Nikolai Tillmann},
         title = {Action Machines: a Framework for Encoding and Composing Partial Behaviors},
         journal = {International Journal of Software Engineering and Knowledge Engineering},
         year = {2006},
         volume = {16},
         pages = {705-726},
         number = {5},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://dx.doi.org/10.1142/S0218194006002963},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Griesmayer2009,
         author = {Andreas Griesmayer and Bernhard K. Aichernig and Einar Broch Johnsen
       	and Rudolf Schlatte},
         title = {Dynamic Symbolic Execution for Testing Distributed Objects},
         booktitle = {TAP},
         year = {2009},
         pages = {105-120},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://dx.doi.org/10.1007/978-3-642-02949-3_9}
+      }
       @BOOK{Group1992,
         title = {The RAISE Specification Language},
         publisher = {Prentice-Hall},
         year = {1992},
         author = {The RAISE Language Group},
         series = {The BCS Practitioners Series},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{Group1995,
         title = {The RAISE Development Method},
         publisher = {Prentice-Hall},
         year = {1995},
         author = {The RAISE Method Group},
         series = {The BCS Practitioners Series},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Gupta2000,
         author = {Gupta, N. and Mathur, A. P. and Soffa, M. L. },
         title = {Generating test data for branch coverage},
         journal = {Automated Software Engineering, 2000. Proceedings ASE 2000. The Fifteenth
       	IEEE International Conference on},
         year = {2000},
         pages = {219--227},
         abstract = {Branch coverage is an important criteria used during the structural
       	testing of programs. In this paper, we present a new program execution
       	based approach to generate input data that exercises a selected branch
       	in a program. The test data generation is initiated with an arbitrarily
       	chosen input from the input domain of the program. A new input is
       	derived from the initial input in an attempt to force execution through
       	any of the paths through the selected branch. The method dynamically
       	switches among the paths that reach the branch by refining the input.
       	Using a numerical iterative technique that attempts to generate an
       	input to exercise the branch, it dynamically selects Q path that
       	offers less resistance. We have implemented the technique and present
       	experimental results of its performance for some programs. Our results
       	show that our method is feasible and practical.},
         citeulike-article-id = {2638009},
         doi = {10.1109/ASE.2000.873666},
         keywords = {bibtex-import, branch, coverage, generation, program, structural,
       	test, testing, vector},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/00873666.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:44},
         priority = {2},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/10.1109/ASE.2000.873666}
+      }
       @ARTICLE{Gupta1998,
         author = {Gupta, Neelam and Mathur, Aditya P. and Soffa, Mary L. },
         title = {Automated test data generation using an iterative relaxation method},
         journal = {SIGSOFT Softw. Eng. Notes},
         year = {1998},
         volume = {23},
         pages = {231--244},
         number = {6},
         abstract = {An important problem that arises in path oriented testing is the generation
       	of test data that causes a program to follow a given path. In this
       	paper, we present a novel program execution based approach using
       	an iterative relaxation method to address the above problem. In this
       	method, test data generation is initiated with an arbitrarily chosen
       	input from a given domain. This input is then iteratively refined
       	to obtain an input on which all the branch predicates on the given
       	path evaluate to the desired outcome. In each iteration the program
       	statements relevant to the evaluation of each branch predicate on
       	the path are executed, and a set of linear constraints is derived.
       	The constraints are then solved to obtain the increments for the
       	input. These increments are added to the current input to obtain
       	the input for the next iteration. The relaxation technique used in
       	deriving the constraints provides feedback on the amount by which
       	each input variable should be adjusted for the branches on the path
       	to evaluate to the desired outcome.When the branch conditions on
       	a path are linear functions of input variables, our technique either
       	finds a solution for such paths in one iteration or it guarantees
       	that the path is infeasible. In contrast, existing execution based
       	approaches may require an unacceptably large number of iterations
       	for relatively long paths because they consider only one input variable
       	and one branch predicate at a time and use backtracking. When the
       	branch conditions on a path are nonlinear functions of input variables,
       	though it may take more then one iteration to derive a desired input,
       	the set of constraints to be solved in each iteration is linear and
       	is solved using Gaussian elimination. This makes our technique practical
       	and suitable for automation.},
         address = {New York, NY, USA},
         citeulike-article-id = {2638001},
         doi = {http://doi.acm.org/10.1145/291252.288321},
         keywords = {bibtex-import},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/p231-gupta.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:43},
         priority = {2},
         publisher = {ACM},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/10.1145/291252.288321}
+      }
       @ARTICLE{Gurevich2000,
         author = {Yuri Gurevich},
         title = {Sequential abstract-state machines capture sequential algorithms},
         journal = {ACM Trans. Comput. Logic},
         year = {2000},
         volume = {1},
         pages = {77--111},
         number = {1},
         address = {New York, NY, USA},
         doi = {http://doi.acm.org/10.1145/343369.343384},
         issn = {1529-3785},
         owner = {harald},
         publisher = {ACM},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Guttag1977,
         author = {J.~Guttag},
         title = {Abstract Data Types and the Development of Data Structures},
         journal = {Communications of the ACM},
         year = {1977},
         volume = {20},
         pages = {369--405},
         number = {6},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Guttag1985,
         author = {J.V.~Guttag and J.J.~Horning and J.M.~Wing},
         title = {The {Larch} family of specification languages},
         journal = {IEEE Software},
         year = {1985},
         volume = {2},
         pages = {24--36},
         number = {5},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{Guttag1993,
         title = {{Larch}: Languages and Tools for Formal Specification},
         publisher = {Springer Verlag},
         year = {1993},
         author = {John V.~Guttag and James J.~Horning},
         series = {Texts and Monographs in Computer Science},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Haeberer2001,
         author = {A. M. Haeberer and T. S. E. Maibaum},
         title = {{Scientific rigour, an answer to a pragmatic question: a linguistic
       	framework for software engineering}},
         booktitle = {Proceedings of the 23rd International Conference on Software engineering,
       	Toronto, Ontario, Canada},
         year = {2001},
         pages = {463--472},
         publisher = {IEEE Computer Society},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Halbwachs1991,
         author = {N. Halbwachs and P. Caspi and P. Raymond and D. Pilaud},
         title = {The synchronous data-flow programming language {LUSTRE}},
         journal = {Proceedings of the IEEE},
         year = {1991},
         volume = {79},
         pages = {1305--1320},
         number = {9},
         month = {September},
         owner = {harald},
         timestamp = {2009.09.18},
         url = {citeseer.ist.psu.edu/halbwachs91synchronous.html}
+      }
       @ARTICLE{Harder3-10May2003,
         author = {Harder, M. and Mellen, J. and Ernst, M. D. },
         title = {Improving test suites via operational abstraction},
         journal = {Software Engineering, 2003. Proceedings. 25th International Conference
       	on},
         year = {3-10 May 2003},
         pages = {60--71},
         abstract = {This paper presents the operational difference technique for generating,
       	augmenting, and minimizing test suites. The technique is analogous
       	to structural code coverage techniques, but it operates in the semantic
       	domain of program properties rather than the syntactic domain of
       	program text. The operational difference technique automatically
       	selects test cases; it assumes only the existence of a source of
       	test cases. The technique dynamically generates operational abstractions
       	(which describe observed behavior and are syntactically identical
       	to formal specifications)from test suite executions. Test suites
       	can be generated by adding cases until the operational abstraction
       	stops changing. The resulting test suites are as small, and detect
       	as many faults, as suites with 100 branch coverage, and are better
       	at detecting certain common faults. This paper also presents the
       	area and stacking techniques for comparing test suite generation
       	strategies; these techniques avoid bias due to test suite size.},
         citeulike-article-id = {2638000},
         doi = {10.1109/ICSE.2003.1201188},
         keywords = {abstractions, bibtex-import, code, coverage, difference, domain, executions,
       	formal, generation, language, operational, program, programming,
       	semantics, specification, specifications, stacking, strategies, structural,
       	suite, syntactic, technique, techniques, test, testing, text, verification},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/improve-testsuite-icse2003.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:43},
         priority = {2},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/10.1109/ICSE.2003.1201188}
+      }
       @ARTICLE{Harel1987,
         author = {David Harel},
         title = {Statecharts: {A} Visual Formalism for Complex Systems},
         journal = {Science of Computer Programming},
         year = {1987},
         volume = {8},
         pages = {231--274},
         number = {3},
         month = {June},
         owner = {harald},
         timestamp = {2009.09.18},
         url = {citeseer.ist.psu.edu/harel87statecharts.html}
+      }
       @ARTICLE{Harel1987a,
         author = {David Harel},
         title = {Statecharts: A visual formalism for complex systems},
         journal = {Sci. Comput. Program.},
         year = {1987},
         volume = {8},
         pages = {231--274},
         number = {3},
         address = {Amsterdam, The Netherlands, The Netherlands},
         doi = {http://dx.doi.org/10.1016/0167-6423(87)90035-9},
         issn = {0167-6423},
         owner = {harald},
         publisher = {Elsevier North-Holland, Inc.},
         timestamp = {2009.09.18}
+      }
       @TECHREPORT{Hartman2004,
         author = {Alan Hartman},
         title = {Final Project Report},
         institution = {AGEDIS},
         year = {2004},
         month = {February},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Hartmann2000,
         author = {Jean Hartmann and Claudio Imoberdorf and Michael Meisinger},
         title = {UML-Based integration testing},
         booktitle = {ISSTA},
         year = {2000},
         pages = {60-70},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://doi.acm.org/10.1145/347324.348872},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Hartmann2005,
         author = {Jean Hartmann and Marlon Vieira and Herbert Foster and Axel Ruder},
         title = {A UML-based approach to system testing},
         journal = {ISSE},
         year = {2005},
         volume = {1},
         pages = {12-24},
         number = {1},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://dx.doi.org/10.1007/s11334-005-0006-0},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Hennessy1985,
         author = {Matthew Hennessy and Robin Milner},
         title = {Algebraic laws for nondeterminism and concurrency},
         journal = {J. ACM},
         year = {1985},
         volume = {32},
         pages = {137--161},
         number = {1},
         address = {New York, NY, USA},
         doi = {10.1145/2455.2460},
         issn = {0004-5411},
         owner = {harald},
         publisher = {ACM Press},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Henzinger1996,
         author = {T. A. Henzinger},
         title = {The theory of hybrid automata},
         booktitle = {LICS '96: Proceedings of the 11th Annual IEEE Symposium on Logic
       	in Computer Science},
         year = {1996},
         pages = {278},
         address = {Washington, DC, USA},
         publisher = {IEEE Computer Society},
         isbn = {0-8186-7463-6},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Henzinger1997,
         author = {Henzinger, Thomas A. and Ho, Pei-Hsin and Wong-Toi, Howard},
         title = {HYTECH: A Model Checker for Hybrid Systems},
         booktitle = {CAV '97: Proceedings of the 9th International Conference on Computer
       	Aided Verification},
         year = {1997},
         pages = {460--463},
         address = {London, UK},
         publisher = {Springer-Verlag},
         isbn = {3-540-63166-6}
+      }
       @INPROCEEDINGS{Henzinger2000,
         author = {Thomas A. Henzinger and Benjamin Horowitz and Rupak Majumdar and
       	Howard Wong-toi},
         title = {Beyond HYTECH: Hybrid systems analysis using interval numerical methods},
         booktitle = {in HSCC},
         year = {2000},
         pages = {130--144},
         publisher = {Springer}
+      }
       @INPROCEEDINGS{Henzinger2002,
         author = {Henzinger, Thomas A. and Jhala, Ranjit and Majumdar, Rupak and Sutre,
       	Gr\'{e}goire },
         title = {Lazy abstraction},
         booktitle = {POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on
       	Principles of programming languages},
         year = {2002},
         pages = {58--70},
         address = {New York, NY, USA},
         publisher = {ACM},
         abstract = {One approach to model checking software is based on the abstract-check-refine
       	paradigm: build an abstract model, then check the desired property,
       	and if the check fails, refine the model and start over. We introduce
       	the concept of lazy abstraction to integrate and optimize the three
       	phases of the abstract-cheek-refine loop. Lazy abstraction continuously
       	builds and refines a single abstract model on demand, driven by the
       	model checker, so that different parts of the model may exhibit different
       	degrees of precision, namely just enough to verify the desired property.
       	We present an algorithm for model checking safety properties using
       	lazy abstraction and describe an implementation of the algorithm
       	applied to C programs. We also provide sufficient conditions for
       	the termination of the method.},
         citeulike-article-id = {2638014},
         doi = {http://doi.acm.org/10.1145/503272.503279},
         keywords = {bibtex-import, blast},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/p58-henzinger.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:45},
         priority = {2},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/10.1145/503272.503279}
+      }
       @INPROCEEDINGS{Henzinger1995,
         author = {Henzinger, Thomas A. and Kopke, Peter W. and Puri, Anuj and Varaiya,
       	Pravin},
         title = {What's decidable about hybrid automata?},
         booktitle = {STOC '95: Proceedings of the twenty-seventh annual ACM symposium
       	on Theory of computing},
         year = {1995},
         pages = {373--382},
         address = {New York, NY, USA},
         publisher = {ACM},
         doi = {http://doi.acm.org/10.1145/225058.225162},
         isbn = {0-89791-718-9},
         location = {Las Vegas, Nevada, United States}
+      }
       @INPROCEEDINGS{Hessel2004,
         author = {Anders Hessel and Paul Pettersson},
         title = {A Test Case Generation Algorithm for Real-Time Systems},
         booktitle = {QSIC '04: Proceedings of the Quality Software, Fourth International
       	Conference},
         year = {2004},
         pages = {268--273},
         address = {Washington, DC, USA},
         publisher = {IEEE Computer Society},
         doi = {http://dx.doi.org/10.1109/QSIC.2004.5},
         isbn = {0-7695-2207-6},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Hickey2004,
         author = {Timothy J. Hickey and David K. Wittenberg},
         title = {Rigorous Modeling of Hybrid Systems Using Interval Arithmetic Constraints},
         booktitle = {HSCC},
         year = {2004},
         pages = {402-416},
         owner = {harald},
         timestamp = {2009.09.18},
         url = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=2993{\&}spage=402}
+      }
       @ARTICLE{Hierons2009,
         author = {Robert M. Hierons and Kirill Bogdanov and Jonathan P. Bowen and Rance
       	Cleaveland and John Derrick and Jeremy Dick and Marian Gheorghe and
       	Mark Harman and Kalpesh Kapoor and Paul Krause and Gerald L{\"u}ttgen
       	and Anthony J. H. Simons and Sergiy A. Vilkomir and Martin R. Woodward
       	and Hussein Zedan},
         title = {Using formal specifications to support testing},
         journal = {ACM Computing Surveys},
         year = {2009},
         volume = {41},
         number = {2},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://doi.acm.org/10.1145/1459352.1459354},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Hierons2008a,
         author = {Hierons, Robert M. and Merayo, Mercedes G. and N, Manuel},
         title = {Implementation Relations for the Distributed Test Architecture},
         booktitle = {TestCom '08 / FATES '08: Proceedings of the 20th IFIP TC 6/WG 6.1
       	international conference on Testing of Software and Communicating
       	Systems},
         year = {2008},
         pages = {200--215},
         address = {Berlin, Heidelberg},
         publisher = {Springer-Verlag},
         doi = {http://dx.doi.org/10.1007/978-3-540-68524-1_15},
         isbn = {978-3-540-68514-2},
         location = {Tokyo, Japan}
+      }
       @BOOK{Hoare1985,
         title = {Communicating Sequential Processes},
         publisher = {Prentice-Hall},
         year = {1985},
         author = {C.A.R. Hoare},
         series = {International Series in Computer Science},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Hoare1978,
         author = {Hoare, CAR},
         title = {{Communicating sequential processes}},
         journal = {Communications of the ACM},
         year = {1978},
         volume = {21},
         pages = {666--677},
         number = {8},
         owner = {harald},
         publisher = {ACM Press New York, NY, USA},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Hoare1969,
         author = {Hoare, C. A. R.},
         title = {An Axiomatic Basis for Computer Programming},
         journal = {Communications of the ACM},
         year = {1969},
         volume = {12},
         pages = {576--580 and 583},
         number = {10},
         month = {October},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{Hoare1998,
         title = {Unifying Theories of Programming},
         publisher = {Prentice-Hall International},
         year = {1998},
         author = {C.A.R.~Hoare and He Jifeng},
         key = {HH98},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Holzer2008,
         author = {Andreas Holzer and Christian Schallhart and Michael Tautschnig and
       	Helmut Veith},
         title = {{FShell: Systematic Test Case Generation for Dynamic Analysis and
       	Measurement}},
         booktitle = {Proceedings of the 20th International Conference on Computer Aided
       	Verification (CAV 2008)},
         year = {2008},
         volume = {5123},
         series = {Lecture Notes in Computer Science},
         pages = {209--213},
         address = {Princeton, NJ, USA},
         month = JUL,
         publisher = {Springer},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{Holzmann2004,
         title = {{The Spin Model Checker: Primer and Reference Manual}},
         publisher = {Addison-Wesley Professional},
         year = {2004},
         author = {Holzmann, G.J.},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Holzmann1997,
         author = {Gerard J. Holzmann},
         title = {{The Model Checker SPIN}},
         journal = {IEEE Trans. Softw. Eng.},
         year = {1997},
         volume = {23},
         pages = {279--295},
         number = {5},
         address = {Piscataway, NJ, USA},
         doi = {10.1109/32.588521},
         issn = {0098-5589},
         owner = {harald},
         publisher = {IEEE Press},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Hong2003,
         author = {Hong, Hyoung S. and Cha, Sung D. and Lee, Insup and Sokolsky, Oleg
       	and Ural, Hasan},
         title = {Data Flow Testing as Model Checking},
         journal = {icse},
         year = {2003},
         volume = {00},
         pages = {232},
         abstract = {This paper presents a model checking-based approach to data flow testing.
       	We characterize data flow oriented coverage criteria in temporal
       	logic such that the problem of test generation is reduced to the
       	problem of finding witnesses for a set of temporal logic formulas.
       	The capability of model checkers to construct witnesses and counterexamples
       	allows test generation to be fully automatic. We discuss complexity
       	issues in minimal cost test generation and describe heurstic test
       	generation algorithms. We illustrate our approach using CTL as temporal
       	logic and SMV as model checker.},
         address = {Los Alamitos, CA, USA},
         citeulike-article-id = {2638002},
         doi = {http://doi.ieeecomputersociety.org/10.1109/ICSE.2003.1201203},
         keywords = {bibtex-import, coverage, criteria},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/03icse.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:43},
         priority = {2},
         publisher = {IEEE Computer Society},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/http://doi.ieeecomputersociety.org/10.1109/ICSE.2003.1201203}
+      }
       @BOOK{Horebeek1993,
         title = {Algebraic Specifications in Software Engineering, an Introduction},
         publisher = {Springer Verlag},
         year = {1993},
         author = {Ivo Van Horebeek and Johan Lewi},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{HowdenSept.1976,
         author = {Howden, W. E. },
         title = {Reliability of the Path Analysis Testing Strategy},
         journal = {Software Engineering, Transactions on},
         year = {Sept. 1976},
         volume = {SE-2},
         pages = {208--215},
         number = {3},
         abstract = {A set of test data T for a program P is reliable if it reveals that
       	P contains an error whenever P is incorrect. If a set of tests T
       	is reliable and P produces the correct output for each element of
       	T then P is a correct program. Test data generation strategies are
       	procedures for generating sets of test data. A testing strategy is
       	reliable for a program P if it produces a reliable set of test data
       	for P. It is proved that an effective testing strategy which is reliable
       	for all programs cannot be constructed. A description of the path
       	analysis testing strategy is presented. In the path analysis strategy
       	data are generated which cause different paths in a program to be
       	executed. A method for analyzing the reliability of path testing
       	is introduced. The method is used to characterize certain classes
       	of programs and program errors for which the path analysis strategy
       	is reliable. Examples of published incorrect programs are included.},
         citeulike-article-id = {2637999},
         keywords = {analysissymbolic, bibtex-import, execution, path},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/01702367.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:42},
         priority = {2},
         timestamp = {2009.09.18}
+      }
       @ELECTRONIC{ConferenceProtocol,
         author = {http://fmt.cs.utwente.nl/ConfCase/v1.00/description/confprot.html},
         title = {Conference Protocol},
         url = {http://fmt.cs.utwente.nl/ConfCase/v1.00/description/confprot.html},
         owner = {harald},
         timestamp = {2009.06.22}
+      }
       @ELECTRONIC{EventB,
         author = {http://www.event-b.org/},
         title = {Event-B},
         url = {http://www.event-b.org/},
         owner = {harald},
         timestamp = {2009.06.22}
+      }
       @ARTICLE{IEEE2Sep1998,
         author = {IEEE},
         title = {IEEE standard for information technology - requirements and guidelines
       	for test methods specifications and test method implementations for
       	measuring conformance to POSIX(R) standards},
         journal = {IEEE Std 2003-1997},
         year = {2 Sep 1998},
         pages = {-},
         keywords = {IEEE standards, Unix, application program interfaces, conformance
       	testing, formal specification, information technology, program testing,
       	software standardsAPI standards, IEEE Std 2003-1997, IEEE standard,
       	POSIX standards, application programming interface, assertion test,
       	conformance document, conformance measurement, conformance test procedure,
       	conformance test software, implementation under test, information
       	technology, options, specification standards, test method implementations,
       	test method specifications, test result code},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{IEEE1990,
         author = {IEEE},
         title = {{IEEE} Standard Glossary of Software Engineering Terminology},
         journal = {IEEE Std 610.12-1990},
         year = {1990},
         month = Dec,
         biburl = {http://www.bibsonomy.org/bibtex/2168c4ff010eecef4cce9d5b0030060ce/wiljami74},
         keywords = {IEEE_Standard}
+      }
       @MISC{ISO1997,
         author = {ISO},
         title = {Information processing systems --- {Open} systems interconnection
       	--- {Estelle} --- A formal description technique based on an extended
       	state transition model},
         year = {1997},
         address = {Geneva},
         number = {9074},
         organization = {International Organization for Standardization},
         owner = {harald},
         timestamp = {2009.09.18},
         type = {IS}
+      }
       @MISC{ISO1989,
         author = {ISO},
         title = {{ISO} 8807: Information processing systems -- Open Systems Interconnection
       	-- {LOTOS} -- A formal description technique based on the temporal
       	ordering of observational behaviour},
         year = {1989},
         comment = {r},
         file = {iso1989lotos.pdf:iso1989lotos.pdf:PDF},
         institution = {iso.ch},
         owner = {martin},
         timestamp = {2007.09.07}
+      }
       @BOOK{ISO/IEC2002,
         title = {Z formal specification notation -- Syntax, type system and semantics},
         publisher = {ISO/IEC},
         year = {2002},
         author = {ISO/IEC},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @MISC{ITU-T2002,
         author = {ITU-T},
         title = {{Formal description techniques (FDT) -- Specification and Description
       	Language (SDL)}},
         year = {2002},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{J'eron1999,
         author = {J\'{e}ron, Thierry and Morel, Pierre},
         title = {Test Generation Derived from Model-Checking},
         booktitle = {CAV '99: Proceedings of the 11th International Conference on Computer
       	Aided Verification},
         year = {1999},
         pages = {108--121},
         address = {London, UK},
         publisher = {Springer-Verlag},
         isbn = {3-540-66202-2}
+      }
       @BOOK{Jackson2006,
         title = {Software Abstractions: Logic, Language, and Analysis},
         publisher = {The MIT Press},
         year = {2006},
         author = {Daniel Jackson},
         isbn = {0262101149},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Jackson2000,
         author = {Jackson, Daniel and Vaziri, Mandana },
         title = {Finding bugs with a constraint solver},
         journal = {SIGSOFT Softw. Eng. Notes},
         year = {2000},
         volume = {25},
         pages = {14--25},
         number = {5},
         abstract = {A method for finding bugs in code is presented. For given small numbers
       	j and k, the code of a procedure is translated into a relational
       	formula whose models represent all execution traces that involve
       	at most j heap cells and k loop iterations. This formula is conjoined
       	with the negation of the procedure's specification. The models of
       	the resulting formula, obtained using a constraint solver, are counterexamples:
       	executions of the code that violate the specification. The method
       	can analyze millions of executions in seconds, and thus rapidly expose
       	quite subtle flaws. It can accommodate calls to procedures for which
       	specifications but no code is available. A range of standard properties
       	(such as absence of null pointer dereferences) can also be easily
       	checked, using predefined specifications.},
         address = {New York, NY, USA},
         citeulike-article-id = {2638006},
         doi = {http://doi.acm.org/10.1145/347636.383378},
         keywords = {bibtex-import, boundingsymbolic, execution, loop},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/p14-jackson.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:44},
         priority = {2},
         publisher = {ACM},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/10.1145/347636.383378}
+      }
       @ARTICLE{Jacobs2001,
         author = {Bart Jacobs},
         title = {Assertional and Behavioural Refinement in Coalgebraic Specification},
         journal = {Electronic Notes in Theoretical Computer Science},
         year = {2001},
         volume = {47},
         pages = {1--36},
         libnum = {178},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Jard2005,
         author = {Claude Jard and Thierry J{\'e}ron},
         title = {{TGV}: theory, principles and algorithms},
         journal = {International Journal on Software Tools for Technology Transfer},
         year = {2005},
         volume = {7},
         pages = {297-315},
         number = {4},
         month = {August},
         abstract = {This paper discusses the details of the tool TGV. TGV operates on
       	a Input/Output-Labeled Transition System (IOLTS) for the specification
       	and an IOLTS for a test purpose. On the construction of the intersection
       	of this IOLTS TGV generates a Test-Case Graph. This Test-Case Graph
       	is again an IOLTS. Based on the input/output conformance relation
       	the Test-Case Graph can be used to generate a verdict for a certain
       	Implementation under Test},
         comment = {p,r},
         file = {jard2005tgv.pdf:jard2005tgv.pdf:PDF},
         filename = {./test\_generation/Jard-Jeron-05.ps},
         keywords = {Testing, Conformance Test, Test generation, Input/Output Labeled Transition
       	System},
         owner = {martin},
         timestamp = {2007.07.27}
+      }
       @INPROCEEDINGS{Jasper1994,
         author = {Jasper, Robert and Brennan, Mike and Williamson, Keith and Currier,
       	Bill and Zimmerman, David },
         title = {Test data generation and feasible path analysis},
         booktitle = {ISSTA '94: Proceedings of the 1994 ACM SIGSOFT international symposium
       	on Software testing and analysis},
         year = {1994},
         pages = {95--107},
         address = {New York, NY, USA},
         publisher = {ACM},
         abstract = {This paper describes techniques used by Test Specification and Determination
       	Tool (TSDT), an experimental prototype for analysis and testing of
       	critical applications written in Ada. Two problems dominate structural
       	testing of programs: exponential explosion in the number of execution
       	paths and feasible path determination, A path is feasible if there
       	exists some input that will cause the path to be traversed during
       	execution. We present techniques based on new representations combined
       	with automated theorem proving to deal with these problems, The paper
       	describes how these techniques can be used to determine the feasibility
       	of expressions containing references to Ada arrays. Finally, we present
       	algorithms specific to generating test data under the modified condition
       	decision coverage (MCDC) criterion. While we realize that many of
       	the problems we are attempting to solve are, in general, undecidable,
       	we are encouraged by preliminary results obtained from running TSDT
       	against vendor supplied code. Based on our results, we feel these
       	techniques can be applied to a broad enough section of Ada code to
       	make them cost effective.},
         citeulike-article-id = {2638010},
         doi = {http://doi.acm.org/10.1145/186258.187150},
         keywords = {bibtex-import, execution, generationsymbolic, infeasibility, problemtest,
       	vector},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/p95-jasper.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:44},
         priority = {2},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/10.1145/186258.187150}
+      }
       @ARTICLE{Jia2010,
         author = {Yue Jia and Mark Harman},
         title = {An Analysis and Survey of the Development of Mutation Testing},
         journal = {IEEE Transactions on Software Engineering},
         year = {2010},
         volume = {99},
         number = {PrePrints},
         address = {Los Alamitos, CA, USA},
         doi = {http://doi.ieeecomputersociety.org/10.1109/TSE.2010.62},
         issn = {0098-5589},
         publisher = {IEEE Computer Society}
+      }
       @INPROCEEDINGS{Johnsen2004,
         author = {Johnsen, Einar B. and Owe, Olaf },
         title = {An Asynchronous Communication Model for Distributed Concurrent Objects},
         booktitle = {SEFM '04: Proceedings of the Software Engineering and Formal Methods,
       	Second International Conference},
         year = {2004},
         pages = {188--197},
         address = {Washington, DC, USA},
         publisher = {IEEE Computer Society},
         citeulike-article-id = {2653554},
         doi = {http://dx.doi.org/10.1109/SEFM.2004.6},
         owner = {harald},
         posted-at = {2008-04-11 12:44:52},
         priority = {3},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/10.1109/SEFM.2004.6}
+      }
       @BOOK{Jones1990,
         title = {Systematic Software Development Using VDM},
         publisher = {Prentice-Hall},
         year = {1990},
         author = {Cliff B. Jones},
         series = {Series in Computer Science},
         edition = {second},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{Jr.1999,
         title = {Model Checking},
         publisher = {The MIT Press},
         year = {1999},
         author = {Edmund M. Clarke Jr. and Orna Grumberg and Doron A. Peled},
         isbn = {0262032708}
+      }
       @INPROCEEDINGS{Joebstl2010,
         author = {Jöbstl, Elisabeth and Weiglhofer, Martin and Aichernig, Bernhard
       	K. and Wotawa, Franz},
         title = {When {BDD}s Fail: Conformance Testing with Symbolic Execution and
       	{SMT} Solving},
         booktitle = {Proceedings of the 2010 Third International Conference on Software
       	Testing, Verification and Validation},
         year = {2010},
         series = {ICST '10},
         pages = {479--488},
         address = {Washington, DC, USA},
         publisher = {IEEE Computer Society},
         acmid = {1828492},
         doi = {http://dx.doi.org/10.1109/ICST.2010.48},
         isbn = {978-0-7695-3990-4},
         keywords = {model-based testing, symbolic execution, conformance testing, symbolic
       	input-output conformance, symbolic test case generation},
         numpages = {10},
         url = {http://dx.doi.org/10.1109/ICST.2010.48}
+      }
       @TECHREPORT{K.L.McMillan1992,
         author = {{K.L. McMillan}},
         title = {The {SMV} system},
         institution = {Carnegie-Mellon University},
         year = {1992},
         number = {CMU-CS-92-131},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Kansomkeat2003,
         author = {Supaporn Kansomkeat and Wanchai Rivepiboon},
         title = {Automated-generating test case using {UML} statechart diagrams},
         booktitle = {Proc. of SAICSIT 2003},
         year = {2003},
         pages = {296--300}
+      }
       @INPROCEEDINGS{Khurshid2003,
         author = {Khurshid, Sarfraz and Pasareanu, Corina S. and Visser, Willem },
         title = {Generalized Symbolic Execution for Model Checking and Testing},
         booktitle = {TACAS},
         year = {2003},
         pages = {553--568},
         abstract = {Modern software systems, which often are concurrent and manipulate
       	complex data structures must be extremely reliable. We present a
       	novel framework based on symbolic execution, for automated checking
       	of such systems. We provide a two-fold generalization of traditional
       	symbolic execution based approaches. First, we define a source to
       	source translation to instrument a program, which enables standard
       	model checkers to perform symbolic execution of the program. Second,
       	we give a novel symbolic execution algorithm that handles dynamically
       	allocated structures (e.g., lists and trees), method preconditions
       	(e.g., acyclicity), data (e.g., integers and strings) and concurrency.
       	The program instrumentation enables a model checker to automatically
       	explore different program heap configurations and manipulate logical
       	formulae on program data (using a decision procedure). We illustrate
       	two applications of our framework: checking correctness of multi-threaded
       	programs that take inputs from unbounded domains with complex structure
       	and generation of non-isomorphic test inputs that satisfy a testing
       	criterion. Our implementation for Java uses the Java PathFinder model
       	checker.},
         citeulike-article-id = {2638007},
         keywords = {bibtex-import, bounding, executionloop, generationsymbolic, test,
       	vector},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/GSE.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:44},
         priority = {2},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Kicillof2007,
         author = {Nicolas Kicillof and Wolfgang Grieskamp and Nikolai Tillmann and
       	Victor Braberman},
         title = {Achieving both model and code coverage with automated gray-box testing},
         booktitle = {A-MOST '07: Proceedings of the 3rd international workshop on Advances
       	in model-based testing},
         year = {2007},
         pages = {1--11},
         address = {New York, NY, USA},
         publisher = {ACM},
         doi = {http://doi.acm.org/10.1145/1291535.1291536},
         isbn = {978-1-59593-850-3},
         location = {London, United Kingdom},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{King1976,
         author = {King, James C. },
         title = {Symbolic execution and program testing},
         journal = {Commun. ACM},
         year = {1976},
         volume = {19},
         pages = {385--394},
         number = {7},
         abstract = {This paper describes the symbolic execution of programs. Instead of
       	supplying the normal inputs to a program (e.g. numbers) one supplies
       	symbols representing arbitrary values. The execution proceeds as
       	in a normal execution except that values may he symbolic formulas
       	over the input symbols. The difficult, yet interesting issues arise
       	during the symbolic execution of conditional branch type statements.
       	A particular system called EFFIGY which provides symbolic execution
       	for program testing and debugging is also described, it interpretively
       	executes programs written in a simple PL/I style programming language.
       	It includes many standard debugging features, the ability to manage
       	and to prove things about symbolic expressions, a simple program
       	testing manager, and a program verifier. A brief discussion of the
       	relationship between symbolic execution and program proving is also
       	included.},
         address = {New York, NY, USA},
         citeulike-article-id = {2638012},
         doi = {http://doi.acm.org/10.1145/360248.360252},
         keywords = {bibtex-import, execution, generationsymbolic, test, vector},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/p385-king.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:45},
         priority = {2},
         publisher = {ACM},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/10.1145/360248.360252}
+      }
       @ARTICLE{Kleer1984,
         author = {Johan De Kleer and John Seely Brown},
         title = {A qualitative physics based on confluences},
         journal = {Artif. Intell.},
         year = {1984},
         volume = {24},
         pages = {7--83},
         number = {1-3},
         address = {Essex, UK},
         doi = {http://dx.doi.org/10.1016/0004-3702(84)90037-7},
         issn = {0004-3702},
         owner = {harald},
         publisher = {Elsevier Science Publishers Ltd.},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Kozen1983,
         author = {Dexter Kozen},
         title = {Results on the Propositional mu-Calculus.},
         journal = {Theor. Comput. Sci.},
         year = {1983},
         volume = {27},
         pages = {333-354},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Krenn2010,
         author = {Willibald Krenn and Rupert Schlick and Bernhard K. Aichernig},
         title = {Mapping {UML} to Labeled Transition Systems for Test-Case Generation
       	-- A Translation via Object-Oriented Action Systems},
         booktitle = {Proc. of Formal Methods for Components and Objects (FMCO) 2009},
         year = {2010},
         volume = {6286},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         owner = {wkrenn},
         timestamp = {2010.03.18}
+      }
       @ARTICLE{Krichen2009,
         author = {Krichen, Moez and Tripakis, Stavros},
         title = {Conformance testing for real-time systems},
         journal = {Form. Methods Syst. Des.},
         year = {2009},
         volume = {34},
         pages = {238--304},
         number = {3},
         address = {Hingham, MA, USA},
         doi = {http://dx.doi.org/10.1007/s10703-009-0065-1},
         issn = {0925-9856},
         publisher = {Kluwer Academic Publishers}
+      }
       @BOOK{Kuipers1994,
         title = {Qualitative Reasoning: Modeling and Simulation with Incomplete Knowledge},
         publisher = {MIT Press},
         year = {1994},
         author = {Kuipers, Benjamin},
         keywords = {QSIM},
         owner = {harald},
         priority = {0},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Larsen2005a,
         author = {Kim G. Larsen and Marius Mikucionis and Brian Nielsen},
         title = {Online Testing of Real-Time Systems Using UPPAAL: Status and Future
       	Work},
         booktitle = {Perspectives of Model-Based Testing},
         year = {2005},
         editor = {Ed Brinksma and Wolfgang Grieskamp and Jan Tretmans},
         number = {04371},
         series = {Dagstuhl Seminar Proceedings},
         publisher = {Internationales Begegnungs- und Forschungszentrum fuer Informatik
       	(IBFI), Schloss Dagstuhl, Germany},
         note = {$<$http://drops.dagstuhl.de/opus/volltexte/2005/326$>$ [date of citation:
 -01-01]},
         issn = {1862-4405},
         optaddress = {Dagstuhl, Germany},
         optannote = {Keywords: Online testing, black-box testing, real-time systems, embedded
       	systems, symbolic state representation, relativized timed input/output
       	conformance, mo},
         opturl = {http://drops.dagstuhl.de/opus/volltexte/2005/326 [date of citation:
 -01-01]},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Larsen2005,
         author = {Kim G. Larsen and Marius Mikucionis and Brian Nielsen and Arne Skou},
         title = {Testing real-time embedded software using UPPAAL-TRON: an industrial
       	case study},
         booktitle = {EMSOFT '05: Proceedings of the 5th ACM international conference on
       	Embedded software},
         year = {2005},
         pages = {299--306},
         address = {New York, NY, USA},
         publisher = {ACM},
         doi = {http://doi.acm.org/10.1145/1086228.1086283},
         isbn = {1-59593-091-4},
         location = {Jersey City, NJ, USA},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{LaValle1999,
         author = {Steven M. LaValle and James J. Kuffner Jr.},
         title = {Randomized Kinodynamic Planning},
         booktitle = {International Conference on Robotics and Automation},
         year = {1999},
         pages = {473-479},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INCOLLECTION{Leavens1999,
         author = {Gary T. Leavens and Albert L. Baker and Clyde Ruby},
         title = {{JML}: {A} Notation for Detailed Design},
         booktitle = {Behavioral Specifications of Businesses and Systems},
         publisher = {Kluwer Academic Publishers},
         year = {1999},
         editor = {Haim Kilov and Bernhard Rumpe and Ian Simmonds},
         pages = {175--188},
         owner = {harald},
         timestamp = {2009.09.18},
         url = {citeseer.ist.psu.edu/leavens99jml.html}
+      }
       @ARTICLE{Lee1996,
         author = {David Lee and Mihakus Yannakakis},
         title = {Principles and Methods of Testing Finite State Machines -- A Survey},
         journal = {Proceedings of the IEEE},
         year = {1996},
         volume = {84},
         pages = {1090--1123},
         number = {8},
         month = {August},
         abstract = {This paper reviews possible test generation techniques on finite state
       	machines. It discusses distinquishing sequences, seperating sequences,
       	intput/output sequences, seperating sequences and so on. It concludes
       	with a short view on other state machine representations such as
       	extended finite state machines and probabilistic state machines.},
         file = {lee1996principles.pdf:lee1996principles.pdf:PDF},
         filename = {./test\_generation/lee96principles.pdf},
         keywords = {Testing, FSM, EFSM, PFSM, NFSM},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Lefebvre2006,
         author = {Marie-Anne Lefebvre and Hervé Guéguen},
         title = {Hybrid abstractions of affine systems},
         journal = {Nonlinear Analysis},
         year = {2006},
         volume = {65},
         pages = {1150 - 1167},
         number = {6},
         note = {Hybrid Systems and Applications (5)},
         doi = {DOI: 10.1016/j.na.2005.12.016},
         issn = {0362-546X},
         keywords = {Hybrid systems},
         url = {http://www.sciencedirect.com/science/article/B6V0Y-4JFGF71-2/2/9f7f4ee86fb16bf7f463a65950bc6feb}
+      }
       @INPROCEEDINGS{Legeard2002,
         author = {Bruno Legeard and Fabien Peureux and Mark Utting},
         title = {Automated Boundary Testing from {Z} and {B}},
         booktitle = {Proceedings of FME 2002: Formal Methods --- Getting IT Right, International
       	Symposium of Formal Methods Europe, July 2002, Copenhagen, Denmark},
         year = {2002},
         editor = {Lars-Henrik Eriksson and Peter A. Lindsay},
         volume = {2391},
         series = {Lecture Notes in Computer Science},
         pages = {21--40},
         publisher = {Springer-Verlag},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Leveson2004,
         author = {Nancy G. Leveson},
         title = {The role of software in spacecraft accidents},
         journal = {AIAA Journal of Spacecraft and Rockets},
         year = {2004},
         volume = {41},
         pages = {564--575}
+      }
       @INPROCEEDINGS{Ma2006,
         author = {Ma, Yu-Seung and Offutt, Jeff and Kwon, Yong-Rae},
         title = {MuJava: a mutation system for java},
         booktitle = {ICSE '06: Proceedings of the 28th international conference on Software
       	engineering},
         year = {2006},
         pages = {827--830},
         address = {New York, NY, USA},
         publisher = {ACM},
         bdsk-url-1 = {http://doi.acm.org/10.1145/1134285.1134425},
         doi = {http://doi.acm.org/10.1145/1134285.1134425},
         isbn = {1-59593-375-1},
         location = {Shanghai, China}
+      }
       @INPROCEEDINGS{Maibaum2003,
         author = {Tom Maibaum},
         title = {In Memoriam {Armando Mart\'{i}n Haeberer}},
         booktitle = {Formal Methods at the Crossroads: from Panacea to Foundational Support},
         year = {2003},
         editor = {Bernhard K.\ Aichernig and Tom Maibaum},
         volume = {2757},
         series = {Lecture Notes in Computer Science},
         pages = {1--25},
         publisher = {Springer-Verlag},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PHDTHESIS{Man2006,
         author = {K.L. Man and R.R.H. Schiffelers},
         title = {Formal Specification and Analysis of Hybrid Systems},
         school = {Eindhoven University of Technology},
         year = {2006},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{Matiyasevich1993,
         title = {Hilbert's tenth problem},
         publisher = {MIT Press},
         year = {1993},
         author = {Matiyasevich, Yuri V.},
         address = {Cambridge, MA, USA},
         isbn = {0-262-13295-8}
+      }
       @BOOK{McMillan1993,
         title = {Symbolic Model Checking},
         publisher = {Kluwer Academic Publishers},
         year = {1993},
         author = {Kenneth L. McMillan},
         address = {Norwell, MA, USA},
         isbn = {0792393805},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Memon2007,
         author = {Atif M. Memon},
         title = {An event-flow model of GUI-based applications for testing},
         journal = {Softw. Test., Verif. Reliab.},
         year = {2007},
         volume = {17},
         pages = {137-157},
         number = {3},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://dx.doi.org/10.1002/stvr.364},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{Meyer1997,
         title = {Object-Oriented Software Construction},
         publisher = {Prentice Hall Professional Technical Reference},
         year = {1997},
         author = {Bertrand Meyer},
         abstract = {The developer of the acclaimed Eiffel programming language comes through
       	with one of the clearest and most informative books about computers
       	ever committed to paper. <i>Object-Oriented Software Construction</i>
       	is the gospel of object-oriented technology and it deserves to be
       	spread everywhere. Meyer opens with coverage of the need for an object-oriented
       	approach to software development, citing improved quality and development
       	speed as key advantages of the approach. He then explains all the
       	key criteria that define an object- oriented approach to a problem.
       	Meyer pays attention to techniques, such as classes, objects, memory
       	management, and more, returning to each technique and polishing his
       	readers' knowledge of it as he explains how to employ it "well."
       	In a section on advanced topics, Meyer explores interesting and relevant
       	topics, such as persistent objects stored in a database. He also
       	offers a sort of "Do and Don't" section in which he enumerates common
       	mistakes and ways to avoid them. Management information isn't the
       	main point of <i>Object-Oriented Software Construction</i>, but you'll
       	find some in its pages. Meyer concludes his tour de force with comparisons
       	of all the key object-oriented languages, including Java. He also
       	covers the potential of simulating object technology in non-object-oriented
       	languages, such as Pascal and Fortran. The companion CD-ROM includes
       	the full text of this book in hypertext form, as well as some tools
       	for designing object-oriented systems. If you program computers,
       	you need to read this book. <I>Recipient of the 1997 Jolt Award.</I>
       	<P>The developer of the acclaimed Eiffel programming language comes
       	through with one of the clearest and most informative books about
       	computers ever committed to paper. Object-Oriented Software Construction
       	is the gospel of object-oriented technology and it deserves to be
       	spread everywhere. Meyer opens with coverage of the need for an object-oriented
       	approach to software development, citing improved quality and development
       	speed as key advantages of the approach. He then explains all the
       	key criteria that define an object- oriented approach to a problem.
       	Meyer pays attention to techniques, such as classes, objects, memory
       	management, and more, returning to each technique and polishing his
       	readers' knowledge of it as he explains how to employ it "well."
       	In a section on advanced topics, Meyer explores interesting and relevant
       	topics, such as persistent objects stored in a database. He also
       	offers a sort of "Do and Don't" section in which he enumerates common
       	mistakes and ways to avoid them. Management information isn't the
       	main point of Object-Oriented Software Construction, but you'll find
       	some in its pages. Meyer concludes his tour de force with comparisons
       	of all the key object-oriented languages, including Java. He also
       	covers the potential of simulating object technology in non-object-oriented
       	languages, such as Pascal and Fortran. The companion CD-ROM includes
       	the full text of this book in hypertext form, as well as some tools
       	for designing object-oriented systems. If you program computers,
       	you need to read this book.},
         isbn = {0-13-629155-4},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{Milner1999,
         title = {Communicating and Mobile Systems: the Pi-Calculus},
         publisher = {{Cambridge University Press}},
         year = {1999},
         author = {Milner, Robin },
         month = {June},
         citeulike-article-id = {500640},
         howpublished = {Paperback},
         isbn = {0521658691},
         keywords = {calculus, process},
         owner = {harald},
         priority = {3},
         timestamp = {2009.09.18},
         url = {http://www.amazon.ca/exec/obidos/redirect?tag=citeulike09-20\&amp;path=ASIN/0521658691}
+      }
       @BOOK{Milner1982,
         title = {{A Calculus of Communicating Systems}},
         publisher = {Springer-Verlag New York, Inc. Secaucus, NJ, USA},
         year = {1982},
         author = {Milner, R.},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{Morgan1990,
         title = {Programming from Specifications},
         publisher = {Prentice-Hall International},
         year = {1990},
         author = {Carroll C.\ Morgan},
         series = {Series in Computer Science},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Mosses1999,
         author = {Peter D.~Mosses},
         title = {{CASL}: A guided tour of its design},
         booktitle = {Proceedings of WADT'98},
         year = {1999},
         volume = {1589},
         series = {Lecture Notes in Computer Science},
         pages = {216--240},
         publisher = {Springer-Verlag},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Moura2004,
         author = {Leonardo de Moura and Sam Owre and Harald Rue{\ss} and John Rushbyand
       	N. Shankar and Maria Sorea and Ashish Tiwari},
         title = {{SAL 2}},
         booktitle = {Computer-Aided Verification, {CAV} 2004},
         year = {2004},
         editor = {Rajeev Alur and Doron Peled},
         volume = {3114},
         series = {Lecture Notes in Computer Science},
         pages = {496--500},
         address = {Boston, MA},
         month = jul,
         publisher = {Springer-Verlag},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{Myers2004,
         title = {{The Art of Software Testing}},
         publisher = {Wiley},
         year = {2004},
         author = {Myers, G. J. },
         citeulike-article-id = {2804765},
         keywords = {fundamentals},
         owner = {harald},
         posted-at = {2008-05-16 10:32:55},
         priority = {4},
         timestamp = {2009.09.18}
+      }
       @BOOK{Myers2004a,
         title = {The Art of Software Testing},
         publisher = {John Wiley \& Sons},
         year = {2004},
         author = {Myers, Glenford J. and Sandler, Corey},
         isbn = {0471469122}
+      }
       @INPROCEEDINGS{Nahhal2007,
         author = {Tarik Nahhal and Thao Dang},
         title = {Test Coverage for Continuous and Hybrid Systems},
         booktitle = {Computer Aided Verification},
         year = {2007},
         pages = {449-462},
         doi = {http://dx.doi.org/10.1007/978-3-540-73368-3_47},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Nicola1990,
         author = {Rocco De Nicola and Frits Vaandrager},
         title = {Action versus state based logics for transition systems},
         booktitle = {Proceedings of the LITP spring school on theoretical computer science
       	on Semantics of systems of concurrent processes},
         year = {1990},
         pages = {407--419},
         address = {New York, NY, USA},
         publisher = {Springer-Verlag New York, Inc.},
         isbn = {0-387-53479-2},
         location = {La Roche Posay, France},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{Nipkow2002,
         title = {Isabelle/HOL - A Proof Assistant for Higher-Order Logic},
         publisher = {Springer},
         year = {2002},
         author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
         volume = {2283},
         series = {Lecture Notes in Computer Science},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         isbn = {3-540-43376-7},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Offutt1996,
         author = {Offutt, A.J. and Jie Pan},
         title = {Detecting equivalent mutants and the feasible path problem},
         year = {1996},
         pages = {224 -236},
         month = {jun.},
         doi = {10.1109/CMPASS.1996.507890},
         journal = {Computer Assurance, 1996. COMPASS '96, 'Systems Integrity. Software
       	Safety. Process Security'. Proceedings of the Eleventh Annual Conference
       	on},
         keywords = {critical software;equivalent mutant programs;feasible path problem;high
       	reliability;infeasible constraints;mathematical constraint systems;mathematical
       	constraints;mutation testing;proof of concept implementation;software
       	unit testing;test criteria;program testing;safety-critical software;software
       	quality;}
+      }
       @ARTICLE{Offutt1997,
         author = {A. Jefferson Offutt and Jie Pan},
         title = {Automatically Detecting Equivalent Mutants and Infeasible Paths},
         journal = {Software Testing, Veri and Reliability},
         year = {1997},
         volume = {7},
         pages = {165--192}
+      }
       @ARTICLE{Oliveira2007,
         author = {Marcel Oliveira and Ana Cavalcanti and Jim Woodcock},
         title = {A Denotational Semantics for Circus},
         journal = {Electr. Notes Theor. Comput. Sci.},
         year = {2007},
         volume = {187},
         pages = {107-123},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://dx.doi.org/10.1016/j.entcs.2006.08.047},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PHDTHESIS{Oster2007,
         author = {Norbert Oster},
         title = {Automatische Generierung optimaler struktureller Testdaten f{\"u}r
       	objekt-orientierte Software mittels multi-objektiver Metaheuristiken
       	},
         school = {Friedrich--Alexander University, Erlangen-N{\"u}rnberg},
         year = {2007},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Ostrand1998,
         author = {Thomas Ostrand and Aaron Anodide and Herbert Foster and Tarak Goradia},
         title = {A visual test development environment for GUI systems},
         journal = {SIGSOFT Softw. Eng. Notes},
         year = {1998},
         volume = {23},
         pages = {82--92},
         number = {2},
         address = {New York, NY, USA},
         doi = {http://doi.acm.org/10.1145/271775.271793},
         issn = {0163-5948},
         owner = {harald},
         publisher = {ACM},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Ostrand1988,
         author = {T. J. Ostrand and M. J. Balcer},
         title = {The category-partition method for specifying and generating fuctional
       	tests},
         journal = {Commun. ACM},
         year = {1988},
         volume = {31},
         pages = {676--686},
         number = {6},
         address = {New York, NY, USA},
         doi = {http://doi.acm.org/10.1145/62959.62964},
         issn = {0001-0782},
         owner = {harald},
         publisher = {ACM},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Paradkar2005,
         author = {Paradkar, Amit },
         title = {Case studies on fault detection effectiveness of model based test
       	generation techniques},
         booktitle = {A-MOST '05: Proceedings of the 1st international workshop on Advances
       	in model-based testing},
         year = {2005},
         pages = {1--7},
         address = {New York, NY, USA},
         publisher = {ACM},
         abstract = {Model-based test generation (MBTG) is becoming an area of active research.
       	These techniques differ in terms of (1) modeling notations used,
       	and (2) the adequacy criteria used for test generation. This paper
       	(1) reviews different classes of MBTG techniques at a conceptual
       	level, and (2) reports results of two case studies comparing various
       	techniques in terms of their fault detection effectiveness. Our results
       	indicate that MBTG technique which employs mutation and explicitly
       	generates state verification sequences has better fault detection
       	effectiveness than those based on boundary values, and predicate
       	coverage criteria for transitions. Instead of a default adequacy
       	criteria, certain techniques allow the user to specify test objectives
       	in addition to the model. Our experience indicates that the task
       	of defining appropriate test objectives is not intuitive. Furthermore,
       	notations provided to describe such test objectives may have inadequate
       	expressive power. We posit the need for a suitable fault modeling
       	notation.},
         citeulike-article-id = {2638015},
         doi = {http://doi.acm.org/10.1145/1083274.1083286},
         keywords = {bibtex-import},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/p12-paradkar.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:45},
         priority = {2},
         timestamp = {2009.09.18},
         url = {http://doi.acm.org/10.1145/1083274.1083286}
+      }
       @TECHREPORT{Paul2007,
         author = {Paul},
         title = {Testing with model checkers: A survey},
         institution = {Competence Network Softnet Austria},
         year = {2007},
         number = {SNA-TR-2007-P2-04},
         citeulike-article-id = {2637994},
         keywords = {bibtex-import, tug},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/SNA-TR-2007-P2-04.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:41},
         priority = {2},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Peischl2007,
         author = {Peischl, Bernhard and Weiglhofer, Martin and Wotawa, Franz },
         title = {Executing Abstract Test Cases},
         booktitle = {In Proceedings of the Model-based Testing Workshop held in conjunction
       	with the 37th Annual Congress of the Gesellschaft fuer Informatik
       	(MOTES 2007)},
         year = {2007},
         pages = {421--426},
         month = {September},
         abstract = {This paper shows how to use an on-the-fly verification algo rithm,
       	that verifies the equivalence of labeled transition sys tems, for
       	the verification of the input output conformance (ioco) of input
       	output labeled transition systems. Since ioco is usually used for
       	testing there are several requirements on the input output labeled
       	transition system (IOLTS) that are used for test generation. We show
       	how to take care of these requirements during the on-the-fly verification.
       	Thus the presented approach can be applied to IOLTSs that do not
       	initially fulfill these requirements. Finally, we discuss the evaluation
       	of a prototype implementation on the datalink protocol.},
         citeulike-article-id = {2637992},
         keywords = {bibtex-import, tug},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/motes2007.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:41},
         priority = {2},
         timestamp = {2009.09.18}
+      }
       @INBOOK{Peled2003,
         title = {Model Checking and Testing Combined},
         publisher = {Springer Berlin / Heidelberg},
         year = {2003},
         author = {Peled, Doron },
         volume = {2719/2003},
         series = {Lecture Notes in Computer Science},
         month = {jan},
         abstract = {Model checking is a technique for automatically checking properties
       	of models of systems. We present here several combinations of model
       	checking with testing techniques. This allows checking systems when
       	no model is given, when the model is inaccurate, or when only a part
       	of its description is given.},
         citeulike-article-id = {2638004},
         doi = {10.1007/3-540-45061-0\_5},
         keywords = {bibtex-import, black-box, testing},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/peled-modcheckandtest.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:44},
         priority = {2},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/10.1007/3-540-45061-0\_5}
+      }
       @INPROCEEDINGS{Peleska1996,
         author = {Jan Peleska and Michael Siegel},
         title = {From Testing Theory to Test Driver Implementation},
         booktitle = {FME'96: Industrial Benefit and Advances in Formal Methods},
         year = {1996},
         editor = {Marie-Claude Gaudel and Jim Woodcock},
         pages = {538--556},
         month = {March},
         publisher = {Springer-Verlag},
         key = {Peleska\&96},
         libnum = {6},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Petrenko2002,
         author = {Alexandre Petrenko and Nina Yevtushenko},
         title = {Queued Testing of Transition Systems with Inputs and Outputs},
         booktitle = {Proceedings of the Workshop on Formal Approaches to Testing Of Software
       	(Fates'02), A Satellite Workshop of Concur'02},
         year = {2002},
         editor = {Rob Hierons and Thierry J\'{e}ron},
         pages = {79--94},
         address = {Brno, Czech Republic},
         month = {August},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Platzer2008,
         author = {Andr{\'e} Platzer},
         title = {Differential Dynamic Logic for Hybrid Systems.},
         journal = {Journal of Automated Reasoning},
         year = {2008},
         volume = {41},
         pages = {143-189},
         number = {2},
         abstract = { Hybrid systems are models for complex physical systems and are defined
       	as dynamical systems with interacting discrete transitions and continuous
       	evolutions along differential equations. With the goal of developing
       	a theoretical and practical foundation for deductive verification
       	of hybrid systems, we introduce a dynamic logic for hybrid programs,
       	which is a program notation for hybrid systems. As a verification
       	technique that is suitable for automation, we introduce a free variable
       	proof calculus with a novel combination of real-valued free variables
       	and Skolemisation for lifting quantifier elimination for real arithmetic
       	to dynamic logic. The calculus is compositional, i.e., it reduces
       	properties of hybrid programs to properties of their parts. Our main
       	result proves that this calculus axiomatises the transition behaviour
       	of hybrid systems completely relative to differential equations.
       	In a case study with cooperating traffic agents of the European Train
       	Control System, we further show that our calculus is well-suited
       	for verifying realistic hybrid systems with parametric system dynamics.
       	},
         doi = {10.1007/s10817-008-9103-8},
         issn = {0168-7433},
         keywords = {dynamic logic, differential equations, sequent calculus, axiomatisation,
       	automated theorem proving, verification of hybrid systems},
         longjournal = {Journal of Automated Reasoning},
         medjournal = {J. Autom. Reasoning}
+      }
       @INCOLLECTION{Platzer2008a,
         author = {Platzer, André and Quesel, Jan-David},
         title = {KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)},
         booktitle = {Automated Reasoning},
         publisher = {Springer Berlin, Heidelberg},
         year = {2008},
         editor = {Armando, Alessandro and Baumgartner, Peter and Dowek, Gilles},
         volume = {5195},
         series = {Lecture Notes in Computer Science},
         pages = {171-178}
+      }
       @INPROCEEDINGS{Platzer2008b,
         author = {Platzer, Andr\'{e} and Quesel, Jan-David},
         title = {Logical Verification and Systematic Parametric Analysis in Train
       	Control},
         booktitle = {HSCC '08: Proceedings of the 11th international workshop on Hybrid
       	Systems},
         year = {2008},
         pages = {646--649},
         address = {Berlin, Heidelberg},
         publisher = {Springer-Verlag},
         doi = {http://dx.doi.org/10.1007/978-3-540-78929-1_55},
         isbn = {978-3-540-78928-4},
         location = {St. Louis, MO, USA}
+      }
       @INPROCEEDINGS{Pnueli1977,
         author = {Amir Pnueli},
         title = {The Temporal Logic of Programs},
         booktitle = {18th Annual Symposium on Foundations of Computer Science, 31 October-2
       	November, Providence, Rhode Island, USA},
         year = {1977},
         pages = {46--57},
         publisher = {IEEE},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Ronkko2003,
         author = {Mauno R\"{o}nkk\"{o} and Anders P. Ravn and Kaisa Sere},
         title = {Hybrid action systems},
         journal = {Theor. Comput. Sci.},
         year = {2003},
         volume = {290},
         pages = {937--973},
         number = {1},
         address = {Essex, UK},
         doi = {http://dx.doi.org/10.1016/S0304-3975(02)00547-9},
         issn = {0304-3975},
         owner = {harald},
         publisher = {Elsevier Science Publishers Ltd.},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Ronkko1999,
         author = {R\"{o}nkk\"{o},, Mauno and Sere,, Kaisa},
         title = {Refinement and Continuous Behaviour},
         booktitle = {HSCC '99: Proceedings of the Second International Workshop on Hybrid
       	Systems},
         year = {1999},
         pages = {223--237},
         address = {London, UK},
         publisher = {Springer-Verlag},
         isbn = {3-540-65734-7}
+      }
       @BOOK{RAISELanguageGroup1995,
         title = {The {RAISE} Development Method},
         publisher = {Prentice Hall},
         year = {1995},
         author = {{RAISE Language Group}, The},
         series = {BCS Practitioner Series},
         annote = {\CRCS{D.2.1, 000427}},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{RamamoorthyDec.1976,
         author = {Ramamoorthy, C. V. and Ho and Chen, W. T. },
         title = {On the Automated Generation of Program Test Data},
         journal = {Software Engineering, Transactions on},
         year = {Dec. 1976},
         volume = {SE-2},
         pages = {293--300},
         number = {4},
         abstract = {Software validation through testing will continue to be a very important
       	tool for ensuring correctness of large scale software systems. Automation
       	of testing tools can greatly enhance their power and reduce testing
       	cost. In,this paper, techniques for automated test data generation
       	are discussed. Given a program graph, a set of paths are identified
       	to satisfy some given testing criteria. When a path or a program
       	segment is specified, symbolic execution is used for generating input
       	constraints which defme a set of inputs for executing this path or
       	segment. Problems encountered in symbolic execution are discussed.
       	A new approach for resolving array reference ambiguities and a procedure
       	for generating test inputs satisfying input constraints are proposed.
       	References to arrays are recorded in a table during symbolic execution
       	and ambiguities are resolved when test data are-generated to evaluate
       	the subscript expressions. The implementation of a test data generator
       	for Fortran programs incorporating these techniques is also described.},
         citeulike-article-id = {2638011},
         keywords = {ambiguity, array, bibtex-import, constraint, execution, generation,
       	path, reference, solver, symbolic, test, vector},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/01702386.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:45},
         priority = {2},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Rapps1985,
         author = {Sandra Rapps and Elaine J. Weyuker},
         title = {Selecting Software Test Data Using Data Flow Information},
         journal = {IEEE Trans. Software Eng.},
         year = {1985},
         volume = {11},
         pages = {367-375},
         number = {4},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @TECHREPORT{ReactiveSystems2003,
         author = {{Reactive Systems}},
         title = {Model-Based Testing and Validation with {Reactis}},
         institution = {Reactive Systems, Inc.},
         year = {2003},
         key = {{Reactive Systems, Inc.}},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Richters1998,
         author = {Richters, Mark and Gogolla, Martin},
         title = {On Formalizing the UML Object Constraint Language OCL},
         journal = {Conceptual Modeling --ER '98},
         year = {1998},
         pages = {449--464},
         abstract = {We present a formal semantics for the Object Constraint Language (OCL)
       	which is part of the Unified Modeling Language (UML) - an emerging
       	standard language and notation for object-oriented analysis and design.
       	In context of information systems modeling, UML class diagrams can
       	be utilized for describing the overall structure, whereas additional
       	integrity constraints and queries are specified with OCL expressions.
       	By using OCL, constraints and queries can be specified in a formal
       	yet comprehensible way. However, the OCL itself is currently defined
       	only in a semi-formal way. Thus the semantics of constraints is in
       	general not precisely defined. Our approach gives precise meaning
       	to OCL concepts and to some central aspects of UML class models.
       	A formal semantics facilitates verification, validation and simulation
       	of models and helps to improve the quality of models and software
       	designs.},
         date-added = {2008-05-27 02:43:14 +0200},
         date-modified = {2008-05-27 02:43:14 +0200},
         owner = {harald},
         timestamp = {2009.09.18},
         ty = {CHAPTER},
         url = {http://www.springerlink.com/content/74bxqmgu9uted4fq}
+      }
       @INPROCEEDINGS{Rokicki1994,
         author = {Tomas Rokicki and Chris J. Myers},
         title = {Automatic Verification of Timed Circuits},
         booktitle = {CAV '94: Proceedings of the 6th International Conference on Computer
       	Aided Verification},
         year = {1994},
         pages = {468--480},
         address = {London, UK},
         publisher = {Springer-Verlag},
         isbn = {3-540-58179-0},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @TECHREPORT{Ronkko1997,
         author = {Ronkko, Mauno and Ravn, Anders P.},
         title = {Switches and Jumps in Hybrid Action Systems},
         year = {1997},
         publisher = {Turku Centre for Computer Science},
         source = {http://www.ncstrl.org:8900/ncstrl/servlet/search?formname=detail\&id=oai%3Ancstrlh%3Atucs_fi%3Ancstrl.tucs.fi%2F%2FTUCS-TR-152}
+      }
       @BOOK{Roscoe1997,
         title = {The Theory and Practice of Concurrency},
         publisher = {Prentice Hall PTR},
         year = {1997},
         author = {Roscoe, A. W. and Hoare, C. A. R. and Bird, Richard},
         address = {Upper Saddle River, NJ, USA},
         isbn = {0136744095}
+      }
       @BOOK{Rumbaugh2004,
         title = {The Unified Modeling Language Reference Manual},
         publisher = {Addison--Wesley},
         year = {2004},
         author = {James Rumbaugh and Ivar Jacobson and Grady Booch},
         edition = {2nd},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{Rumbaugh2004a,
         title = {Unified Modeling Language Reference Manual, The (2nd Edition)},
         publisher = {Pearson Higher Education},
         year = {2004},
         author = {Rumbaugh, James and Jacobson, Ivar and Booch, Grady},
         isbn = {0321245628}
+      }
       @BOOK{Russell2002,
         title = {Artificial Intelligence: A Modern Approach (2nd Edition)},
         publisher = {{Prentice Hall}},
         year = {2002},
         author = {Russell, Stuart J. and Norvig, Peter },
         howpublished = {Hardcover},
         isbn = {0137903952},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Say2003,
         author = {Say, A. C. Cem and Akin, H. Levent},
         title = {Sound and complete qualitative simulation is impossible},
         journal = {Artif. Intell.},
         year = {2003},
         volume = {149},
         pages = {251--266},
         number = {2},
         address = {Essex, UK},
         doi = {http://dx.doi.org/10.1016/S0004-3702(03)00077-8},
         issn = {0004-3702},
         publisher = {Elsevier Science Publishers Ltd.}
+      }
       @INPROCEEDINGS{Schlatte2008,
         author = {Rudolf Schlatte and Bernhard Aichernig and Frank de Boer and Andreas
       	Griesmayer and Einar Broch Johnsen},
         title = {Testing Concurrent Objects with Application-Specific Schedulers},
         year = {2008},
         series = {LNCS},
         publisher = {Springer-Verlag},
         note = {To be published in the proceedings for ICTAC 2008},
         abstract = {In this paper, we propose a novel approach to testing executable models
       	of concurrent objects under application-specific scheduling regimes.
       	Method activations in concurrent objects are modelled as a composition
       	of symbolic automata; this composition expresses all possible interleavings
       	of actions. Scheduler specifications, also modelled as automata,
       	are used to constrain the system execution. Test purposes are expressed
       	as assertions on selected states of the system, and weakest precondition
       	calculation is used to derive the test cases from these test purposes.
       	Our new testing technique is based on the assumption that we have
       	full control over the (application-specific) scheduler, which is
       	the case in our executable models under test. Hence, the enforced
       	scheduling policy becomes an integral part of a test case. This tackles
       	the problem of testing non-deterministic behaviour due to scheduling.},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @TECHREPORT{Sekerinski1996,
         author = {Sekerinski, Emil and Sere, Kaisa},
         title = {A Theory of Prioritizing Composition},
         year = {1996},
         publisher = {Turku Centre for Computer Science},
         source = {http://www.ncstrl.org:8900/ncstrl/servlet/search?formname=detail\&id=oai%3Ancstrlh%3Atucs_fi%3Ancstrl.tucs.fi%2F%2FTUCS-TR-5}
+      }
       @INPROCEEDINGS{Sen2005a,
         author = {Sen, Koushik and Marinov, Darko and Agha, Gul },
         title = {CUTE: a concolic unit testing engine for C},
         booktitle = {ESEC/FSE-13: Proceedings of the 10th European software engineering
       	conference held jointly with 13th ACM SIGSOFT international symposium
       	on Foundations of software engineering},
         year = {2005},
         pages = {263--272},
         address = {New York, NY, USA},
         publisher = {ACM},
         abstract = {In unit testing, a program is decomposed into units which are collections
       	of functions. A part of unit can be tested by generating inputs for
       	a single entry function. The entry function may contain pointer arguments,
       	in which case the inputs to the unit are memory graphs. The paper
       	addresses the problem of automating unit testing with memory graphs
       	as inputs. The approach used builds on previous work combining symbolic
       	and concrete execution, and more specifically, using such a combination
       	to generate test inputs to explore all feasible execution paths.
       	The current work develops a method to represent and track constraints
       	that capture the behavior of a symbolic execution of a unit with
       	memory graphs as inputs. Moreover, an efficient constraint solver
       	is proposed to facilitate incremental generation of such test inputs.
       	Finally, CUTE, a tool implementing the method is described together
       	with the results of applying CUTE to real-world examples of C code.},
         citeulike-article-id = {2236218},
         doi = {10.1145/1081706.1081750},
         isbn = {1595930140},
         keywords = {c, concolic, testing},
         owner = {harald},
         posted-at = {2008-04-15 08:49:28},
         priority = {2},
         timestamp = {2009.09.18},
         url = {http://portal.acm.org/citation.cfm?id=1081750}
+      }
       @ARTICLE{Sims2007,
         author = {Sims, S. and DuVarney, D.C.},
         title = {{Experience report: the reactis validation tool}},
         journal = {Proceedings of the 2007 ACM SIGPLAN international conference on Functional
       	programming},
         year = {2007},
         pages = {137--140},
         owner = {harald},
         publisher = {ACM Press New York, NY, USA},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Slaughter1998,
         author = {Sandra A. Slaughter and Donald E. Harter and Mayuram S. Krishnan},
         title = {Evaluating the cost of software quality},
         journal = {Commun. ACM},
         year = {1998},
         volume = {41},
         pages = {67--73},
         number = {8},
         address = {New York, NY, USA},
         doi = {http://doi.acm.org/10.1145/280324.280335},
         issn = {0001-0782},
         owner = {harald},
         publisher = {ACM},
         timestamp = {2009.09.18}
+      }
       @BOOK{Stewart1977,
         title = {The Foundations of Mathematics},
         publisher = {Oxford University Press},
         year = {1977},
         author = {Ian Stewart and David Tall},
         owner = {harald},
         timestamp = {2010.11.03}
+      }
       @ARTICLE{TaiAug1996,
         author = {Tai, Kuo C. },
         title = {Theory of fault-based predicate testing for computer programs},
         journal = {Software Engineering, Transactions on},
         year = {Aug 1996},
         volume = {22},
         pages = {552--562},
         number = {8},
         abstract = {Predicates appear in both the specification and implementation of
       	a program. One approach to software testing, referred to as predicate
       	testing, is to require certain types of tests for a predicate. In
       	this paper, three fault-based testing criteria are defined for compound
       	predicates, which are predicates with one or more AND/OR operators.
       	BOR (boolean operator) testing requires a set of tests to guarantee
       	the detection of (single or multiple) boolean operator faults, including
       	incorrect AND/OR operators and missing/extra NOT operators. BRO (boolean
       	and relational operator) testing requires a set of tests to guarantee
       	the detection of boolean operator faults and relational operator
       	faults (i.e., incorrect relational operators). BRE (boolean and relational
       	expression) testing requires a set of tests to guarantee the detection
       	of boolean operator faults, relational operator faults, and a type
       	of fault involving arithmetical expressions. It is shown that for
       	a compound predicate with n, n>0, AND/OR operators, at most n+2 constraints
       	are needed for BOR testing and at most 2*n+3 constraints for BRO
       	or BRE testing, where each constraint specifies a restriction on
       	the value of each boolean variable or relational expression in the
       	predicate. Algorithms for generating a minimum set of constraints
       	for BOR, BRO, and BRE testing of a compound predicate are given,
       	and the feasibility problem for the generated constraints is discussed.
       	For boolean expressions that contain multiple occurrences of some
       	boolean variables, how to combine BOR testing with the meaningful
       	impact strategy (Weyuker et al., 1994) is described},
         citeulike-article-id = {2637997},
         doi = {10.1109/32.536956},
         keywords = {arithmetical, bibtex-import, boolean, bor, bre, bro, compound, debugging,
       	expression, expressions, fault-based, faults, feasibility, formal,
       	functions, impact, implementation, meaningful, not, operator, operators,
       	predicate, predicates, problem, program, programming, relational,
       	specification, strategy, testing, theoryandor, variable},
         owner = {harald},
         posted-at = {2008-04-07 16:23:42},
         priority = {2},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/10.1109/32.536956}
+      }
       @ARTICLE{Tai17-21May1993,
         author = {Tai, K. C. },
         title = {Predicate-based test generation for computer programs},
         journal = {Software Engineering, 1993. Proceedings., 15th International Conference
       	on},
         year = {17-21 May 1993},
         pages = {267--276},
         citeulike-article-id = {2637996},
         doi = {10.1109/ICSE.1993.346037},
         keywords = {and, andor, bibtex-import, boolean, compound, correctness, fault-based,
       	functions, operator, operators, predicates, program, relational,
       	simple, strategies, testing},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/00346037.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:42},
         priority = {2},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/10.1109/ICSE.1993.346037}
+      }
       @INPROCEEDINGS{Tan2004,
         author = {Li Tan and Oleg Sokolsky and Insup Lee},
         title = {Specification-based Testing with Linear Temporal Logic},
         booktitle = {Proceedings of IEEE International Conference on Information Reuse
       	and Integration (IRI'04)},
         year = {2004},
         pages = {493--498},
         owner = {gordon},
         timestamp = {2006.02.20}
+      }
       @INPROCEEDINGS{Tiwari2002,
         author = {Tiwari, Ashish and Khanna, Gaurav},
         title = {Series of Abstractions for Hybrid Automata},
         booktitle = {Hybrid Systems: Computation and Control},
         year = {2002},
         editor = {Tomlin, Claire and Greenstreet, Mark},
         volume = {2289},
         series = {Lecture Notes in Computer Science},
         pages = {425-438},
         publisher = {Springer Berlin, Heidelberg},
         affiliation = {SRI International 333 Ravenswood Ave Menlo Park CA USA},
         url = {http://dx.doi.org/10.1007/3-540-45873-5_36}
+      }
       @ARTICLE{Tomlin1998,
         author = {Tomlin, C. and Pappas, G.J. and Sastry, S.},
         title = {Conflict resolution for air traffic management: a study in multiagent
       	hybrid systems},
         journal = {Automatic Control, IEEE Transactions on},
         year = {1998},
         volume = {43},
         pages = {509 -521},
         number = {4},
         month = apr,
         doi = {10.1109/9.664154},
         issn = {0018-9286}
+      }
       @INPROCEEDINGS{Tretmans2008,
         author = {Jan Tretmans},
         title = {Model Based Testing with Labelled Transition Systems},
         booktitle = {Formal Methods and Testing},
         year = {2008},
         editor = {R.M. Hierons and J.P. Bowen and M. Harman},
         volume = {4949},
         series = {Lecture Notes in Computer Science},
         pages = {1--38},
         publisher = {Springer},
         comment = {p},
         file = {tretmans2008model.pdf:tretmans2008model.pdf:PDF},
         owner = {martin},
         timestamp = {2008.03.13}
+      }
       @INPROCEEDINGS{Tretmans1996,
         author = {Tretmans, Jan },
         title = {Test Generation with Inputs, Outputs, and Quiescence},
         booktitle = {TACAs '96: Proceedings of the Second International Workshop on Tools
       	and Algorithms for Construction and Analysis of Systems},
         year = {1996},
         pages = {127--146},
         address = {London, UK},
         publisher = {Springer-Verlag},
         citeulike-article-id = {1467403},
         isbn = {3540610421},
         keywords = {complete, exhaustive, ioconf, sound},
         owner = {harald},
         posted-at = {2008-04-07 15:37:05},
         priority = {0},
         timestamp = {2009.09.18},
         url = {http://portal.acm.org/citation.cfm?id=693775}
+      }
       @ARTICLE{Tretmans1996a,
         author = {Jan Tretmans},
         title = {Test Generation with Inputs, Outputs and Repetitive Quiescence.},
         journal = {Software - Concepts and Tools},
         year = {1996},
         volume = {17},
         pages = {103--120},
         number = {3},
         comment = {p,r},
         file = {tretmans1996testgeneration.pdf:tretmans1996testgeneration.pdf:PDF},
         keywords = {ioco},
         owner = {martin},
         timestamp = {2007.07.31}
+      }
       @INPROCEEDINGS{Tretmans2003,
         author = {Jan Tretmans and Ed Brinksma},
         title = {{TorX}: Automated Model Based Testing},
         booktitle = {Proceedings of the 1st European Conference on Model-Driven Software
       	Engineering},
         year = {2003},
         editor = {A. Hartman and K. Dussa-Zieger},
         pages = {13--25},
         address = {Nurnburg, Germany},
         abstract = {Similar to the TGV-Tool, this tool relaies on the IOCO-Relation for
       	test generation. There are two main differences. The first one is
       	, that TorX does not produce a test case but sends Input-Sequences
       	directly to the IUT while construction the LTS. The second one is
       	that TorX does not use a test purpose but generates the test sequence
       	randomly.},
         comment = {p,r},
         file = {tretmans2003torx.pdf:tretmans2003torx.pdf:PDF},
         filename = {./test\_generation/trej2003-torx.pdf},
         keywords = {Testing, Conformance Test, Test generation, I/O LTS},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{Utting2006,
         title = {Practical Model-Based Testing: A Tools Approach},
         publisher = {Morgan Kaufmann Publishers Inc.},
         year = {2006},
         author = {Utting, Mark and Legeard, Bruno },
         address = {San Francisco, CA, USA},
         citeulike-article-id = {2637985},
         keywords = {bibtex-import, tug},
         owner = {harald},
         posted-at = {2008-04-07 16:23:40},
         priority = {2},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Vanzin2006,
         author = {Daniel D. Vanzin and Ivan L. Martins and Joao Bosco A. Pereira Filho},
         title = {TDE UML Editor - A Success Development Case of a Software Extension},
         booktitle = {ICGSE '06: Proceedings of the IEEE international conference on Global
       	Software Engineering},
         year = {2006},
         pages = {257--258},
         address = {Washington, DC, USA},
         publisher = {IEEE Computer Society},
         isbn = {0-7695-2663-2},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{Warmer1998,
         title = {The {Object Constraint Language}: Precise Modeling with {UML}},
         publisher = {Addison-Wesley},
         year = {1998},
         author = {Jos Warmer and Anneke Kleppe},
         isbn = {0-201-37940-6},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Weiglhofer2008,
         author = {Martin Weiglhofer and Franz Wotawa},
         title = {Random vs. Scenario-Based vs. Fault-Based Testing -- An Industrial
       	Evaluation of Formal Black-Box Testing Methods},
         booktitle = {Proceedings of the 3rd International Conference on Evaluation of
       	Novel Approaches to Software Engineering},
         year = {2008},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @INPROCEEDINGS{Weiglhofer2008a,
         author = {Martin Weiglhofer and Franz Wotawa},
         title = {"{O}n the fly" input output conformance verification},
         booktitle = {Proceedings of the IASTED International Conference on Software Engineering},
         year = {2008},
         address = {Innsbruck, Austria},
         month = {February},
         note = {To appear.},
         comment = {a},
         file = {weiglhofer2008onthefly.pdf:weiglhofer2008onthefly.pdf:PDF},
         owner = {martin},
         timestamp = {2007.10.09}
+      }
       @INPROCEEDINGS{Wong2010,
         author = {Wong, W.E. and Debroy, V. and Surampudi, A. and HyeonJeong Kim and
       	Siok, M.F.},
         title = {Recent Catastrophic Accidents: Investigating How Software was Responsible},
         booktitle = {Secure Software Integration and Reliability Improvement (SSIRI),
 Fourth International Conference on},
         year = {2010},
         pages = {14 -22},
         month = june,
         doi = {10.1109/SSIRI.2010.38},
         keywords = {accident avoidance;causative factor;recent catastrophic accidents;safety-critical
       	software;safety-critical software;}
+      }
       @INPROCEEDINGS{Wotawa2007,
         author = {Franz Wotawa},
         title = {Generating test-cases from qualitative knowledge -- Preliminary report},
         booktitle = {Proceedings of the 21st Annual Workshop on Qualitative Reasoning},
         year = {2007},
         address = {Aberystwyth, U.K.},
         month = {June},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Xie2007,
         author = {Qing Xie and Atif M. Memon},
         title = {Designing and comparing automated test oracles for GUI-based software
       	applications},
         journal = {ACM Trans. Softw. Eng. Methodol.},
         year = {2007},
         volume = {16},
         number = {1},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         ee = {http://doi.acm.org/10.1145/1189748.1189752},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @ARTICLE{Yates1989,
         author = {Yates, D. and Malevris, N. },
         title = {Reducing the effects of infeasible paths in branch testing},
         journal = {SIGSOFT Softw. Eng. Notes},
         year = {1989},
         volume = {14},
         pages = {48--54},
         number = {8},
         address = {New York, NY, USA},
         citeulike-article-id = {2637995},
         doi = {http://doi.acm.org/10.1145/75309.75315},
         keywords = {bibtex-import},
         local-url = {file://localhost/Users/michele/mogentes/bibliography/p48-yates.pdf},
         owner = {harald},
         posted-at = {2008-04-07 16:23:42},
         priority = {2},
         publisher = {ACM},
         timestamp = {2009.09.18},
         url = {http://dx.doi.org/10.1145/75309.75315}
+      }
       @BOOK{Young2005,
         title = {Software Testing and Analysis: Process, Principles and Techniques},
         publisher = {John Wiley \& Sons},
         year = {2005},
         author = {Young, Michal and Pezze, Mauro },
         citeulike-article-id = {2638003},
         keywords = {bibtex-import, coverage, criteriainfeasibility, problem},
         owner = {harald},
         posted-at = {2008-04-07 16:23:44},
         priority = {2},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Alur2003,
         title = {Embedded Software, Third International Conference, EMSOFT 2003, Philadelphia,
       	PA, USA, October 13-15, 2003, Proceedings},
         year = {2003},
         editor = {Rajeev Alur and Insup Lee},
         volume = {2855},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {EMSOFT},
         isbn = {3-540-20223-4},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Arabnia2007,
         title = {Proceedings of the 2007 International Conference on Software Engineering
       	Research {\&} Practice, SERP 2007, Volume II, June 25-28, 2007, Las
       	Vegas Nevada, USA},
         year = {2007},
         editor = {Hamid R. Arabnia and Hassan Reza},
         publisher = {CSREA Press},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {Software Engineering Research and Practice},
         isbn = {1-60132-034-5},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Avrunin2004,
         title = {Proceedings of the ACM/SIGSOFT International Symposium on Software
       	Testing and Analysis, ISSTA 2004, Boston, Massachusetts, USA, July
 -14, 2004},
         year = {2004},
         editor = {George S. Avrunin and Gregg Rothermel},
         publisher = {ACM},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {ISSTA},
         isbn = {1-58113-820-2},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Ball2006a,
         title = {Computer Aided Verification, 18th International Conference, CAV 2006,
       	Seattle, WA, USA, August 17-20, 2006, Proceedings},
         year = {2006},
         editor = {Thomas Ball and Robert B. Jones},
         volume = {4144},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {CAV},
         isbn = {3-540-37406-X},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Beckert2008,
         title = {Tests and Proofs, Second International Conference, TAP 2008, Prato,
       	Italy, April 9-11, 2008. Proceedings},
         year = {2008},
         editor = {Bernhard Beckert and Reiner H{\"a}hnle},
         volume = {4966},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {TAP},
         isbn = {978-3-540-79123-2},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Bemporad2007,
         title = {Hybrid Systems: Computation and Control, 10th International Workshop,
       	HSCC 2007, Pisa, Italy, April 3-5, 2007, Proceedings},
         year = {2007},
         editor = {Alberto Bemporad and Antonio Bicchi and Giorgio C. Buttazzo},
         volume = {4416},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {HSCC},
         isbn = {978-3-540-71492-7},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Berbers2006,
         title = {Proceedings of the 2006 EuroSys Conference, Leuven, Belgium, April
 -21, 2006},
         year = {2006},
         editor = {Yolande Berbers and Willy Zwaenepoel},
         publisher = {ACM},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {EuroSys},
         isbn = {1-59593-322-0},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Bernardo2004,
         title = {Formal Methods for the Design of Real-Time Systems, International
       	School on Formal Methods for the Design of Computer, Communication
       	and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18,
 , Revised Lectures},
         year = {2004},
         editor = {Marco Bernardo and Flavio Corradini},
         volume = {3185},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {SFM},
         isbn = {3-540-23068-8},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Brim2007,
         title = {Formal Methods: Applications and Technology, 11th International Workshop,
       	FMICS 2006 and 5th International Workshop PDMC 2006, Bonn, Germany,
       	August 26-27, and August 31, 2006, Revised Selected Papers},
         year = {2007},
         editor = {Lubos Brim and Boudewijn R. Haverkort and Martin Leucker and Jaco
       	van de Pol},
         volume = {4346},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {FMICS/PDMC},
         isbn = {978-3-540-70951-0},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Broy2005,
         title = {Model-Based Testing of Reactive Systems},
         year = {2005},
         editor = {Manfred Broy and Bengt Jonsson and Joost-Pieter Katoen and Martin
       	Leucker and Alexander Pretschner},
         volume = {3472},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {Model-Based Testing of Reactive Systems},
         isbn = {3-540-26278-4},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{Buxton1970,
         title = {Software Engineering Techniques: Report of a conference sponsored
       	by the NATO Science Committee, Rome, Italy, 27-31 Oct. 1969, Brussels,
       	Scientific Affairs Division, NATO},
         year = {1970},
         editor = {Buxton, J. N. and Randell, B.}
+      }
       @PROCEEDINGS{Cassez2001,
         title = {Modeling and Verification of Parallel Processes, 4th Summer School,
       	MOVEP 2000, Nantes, France, June 19-23, 2000},
         year = {2001},
         editor = {Franck Cassez and Claude Jard and Brigitte Rozoy and Mark Dermot
       	Ryan},
         volume = {2067},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {MOVEP},
         isbn = {3-540-42787-2},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Chechik2009,
         title = {Fundamental Approaches to Software Engineering, 12th International
       	Conference, FASE 2009, Held as Part of the Joint European Conferences
       	on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29,
 . Proceedings},
         year = {2009},
         editor = {Marsha Chechik and Martin Wirsing},
         volume = {5503},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {FASE},
         ee = {http://dx.doi.org/10.1007/978-3-642-00593-0},
         isbn = {978-3-642-00592-3},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Cin2005,
         title = {Dependable Computing - EDCC-5, 5th European Dependable Computing
       	Conference, Budapest, Hungary, April 20-22, 2005, Proceedings},
         year = {2005},
         editor = {Mario Dal Cin and Mohamed Ka{\^a}niche and Andr{\'a}s Pataricza},
         volume = {3463},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {EDCC},
         isbn = {3-540-25723-3},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Damm2007,
         title = {Computer Aided Verification, 19th International Conference, CAV 2007,
       	Berlin, Germany, July 3-7, 2007, Proceedings},
         year = {2007},
         editor = {Werner Damm and Holger Hermanns},
         volume = {4590},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {CAV},
         isbn = {978-3-540-73367-6},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{DangVan2002,
         title = {Specification case studies in RAISE},
         publisher = {Springer-Verlag},
         year = {2002},
         editor = {Dang Van, H. and George, C. and Janowski, T. and Moore, R. },
         address = {London, UK},
         isbn = {1-85233-359-6},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Dershowitz2003,
         title = {Verification: Theory and Practice, Essays Dedicated to Zohar Manna
       	on the Occasion of His 64th Birthday},
         year = {2003},
         editor = {Nachum Dershowitz},
         volume = {2772},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {Verification: Theory and Practice},
         isbn = {3-540-21002-4},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Dacker2003,
         title = {Proceedings of the 2003 ACM SIGPLAN Workshop on Erlang, Uppsala,
       	Sweden, August 29, 2003},
         year = {2003},
         editor = {Bjarne D{\"a}cker and Thomas Arts},
         publisher = {ACM},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {Erlang Workshop},
         isbn = {1-58113-772-9},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Fitzgerald2005,
         title = {FM 2005: Formal Methods, International Symposium of Formal Methods
       	Europe, Newcastle, UK, July 18-22, 2005, Proceedings},
         year = {2005},
         editor = {John Fitzgerald and Ian J. Hayes and Andrzej Tarlecki},
         volume = {3582},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {FM},
         isbn = {3-540-27882-6},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Garavel2003,
         title = {Tools and Algorithms for the Construction and Analysis of Systems,
 th International Conference, TACAS 2003, Held as Part of the Joint
       	European Conferences on Theory and Practice of Software, ETAPS 2003,
       	Warsaw, Poland, April 7-11, 2003, Proceedings},
         year = {2003},
         editor = {Hubert Garavel and John Hatcliff},
         volume = {2619},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {TACAS},
         isbn = {3-540-00898-5},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Grabowski2005,
         title = {Formal Approaches to Software Testing, 4th International Workshop,
       	FATES 2004, Linz, Austria, September 21, 2004, Revised Selected Papers},
         year = {2005},
         editor = {Jens Grabowski and Brian Nielsen},
         volume = {3395},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {FATES},
         isbn = {3-540-25109-X},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Grieskamp2000,
         title = {Integrated Formal Methods, Second International Conference, IFM 2000,
       	Dagstuhl Castle, Germany, November 1-3, 2000, Proceedings},
         year = {2000},
         editor = {Wolfgang Grieskamp and Thomas Santen and Bill Stoddart},
         volume = {1945},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {IFM},
         isbn = {3-540-41196-8},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Grieskamp2006a,
         title = {Formal Approaches to Software Testing, 5th International Workshop,
       	FATES 2005, Edinburgh, UK, July 11, 2005, Revised Selected Papers},
         year = {2006},
         editor = {Wolfgang Grieskamp and Carsten Weise},
         volume = {3997},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {FATES},
         isbn = {3-540-34454-3},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Halbwachs2005,
         title = {Tools and Algorithms for the Construction and Analysis of Systems,
 th International Conference, TACAS 2005, Held as Part of the Joint
       	European Conferences on Theory and Practice of Software, ETAPS 2005,
       	Edinburgh, UK, April 4-8, 2005, Proceedings},
         year = {2005},
         editor = {Nicolas Halbwachs and Lenore D. Zuck},
         volume = {3440},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {TACAS},
         isbn = {3-540-25333-5},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Havelund2006,
         title = {Formal Approaches to Software Testing and Runtime Verification, First
       	Combined International Workshops, FATES 2006 and RV 2006, Seattle,
       	WA, USA, August 15-16, 2006, Revised Selected Papers},
         year = {2006},
         editor = {Klaus Havelund and Manuel N{\'u}{\~n}ez and Grigore Rosu and Burkhart
       	Wolff},
         volume = {4262},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {FATES/RV},
         isbn = {3-540-49699-8},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Hierons2008,
         title = {Formal Methods and Testing, An Outcome of the FORTEST Network, Revised
       	Selected Papers},
         year = {2008},
         editor = {Robert M. Hierons and Jonathan P. Bowen and Mark Harman},
         volume = {4949},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {Formal Methods and Testing},
         isbn = {978-3-540-78916-1},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Juels2006,
         title = {Proceedings of the 13th ACM Conference on Computer and Communications
       	Security, CCS 2006, Alexandria, VA, USA, Ioctober 30 - November 3,
 },
         year = {2006},
         editor = {Ari Juels and Rebecca N. Wright and Sabrina De Capitani di Vimercati},
         publisher = {ACM},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {ACM Conference on Computer and Communications Security},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Karras2007,
         title = {International Conference on Software Engineering Theory and Practice,
       	SETP-07, Orlando, Florida, USA, July 9-12 2007},
         year = {2007},
         editor = {Dimitris A. Karras and Daming Wei and Jaroslav Zendulka},
         publisher = {ISRST},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {SETP},
         isbn = {978-0-9727412-6-2},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Katoen2002,
         title = {Tools and Algorithms for the Construction and Analysis of Systems,
 th International Conference, TACAS 2002, Held as Part of the Joint
       	European Conference on Theory and Practice of Software, ETAPS 2002,
       	Grenoble, France, April 8-12, 2002, Proceedings},
         year = {2002},
         editor = {Joost-Pieter Katoen and Perdita Stevens},
         volume = {2280},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {TACAS},
         isbn = {3-540-43419-4},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Kaagstrom1998,
         title = {Applied Parallel Computing, Large Scale Scientific and Industrial
       	Problems, 4th International Workshop, PARA '98, Ume{\aa}, Sweden,
       	June 14-17, 1998, Proceedings},
         year = {1998},
         editor = {Bo K{\aa}gstr{\"o}m and Jack Dongarra and Erik Elmroth and Jerzy
       	Wasniewski},
         volume = {1541},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {PARA},
         isbn = {3-540-65414-3},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Lamsweerde1991,
         title = {ESEC '91, 3rd European Software Engineering Conference, Milan, Italy,
       	October 21-24, 1991, Proceedings},
         year = {1991},
         editor = {Axel van Lamsweerde and Alfonso Fugetta},
         volume = {550},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {ESEC},
         isbn = {3-540-54742-8},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Leucker2009,
         title = {Theoretical Aspects of Computing - ICTAC 2009, 6th International
       	Colloquium, Kuala Lumpur, Malaysia, August 16-20, 2009. Proceedings},
         year = {2009},
         editor = {Martin Leucker and Carroll Morgan},
         volume = {5684},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {ICTAC},
         ee = {http://dx.doi.org/10.1007/978-3-642-03466-4},
         isbn = {978-3-642-03465-7},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Misra2006,
         title = {FM 2006: Formal Methods, 14th International Symposium on Formal Methods,
       	Hamilton, Canada, August 21-27, 2006, Proceedings},
         year = {2006},
         editor = {Jayadev Misra and Tobias Nipkow and Emil Sekerinski},
         volume = {4085},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {FM},
         isbn = {3-540-37215-6},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Mosses1995,
         title = {TAPSOFT'95: Theory and Practice of Software Development, 6th International
       	Joint Conference CAAP/FASE, Aarhus, Denmark, May 22-26, 1995, Proceedings},
         year = {1995},
         editor = {Peter D. Mosses and Mogens Nielsen and Michael I. Schwartzbach},
         volume = {915},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {TAPSOFT},
         isbn = {3-540-59293-8},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Petrenko2007,
         title = {Testing of Software and Communicating Systems, 19th IFIP TC6/WG6.1
       	International Conference, TestCom 2007, 7th International Workshop,
       	FATES 2007, Tallinn, Estonia, June 26-29, 2007, Proceedings},
         year = {2007},
         editor = {Alexandre Petrenko and Margus Veanes and Jan Tretmans and Wolfgang
       	Grieskamp},
         volume = {4581},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {TestCom/FATES},
         isbn = {978-3-540-73065-1},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Rafiq1994,
         title = {Protocol Test Systems, VI, Proceedings of the IFIP TC6/WG6.1 Sixth
       	International Workshop on Protocol Test systems, Pau, France, 28-30
       	September, 1993},
         year = {1994},
         editor = {Omar Rafiq},
         volume = {C-19},
         series = {IFIP Transactions},
         publisher = {North-Holland},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {Protocol Test Systems},
         isbn = {0-444-81697-6},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Ramakrishnan2008,
         title = {Tools and Algorithms for the Construction and Analysis of Systems,
 th International Conference, TACAS 2008, Held as Part of the Joint
       	European Conferences on Theory and Practice of Software, ETAPS 2008,
       	Budapest, Hungary, March 29-April 6, 2008. Proceedings},
         year = {2008},
         editor = {C. R. Ramakrishnan and Jakob Rehof},
         volume = {4963},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {TACAS},
         isbn = {978-3-540-78799-0},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Reed2001,
         title = {SDL 2001: Meeting UML, 10th International SDL Forum Copenhagen, Denmark,
       	June 27-29, 2001, Proceedings},
         year = {2001},
         editor = {Rick Reed and Jeanne Reed},
         volume = {2078},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {SDL Forum},
         isbn = {3-540-42281-1},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Robby2008,
         title = {30th International Conference on Software Engineering (ICSE 2008),
       	Leipzig, Germany, May 10-18, 2008, Companion Volume},
         year = {2008},
         editor = {Robby},
         publisher = {ACM},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {ICSE Companion},
         isbn = {978-1-60558-079-1},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Robby2008a,
         title = {30th International Conference on Software Engineering (ICSE 2008),
       	Leipzig, Germany, May 10-18, 2008},
         year = {2008},
         editor = {Robby},
         publisher = {ACM},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {ICSE},
         isbn = {978-1-60558-079-1},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Sangiorgi1998,
         title = {CONCUR '98: Concurrency Theory, 9th International Conference, Nice,
       	France, September 8-11, 1998, Proceedings},
         year = {1998},
         editor = {Davide Sangiorgi and Robert de Simone},
         volume = {1466},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {CONCUR},
         isbn = {3-540-64896-8},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Sarkar2005,
         title = {Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language
       	Design and Implementation, Chicago, IL, USA, June 12-15, 2005},
         year = {2005},
         editor = {Vivek Sarkar and Mary W. Hall},
         publisher = {ACM},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {PLDI},
         isbn = {1-59593-056-6},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Sherratt2003,
         title = {Telecommunications and beyond: The Broader Applicability of SDL and
       	MSC, Third International Workshop, SAM 2002, Aberystwyth, UK, June
 -26, 2002. Revised Papers},
         year = {2003},
         editor = {Edel Sherratt},
         volume = {2599},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {SAM},
         isbn = {3-540-00877-2},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @BOOK{Tretmans2007,
         title = {Tangram: Model-based integration and testing of complex high-tech
       	systems},
         publisher = {Embedded Systems Institute, Eindhoven, The Netherlands},
         year = {2007},
         editor = {Jan Tretmans},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Uyar2006,
         title = {Testing of Communicating Systems, 18th IFIP TC6/WG6.1 International
       	Conference, TestCom 2006, New York, NY, USA, May 16-18, 2006, Proceedings},
         year = {2006},
         editor = {M. {\"U}mit Uyar and Ali Y. Duale and Mariusz A. Fecko},
         volume = {3964},
         series = {Lecture Notes in Computer Science},
         publisher = {Springer},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {TestCom},
         isbn = {3-540-34184-6},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{Wermelinger2005,
         title = {Proceedings of the 10th European Software Engineering Conference
       	held jointly with 13th ACM SIGSOFT International Symposium on Foundations
       	of Software Engineering, 2005, Lisbon, Portugal, September 5-9, 2005},
         year = {2005},
         editor = {Michel Wermelinger and Harald Gall},
         publisher = {ACM},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {ESEC/SIGSOFT FSE},
         isbn = {1-59593-014-0},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @MISC{,
         title = {{T-VEC Tester for Simulink homepage}},
         howpublished = {\url{http://www.t-vec.com/solutions/simulink.php}},
         note = {(checked Aug 10, 2009)},
         key = {t-vec-homepage},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @MISC{,
         title = {{Simulink Design Verifier homepage}},
         howpublished = {\url{http://www.mathworks.com/products/sldesignverifier/}},
         note = {(checked Aug 10, 2009)},
         key = {simulink-design-verifier-homepage},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @MISC{,
         title = {{SCADE} product page},
         howpublished = {\url{http://www.esterel-technologies.com/products/scade-suite/}},
         note = {(checked Aug 10, 2009)},
         key = {scade-homepage},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @MISC{,
         title = {{MaTeLo Product Page}},
         howpublished = {\url{http://www.all4tec.net/index.php/All4tec/matelo-product.html}},
         note = {(checked Aug 5, 2009)},
         key = {MaTeLo},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @MISC{,
         title = {{BEACON Tester homepage}},
         howpublished = {\url{http://www.adi.com/products\_be\_bss\_te.htm}},
         note = {(checked Aug 10, 2009)},
         key = {beacon-homepage},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @MISC{,
         title = {{IBM Rational Tau product page}},
         howpublished = {\url{http://www.telelogic.com/products/tau/}},
         note = {(checked August 5, 2009)},
         key = {tautoolset},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{2007,
         title = {2007 IEEE Symposium on Security and Privacy (S{\&}P 2007), 20-23
       	May 2007, Oakland, California, USA},
         year = {2007},
         publisher = {IEEE Computer Society},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {IEEE Symposium on Security and Privacy},
         key = {IEEE},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @MISC{2006,
         title = {Standard ECMA--335, Common Language Infrastructure (CLI)},
         month = {June},
         year = {2006},
         key = {ECMA},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{2006a,
         title = {Proceedings of the Canadian Conference on Electrical and Computer
       	Engineering, CCECE 2007, May 7, 10, 2006, Ottawa Congress Centre,
       	Ottawa, Canada},
         year = {2006},
         publisher = {IEEE},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {CCECE},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{2004,
         title = {10th IEEE Real-Time and Embedded Technology and Applications Symposium
       	(RTAS 2004), 25-28 May 2004, Toronto, Canada},
         year = {2004},
         publisher = {IEEE Computer Society},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {IEEE Real-Time and Embedded Technology and Applications Symposium},
         isbn = {0-7695-2148-7},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{2003,
         title = {3rd International Conference on Quality Software (QSIC 2003), 6-7
       	November 2003, Dallas, TX, USA},
         year = {2003},
         publisher = {IEEE Computer Society},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {QSIC},
         isbn = {0-7695-2015-4},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{2002,
         title = {8th International Conference on Engineering of Complex Computer Systems
       	(ICECCS 2002), 2-4 December 2002, Greenbelt, MD, USA},
         year = {2002},
         publisher = {IEEE Computer Society},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {ICECCS},
         isbn = {0-7695-1757-9},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @PROCEEDINGS{1998,
         title = {2nd Workshop on Industrial-Strength Formal Specification Techniques
       	(WIFT '98), October 20-23, 1998, Boca Raton, FL, USA},
         year = {1998},
         publisher = {IEEE Computer Society},
         bibsource = {DBLP, http://dblp.uni-trier.de},
         booktitle = {WIFT},
         isbn = {0-7695-0081-1},
         owner = {harald},
         timestamp = {2009.09.18}
+      }
       @comment{jabref-meta: selector_publisher:}
       @comment{jabref-meta: selector_author:}
       @comment{jabref-meta: selector_journal:}
       @comment{jabref-meta: selector_keywords:}

Project

General

Profile

OoasTools

root / branches / compiler / cSharp / ooasCompiler / doc / papers.bib @ 3