Project

General

Profile

Download (211 KB) Statistics
| Revision:

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

% 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,
17th 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
20+ 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
1999},
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:
2005-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:
2005-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),
2010 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
11-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
18-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,
2004, 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,
2009. 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,
9th 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,
11th 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,
2006},
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,
8th 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,
14th 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
24-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:}

(3-3/3)