these.bib

@MISC{SystemCXML,
  AUTHOR = {Deepak Matthaikutty and David Berner and Hiren Patel and Sandeep Shukla},
  TITLE = {{SystemCXML}},
  NOTE = {{\texttt{http://systemcxml.sourceforge.net/}}}
}

@MISC{doxygen,
  AUTHOR = {Dimitri van Heesch},
  TITLE = {Doxygen},
  NOTE = {{\texttt{http://www.doxygen.org}}}
}

@MISC{EDG,
  AUTHOR = {{Edison Design Group}},
  TITLE = {Compiler Front Ends},
  NOTE = {{\texttt{http://www.edg.com/}}}
}

@MISC{underc,
  AUTHOR = {Steve Donovan},
  TITLE = {The {UnderC} Development Project},
  NOTE = {{\texttt{http://home.mweb.co.za/sd/sdonovan/underc.html}}}
}

@MISC{ncsc,
  AUTHOR = {{Cadence Design Systems}},
  TITLE = {{NC-SystemC}},
  NOTE = {{\\ \texttt{http://www.cadence.com/products/functional\_ver/nc-systemc/}}}
}

@MISC{AccurateC,
  AUTHOR = {{Actis Design, LLC}},
  TITLE = {{AccurateC\texttrademark\ Rule Checker}},
  NOTE = {{\texttt{http://www.actisdesign.com/}}}
}

@MISC{heuzeroth02combining,
  AUTHOR = {D. Heuzeroth and T. Holl and W. L{\"o}we},
  TITLE = {Combining static and dynamic analyses to detect interaction patterns},
  NOTE = { In IDPT, 2002. (submitted to). Welf L{\"o}we and Markus Noga},
  YEAR = {2002}
}

@INPROCEEDINGS{riva.rodriguez:combining,
  AUTHOR = {Claudio Riva and Jordi Vidal Rodriguez},
  TITLE = {Combining Static and Dynamic Views for Architecture
                 Reconstruction},
  BOOKTITLE = {European Conference on Software Maintenance and
                 Reengineering},
  PAGES = {47--56},
  YEAR = {2002},
  PUBLISHER = {IEEE Computer Society Press},
  FILE = {riva-iwpc-2002.pdf},
  ABSTRACT = {Static analysis aims at recovering the structure of a
                 software system, while dynamic analysis focuses on its
                 run time behaviour. We propose a technique for
                 combining the analysis of static and dynamic
                 architectural information to support the task of
                 architecture reconstruction. The approach emphasises
                 the correct choice of architecturally significant
                 concepts for the reconstruction process and relies on
                 abstraction techniques for their manipulation. The
                 technique allows the software architect to create a set
                 of architectural views valuable for the architecture
                 description of the system.To support our technique, we
                 outline an environment that relies on hierarchical
                 typed directed graphs to show the system's structure
                 and message sequence charts for its behaviour. The main
                 features of the environment are: visualisation of
                 static and dynamic views, synchronisation of
                 abstractions performed on the views, scripting support
                 and management of the use cases. The approach and the
                 environment are demonstrated with an example.},
  KEYWORDS = {Software Architecture, Reverse Engineering, MSC,
                 Dynamic Analysis, Architecture Reconstruction},
  TARGET = {system decomposition and interaction},
  SOURCE = {static dependencies and program traces},
  MAPPING = {extracted information is presented as Prolog facts;
                 the information is then abstracted by composition rules
                 and view selection; composition rules: part-of relation
                 is added through Prolog clauses which are specified by
                 the human analyst; view selection: (1) definition of a
                 grouping relationship that describes the hierarchy (2)
                 definition of the set of relationships of the graph (3)
                 computing the transitive closure (4) create the graph;
                 the information is visualized by Rigi as hierarchical
                 graph; dynamic information is gathered where the static
                 information gathered earlier drives the choice of the
                 correct instrumentation of the system; the static and
                 dynamic views are traversed}
}

@BOOK{Aho:CPT86,
  AUTHOR = {Alfred V. Aho and Ravi Sethi and Jeffrey D. Ullman},
  TITLE = {Compilers --- Prin\-ci\-ples, Techniques, and
                 Tools},
  PUBLISHER = {Ad{\-d}i{\-s}on-Wes{\-l}ey},
  ADDRESS = {Reading, MA, USA},
  PAGES = {x + 796},
  YEAR = {1986},
  ISBN = {0-201-10088-6},
  LCCN = {QA76.76.C65 A371 1986},
  BIBDATE = {Tue Dec 14 22:33:59 1993}
}

@MISC{spirit,
  AUTHOR = {{SPIRIT Consortium}},
  NOTE = {\texttt{http://www.spiritconsortium.com/}}
}

@MISC{cocentric,
  AUTHOR = {{Synopsys Inc.}},
  TITLE = {{CoCentric} {System} {Studio}.},
  NOTE = {{\\ \small\texttt{http://www.synopsys.com/products/cocentric\_studio/cocentric\_studio.html}}}
}

@MISC{systemperl,
  AUTHOR = {Wilson Snyder},
  TITLE = {{SystemPerl} Home Page},
  NOTE = {\texttt{http://www.veripool.com/systemperl.html}}
}

@INPROCEEDINGS{parsyc,
  AUTHOR = {Görschwin Fey and Daniel Große and Tim Cassens and
                  Christian Genz and Tim Warode and Rolf Drechsler},
  BOOKTITLE = {Synthesis And System Integration of Mixed Information technologies},
  YEAR = 2004,
  TITLE = {{ParSyC}: An Efficient {SystemC} Parser},
  NOTE = {{\footnotesize \texttt{http://www.informatik.uni-bremen.de/agram/doc/work/04sasimi\_parsyc.pdf}}}
}

@MISC{kascpar,
  AUTHOR = {{FZI Forschungszentrum Informatik, Department of Microelectronic System Design}},
  TITLE = {{KaSCPar} - Karlsruhe {SystemC} Parser Suite},
  NOTE = {\texttt{http://www.fzi.de/sim/kascpar.html}}
}

@MISC{sc2v,
  AUTHOR = {Javier Castillo Villar},
  TITLE = {sc2v: {SystemC} to Verilog Synthesizable Subset Translator},
  NOTE = {\texttt{http://www.opencores.org/projects.cgi/web/sc2v/overview}}
}

@MISC{drechsler-reachability,
  AUTHOR = {Rolf Drechsler and Daniel Große},
  TITLE = {Formal Verification of LTL Formulas for SystemC Designs},
  NOTE = {{\scriptsize\texttt{http://www.informatik.uni-bremen.de/grp/ag-ram/doc/konf/iscas03\_verification\_systemc.pdf}}}
}

@MANUAL{systemc-lrm,
  TITLE = {{SystemC} v2.0.1 Language Reference Manual},
  ORGANIZATION = {Open SystemC Initiative},
  YEAR = 2003,
  NOTE = {\texttt{http://www.systemc.org/}}
}

@ARTICLE{lesar:tse,
  AUTHOR = {N. Halbwachs and F. Lagnier and C. Ratel },
  TITLE = {Programming and Verifying Critical Systems
by Means of the Synchronous Data-Flow Programming Language {\sc Lustre}},
  JOURNAL = {IEEE Transactions on Software
Engineering, Special Issue on the Specification and
Analysis of Real-Time Systems},
  MONTH = SEP,
  YEAR = 1992
}

@ARTICLE{jeannet03a,
  AUTHOR = {B. Jeannet},
  TITLE = {Dynamic Partitioning In Linear Relation Analysis. Application To The Verification Of Reactive Systems},
  JOURNAL = {Formal Methods in System Design},
  VOLUME = {23},
  NUMBER = {1},
  PAGES = {5--37},
  PUBLISHER = {Kluwer},
  MONTH = {July},
  YEAR = {2003}
}

@PHDTHESIS{jeannet00b,
  AUTHOR = {Jeannet, B.},
  TITLE = {partitionnement Dynamique dans l'Analyse de Relations Linéraires et Application à la Vérification de Programmes Synchrones},
  SCHOOL = {Institut National Polytechnique de Grenoble},
  MONTH = {September},
  YEAR = {2000}
}

@INPROCEEDINGS{Lustre-rtss85,
  AUTHOR = {J-L. Bergerand and P. Caspi and N. Halbwachs and D. Pilaud and E.
Pilaud },
  TITLE = {Outline of a Real Time Data-Flow Language },
  BOOKTITLE = { Real Time Systems Symposium},
  ADDRESS = {San Diego},
  MONTH = SEP,
  YEAR = {1985}
}

@ARTICLE{clarke86,
  AUTHOR = {E. M. Clarke  and E. A.  Emerson  and A. P.  Sistla  },
  TITLE = {Automatic verification of finite-state concurrent systems using temporal logic specifications },
  JOURNAL = {ACM TOPLAS},
  VOLUME = 8,
  NUMBER = 2,
  YEAR = 1986
}

@INPROCEEDINGS{cesar1,
  AUTHOR = {J. P. Queille  and J.  Sifakis  },
  TITLE = {Specification and Verification of Concurrent Systems in Cesar},
  BOOKTITLE = {International Symposium on Programming},
  PUBLISHER = {LNCS 137, Springer Verlag},
  MONTH = APR,
  YEAR = 1982
}

@INBOOK{kluwer,
  AUTHOR = {W. M\"uler and W. Rosentiel and J. Ruf},
  TITLE = {{SystemC} Methodologies and Applications},
  CHAPTER = 2,
  PUBLISHER = {Kluwer},
  YEAR = 2003
}

@INPROCEEDINGS{Balarin2002,
  AUTHOR = {Felice Balarin and Luciano Lavagno and Claudio Passerone and
Alberto L. Sangiovanni-Vincentelli and Marco Sgroi and Yosinori Watanabe},
  TITLE = {Modeling and Designing Heterogeneous Systems},
  BOOKTITLE = {Concurrency and Hardware Design, Advances in Petri Nets},
  YEAR = {2002},
  ISBN = {3-540-00199-9},
  PAGES = {228--273},
  PUBLISHER = {Springer-Verlag}
}

@MISC{easy,
  AUTHOR = {{ARM Limited}},
  TITLE = {{AHB Example Amba SYstem} technical reference manual},
  YEAR = {{\texttt{http://www.arm.com/pdfs/DDI0170A.zip}}}
}

@UNPUBLISHED{EASY-tlm-st,
  AUTHOR = {Jim-Moi WONG and Jean-Philippe STRASSEN},
  TITLE = {{EASY} Platform},
  NOTE = {STMicroelectronics confidential},
  MONTH = {May},
  YEAR = 2004
}

@INPROCEEDINGS{Godefroid:1997:MCP,
  AUTHOR = {Patrice Godefroid},
  TITLE = {Model checking for programming languages using
                 {VeriSoft}},
  EDITOR = {{ACM}},
  BOOKTITLE = {Conference record of {POPL} '97, the 24th {ACM}
                 {SIGPLAN-SIGACT} Symposium on Principles of Programming
                 Languages: papers presented at the symposium, Paris,
                 France, 15--17 January 1997},
  PUBLISHER = {ACM Press},
  ADDRESS = {New York, NY, USA},
  ISBN = {0-89791-853-3},
  PAGES = {174--186},
  YEAR = {1997},
  BIBDATE = {Mon May 3 12:56:11 MDT 1999},
  URL = {http://www.acm.org:80/pubs/citations/proceedings/plan/263699/p174-godefroid/},
  ACKNOWLEDGEMENT = ACK-NHFB,
  KEYWORDS = {algorithms; design; languages; measurement;
                 performance; theory; verification},
  SUBJECT = {{\bf F.4.1} Theory of Computation, MATHEMATICAL LOGIC
                 AND FORMAL LANGUAGES, Mathematical Logic, Model theory.
                 {\bf D.3.2} Software, PROGRAMMING LANGUAGES, Language
                 Classifications. {\bf F.3.2} Theory of Computation,
                 LOGICS AND MEANINGS OF PROGRAMS, Semantics of
                 Programming Languages. {\bf D.2.4} Software, SOFTWARE
                 ENGINEERING, Software/Program Verification, Correctness
                 proofs.}
}

@TECHREPORT{ucsb_cs:TR-1999-33,
  AUTHOR = {T. Bultan},
  TITLE = {{BDD} vs. Constraint-Based Model Checking: An
                 Experimental Evaluation for Asynchronous Concurrent
                 Systems},
  INSTITUTION = {University of California, Santa Barbara, Computer
                 Science},
  NUMBER = {ucsb_cs:TR-1999-33},
  YEAR = {1999},
  MONTH = OCT # {~6},
  URL = {http://www.cs.ucsb.edu/research/trcs/docs/1999-33.ps;
                 http://www.cs.ucsb.edu/research/trcs/abstracts/1999-33.shtml},
  KEYWORDS = {symbolic model checking, BDDs, constraint
                 representations, Presburger arithmetic},
  ABSTRACT = {BDD-based symbolic model checking has been applied to
                 a wide range of applications. Recently,
                 constraint-based approaches, which use arithmetic
                 constraints as a symbolic representation, have been
                 used in symbolic model checking of infinite-state
                 systems. We argue that use of constraint-based model
                 checking is not limited to infinite-state systems. It
                 can also be an efficient alternative to BDD-based model
                 checking for systems with integer variables that have
                 large domains. In this paper we compare the performance
                 of BDD-based model checker SMV to the performance of
                 our constraint-based model checker on verification of
                 several asynchronous concurrent systems. The results
                 indicate that constraint-based model checking is a
                 viable option for verification of asynchronous
                 concurrent systems that require more than 5 boolean
                 variables to encode each integer variable.}
}

@ARTICLE{bultan-action-language,
  TITLE = {Action Language: {A} Specification Language for Model
                 Checking Reactive Systems},
  AUTHOR = {Tevfik Bultan},
  YEAR = {2000},
  MONTH = MAR,
  ABSTRACT = {We present a specification language called Action
                 Language for model checking software specifications.
                 Action Language forms an interface between transition
                 system models that a model checker generates and high
                 level specification languages such as Statecharts, RSML
                 and SCR---similar to an assembly language between a
                 microprocessor and a programming language. We show that
                 Action Language translations of Statecharts and SCR
                 specifications are compact and they preserve the
                 structure of the original specification. Action
                 Language allows specification of both synchronous and
                 asynchronous systems. It also supports modular
                 specifications to enable compositional model checking.
                 Keywords Reactive systems, specification languages,
                 model checking. 1 INTRODUCTION Developing reliable
                 software for reactive systems is one of the most
                 challenging goals in information technology. A reactive
                 system is one which interacts with its environment
                 continuously without terminating [22]. Typical examples
                 ar...},
  CITESEER-ISREFERNCEDBY = {oai:CiteSeerPSU:389243;
                 oai:CiteSeerPSU:109863; oai:CiteSeerPSU:137659;
                 oai:CiteSeerPSU:130011; oai:CiteSeerPSU:88083;
                 oai:CiteSeerPSU:35198; oai:CiteSeerPSU:125375;
                 oai:CiteSeerPSU:372499; oai:CiteSeerPSU:75055},
  CITESEER-REFERENCES = {oai:CiteSeerPSU:313186},
  ANNOTE = {The Pennsylvania State University CiteSeer Archives},
  LANGUAGE = {en},
  OAI = {oai:CiteSeerPSU:298515},
  RIGHTS = {unrestricted},
  SUBJECT = {Tevfik Bultan Action Language: A Specification
                 Language for Model Checking Reactive Systems},
  URL = {http://citeseer.ist.psu.edu/298515.html;
                 http://www.cs.ucsb.edu/~bultan/publications/icse00.ps}
}

@PHDTHESIS{oai:xtcat.oclc.org:OCLCNo/ocm40966554,
  TITLE = {Automated symbolic analysis of reactive systems},
  AUTHOR = {Tevfik Bultan and},
  YEAR = {1998},
  ANNOTE = {University of Maryland (College Park; Md.).--Dept. of
                 Computer Science.},
  DESCRIPTION = {Thesis research directed by Dept. of Computer
                 Science.; Thesis (Ph. D.)--University of Maryland,
                 College Park, Md., 1998.; Includes bibliographical
                 references (leaves 145-160).},
  OAI = {oai:xtcat.oclc.org:OCLCNo/ocm40966554},
  SCHOOL = {research directed by Dept. of Computer Science},
  SUBJECT = {System analysis.; Infinite matrices.; Software
                 engineering.}
}

@ARTICLE{oai:CiteSeerPSU:8069,
  TITLE = {Composite Model Checking with Type Specific Symbolic
                 Encodings},
  AUTHOR = {Richard Gerber and Tevfik Bultan},
  YEAR = {1998},
  MONTH = MAR # {~13},
  ABSTRACT = {We present a new symbolic model checking technique,
                 which analyzes temporal properties in multityped
                 transition systems. Specifically, the method uses
                 multiple type-specific data encodings to represent
                 system states, and it carries out fixpoint computations
                 via the corresponding type-specific symbolic
                 operations. In essence, different symbolic encodings
                 are unified into one composite model checker. Any
                 type-specific language can be included in this
                 framework -- provided that the language is closed under
                 Boolean connectives, propositions can be checked for
                 satisfiability, and relational images can be computed.
                 Our technique relies on conjunctive partitioning of
                 transition relations of atomic events based on variable
                 types involved, which allows independent computation of
                 one-step pre- and post-conditions for each variable
                 type. In this paper we demonstrate the effectiveness of
                 our method on a nontrivial data-transfer protocol,
                 which contains a mixture of integer and Boolean-valued
                 varia...},
  CITESEER-ISREFERNCEDBY = {oai:CiteSeerPSU:225571;
                 oai:CiteSeerPSU:69777; oai:CiteSeerPSU:57477;
                 oai:CiteSeerPSU:123689; oai:CiteSeerPSU:94134;
                 oai:CiteSeerPSU:170759; oai:CiteSeerPSU:385909;
                 oai:CiteSeerPSU:478550; oai:CiteSeerPSU:322541;
                 oai:CiteSeerPSU:206357; oai:CiteSeerPSU:415119;
                 oai:CiteSeerPSU:136148; oai:CiteSeerPSU:148899;
                 oai:CiteSeerPSU:383028; oai:CiteSeerPSU:145778;
                 oai:CiteSeerPSU:39430; oai:CiteSeerPSU:14969;
                 oai:CiteSeerPSU:181416; oai:CiteSeerPSU:118811;
                 oai:CiteSeerPSU:242379; oai:CiteSeerPSU:387249;
                 oai:CiteSeerPSU:325985; oai:CiteSeerPSU:2522;
                 oai:CiteSeerPSU:66196; oai:CiteSeerPSU:206244;
                 oai:CiteSeerPSU:183750; oai:CiteSeerPSU:295272;
                 oai:CiteSeerPSU:484; oai:CiteSeerPSU:42530;
                 oai:CiteSeerPSU:122641; oai:CiteSeerPSU:32847;
                 oai:CiteSeerPSU:155640},
  CITESEER-REFERENCES = {oai:CiteSeerPSU:17507; oai:CiteSeerPSU:295968;
                 oai:CiteSeerPSU:311874; oai:CiteSeerPSU:40391;
                 oai:CiteSeerPSU:140292; oai:CiteSeerPSU:19422;
                 oai:CiteSeerPSU:220337; oai:CiteSeerPSU:281159;
                 oai:CiteSeerPSU:105376; oai:CiteSeerPSU:284612},
  ANNOTE = {The Pennsylvania State University CiteSeer Archives},
  LANGUAGE = {en},
  OAI = {oai:CiteSeerPSU:8069},
  RIGHTS = {unrestricted},
  SUBJECT = {Richard Gerber,Tevfik Bultan Composite Model Checking
                 with Type Specific Symbolic Encodings},
  URL = {http://citeseer.ist.psu.edu/8069.html;
                 http://www.cs.umd.edu/users/bultan/publications/composite.ps.gz}
}

@TECHREPORT{ucsb_cs:TR-1999-02,
  AUTHOR = {Richard Gerber Tevfik Bultan and Christopher League},
  TITLE = {Composite Model Checking: Verification with
                 Type-Specific Symbolic Representations},
  INSTITUTION = {University of California, Santa Barbara, Computer
                 Science},
  NUMBER = {ucsb_cs:TR-1999-02},
  YEAR = {1999},
  MONTH = JAN # {~2},
  URL = {http://www.cs.ucsb.edu/research/trcs/docs/1999-02.ps;
                 http://www.cs.ucsb.edu/research/trcs/abstracts/1999-02.shtml},
  KEYWORDS = {Symbolic model checking, computer aided verification,
                 software specifications},
  ABSTRACT = {In recent years, there has been a surge of progress in
                 automated verification methods based on state
                 exploration. In areas like hardware design, these
                 technologies are rapidly augmenting key phases of
                 testing and validation. To date, one of the most
                 successful of these methods has been symbolic model
                 checking, in which large finite-state machines are
                 encoded into compact data structures such as binary
                 decision diagrams (BDDs) -- and are then checked for
                 safety and liveness properties. \par However, these
                 techniques have not realized the same success on
                 software systems. One limitation is their inability to
                 deal with infinite-state programs -- even those with a
                 single unbounded integer. A second problem is that of
                 finding efficient representations for various variable
                 types. We recently proposed a model checker for
                 integer-based systems that uses arithmetic constraints
                 as the underlying state representation. While this
                 approach easily verified some subtle, infinite-state
                 concurrency problems, it proved inefficient in its
                 treatment of boolean and (unordered) enumerated types
                 -- which are not efficiently representable using
                 arithmetic constraints. \par In this paper we present a
                 new technique that combines the strengths of both BDD
                 and arithmetic constraint representations. Our
                 composite model merges multiple type-specific symbolic
                 representations in a single model checker. A system's
                 transitions and fixpoint computations are encoded using
                 both BDD (for boolean and enumerated types), and
                 arithmetic constraint (for integers) representations,
                 where the choice depends on the variable types. Our
                 composite model checking strategy can be extended to
                 other symbolic representations provided that they
                 support operations such as intersection, union,
                 complement, equivalence checking and relational image
                 computations. We also present conservative
                 approximation techniques for composite representations
                 to address the undecidability of model checking on
                 infinite-state systems. \par We demonstrate the
                 effectiveness of our approach by analyzing two example
                 systems which include a mixture of booleans, integers
                 and enumerated types. One of them is a requirements
                 specification for the control software of a nuclear
                 reactor's cooling system, and the other one is a
                 transport protocol specification.}
}

@INPROCEEDINGS{CBMC-CK03,
  AUTHOR = { Clarke, Edmund
                and Kroening, Daniel },
  TITLE = { Hardware Verification using {ANSI-C} Programs as a Reference },
  BOOKTITLE = { Proceedings of ASP-DAC 2003 },
  YEAR = { 2003 },
  PUBLISHER = { IEEE Computer Society Press },
  PAGES = { 308--311 },
  ISBN = { 0-7803-7659-5 },
  MONTH = { January }
}

@INPROCEEDINGS{ckl2004,
  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 },
  PUBLISHER = { Springer },
  PAGES = { 168--176 },
  ISBN = { 3-540-21299-X },
  SERIES = { Lecture Notes in Computer Science },
  VOLUME = { 2988 },
  EDITOR = { Kurt Jensen and Andreas Podelski }
}

@ARTICLE{oai:CiteSeerPSU:418439,
  TITLE = {Java PathFinder: {A} Translator from Java to Promela},
  AUTHOR = {Klaus Havelund},
  YEAR = {1999},
  MONTH = SEP # {~30},
  ABSTRACT = {nterrupts, and perhaps most importantly: thread
                 operations. Among major concepts not translated are:
                 packages, method overloading and overriding, method
                 recursion, strings, and floating point numbers.
                 Finally, the class library is not translated.
                 References},
  CITESEER-ISREFERNCEDBY = {oai:CiteSeerPSU:407702;
                 oai:CiteSeerPSU:325803; oai:CiteSeerPSU:58450;
                 oai:CiteSeerPSU:407948},
  CITESEER-REFERENCES = {oai:CiteSeerPSU:173884; oai:CiteSeerPSU:353275;
                 oai:CiteSeerPSU:206733},
  ANNOTE = {The Pennsylvania State University CiteSeer Archives},
  FORMAT = {pdf},
  LANGUAGE = {en},
  OAI = {oai:CiteSeerPSU:418439},
  RIGHTS = {unrestricted},
  SUBJECT = {Klaus Havelund Java PathFinder A Translator from Java
                 to Promela},
  URL = {http://citeseer.ist.psu.edu/418439.html;
                 http://netlib.bell-labs.com/netlib/spin/ws99b/ug090076.pdf}
}

@ARTICLE{Havelund:2004:MJP,
  AUTHOR = {K. Havelund and G. Rosu},
  TITLE = {Monitoring {Java} Programs with {Java PathExplorer}},
  JOURNAL = {Electronic Notes in Theoretical Computer Science},
  VOLUME = {55},
  NUMBER = {2},
  PAGES = {1--18},
  MONTH = JAN,
  YEAR = {2004},
  CODEN = {????},
  ISSN = {1571-0661},
  BIBDATE = {Mon Feb 9 12:01:30 MST 2004},
  ACKNOWLEDGEMENT = ACK-NHFB,
  PAGECOUNT = {18}
}

@ARTICLE{oai:CiteSeerPSU:353275,
  TITLE = {Model Checking Java Programs Using Java PathFinder},
  AUTHOR = {Klaus Havelund and Thomas Pressburger},
  YEAR = {1999},
  MONTH = SEP # {~12},
  ABSTRACT = {. This paper describes a translator called Java
                 PathFinder (Jpf), from Java to Promela, the modeling
                 language of the Spin model checker. Jpf translates a
                 given Java program into a Promela model, which then can
                 be model checked using Spin. The Java program may
                 contain assertions, which are translated to similar
                 assertions in the Promela model. The Spin model checker
                 will then look for deadlocks and violations of any
                 stated assertions. Jpf generates a Promela model with
                 the same state space characteristics as the Java
                 program. Hence, the Java program must have a finite and
                 tractable state space. This work should be seen in a
                 broader attempt to make formal methods applicable
                 within NASA's areas such as space, aviation, and
                 robotics. The work is a continuation of an effort to
                 formally analyze, using Spin, a multi--threaded
                 operating system for the Deep-Space 1 space craft, and
                 of previous work in applying existing model checkers
                 and theorem provers to real applications. Key words:
                 Program...},
  CITESEER-ISREFERNCEDBY = {oai:CiteSeerPSU:45292},
  CITESEER-REFERENCES = {oai:CiteSeerPSU:118642; oai:CiteSeerPSU:110596;
                 oai:CiteSeerPSU:219179; oai:CiteSeerPSU:69237;
                 oai:CiteSeerPSU:288218; oai:CiteSeerPSU:173884;
                 oai:CiteSeerPSU:248384; oai:CiteSeerPSU:22306;
                 oai:CiteSeerPSU:36763},
  ANNOTE = {The Pennsylvania State University CiteSeer Archives},
  LANGUAGE = {en},
  OAI = {oai:CiteSeerPSU:353275},
  RIGHTS = {unrestricted},
  SUBJECT = {Klaus Havelund,Thomas Pressburger Model Checking Java
                 Programs Using Java PathFinder},
  URL = {http://citeseer.ist.psu.edu/353275.html;
                 http://ase.arc.nasa.gov/havelund/Publications/jpf-sttt.ps.Z}
}

@ARTICLE{oai:CiteSeerPSU:325921,
  TITLE = {Java PathFinder - Second Generation of a Java Model
                 Checker},
  AUTHOR = {Klaus Havelund and Seungjoon Park and Willem Visser},
  YEAR = {2000},
  MONTH = MAY # {~27},
  ABSTRACT = {We have been developing an automated abstraction
                 tool, which converts a Java program to an abstract
                 program with respect to user-specified abstraction
                 criteria. The user can specify abstractions by removing
                 variables in the concrete program and/or adding new
                 variables (currently the tool supports adding boolean
                 types only) to the abstract program. Specifically, the
                 user selects variables that must be removed and adds
                 abstract variables that represent the predicates in
                 which these variables occurred (typically the
                 predicates are selected from conditions in if and while
                 statements). Given a Java program and such abstraction
                 criteria, the tool generates an abstract Java program
                 in terms of the new abstract variables and unremoved
                 concrete variables. To compute the conversion
                 automatically, JPF uses a decision procedure, SVC
                 (Stanford Validity Checker), which checks the validity
                 of logical expressions [1]. The abstraction tool is
                 designed for object-oriented programs. The user can
                 sp...},
  CITESEER-ISREFERNCEDBY = {oai:CiteSeerPSU:364138;
                 oai:CiteSeerPSU:328832; oai:CiteSeerPSU:40043},
  CITESEER-REFERENCES = {oai:CiteSeerPSU:18496; oai:CiteSeerPSU:206810;
                 oai:CiteSeerPSU:367316; oai:CiteSeerPSU:247584;
                 oai:CiteSeerPSU:294162; oai:CiteSeerPSU:315574;
                 oai:CiteSeerPSU:173884; oai:CiteSeerPSU:12444;
                 oai:CiteSeerPSU:147558; oai:CiteSeerPSU:150909;
                 oai:CiteSeerPSU:260722; oai:CiteSeerPSU:156182;
                 oai:CiteSeerPSU:39396; oai:CiteSeerPSU:417953},
  ANNOTE = {The Pennsylvania State University CiteSeer Archives},
  LANGUAGE = {en},
  OAI = {oai:CiteSeerPSU:325921},
  RIGHTS = {unrestricted},
  SUBJECT = {And Klaus Havelund,And Seungjoon Park,And Willem
                 Visser Java PathFinder - Second Generation of a Java
                 Model Checker},
  URL = {http://citeseer.ist.psu.edu/325921.html;
                 http://www.riacs.edu/research/detail/ase/wave00.ps.gz}
}

@ARTICLE{oai:CiteSeerPSU:407997,
  TITLE = {Using Runtime Analysis to Guide Model Checking of Java
                 Programs},
  AUTHOR = {Klaus Havelund},
  YEAR = {2001},
  MONTH = JAN # {~27},
  ABSTRACT = {This paper describes how two runtime analysis
                 algorithms, an existing data race detection algorithm
                 and a new deadlock detection algorithm, have been
                 implemented to analyze Java programs. Runtime analysis
                 is based on the idea of executing the program once, and
                 observing the generated run to extract various kinds of
                 information. This information can then be used to
                 predict whether other different runs may violate some
                 properties of interest, in addition of course to
                 demonstrate whether the generated run itself violates
                 such properties. These runtime analyzes can be
                 performed stand-alone to generate a set of warnings. It
                 is furthermore demonstrated how these warnings can be
                 used to guide a model checker, thereby reducing the
                 search space. The described techniques have been
                 implemented in the home grown Java model checker called
                 Java PathFinder.},
  CITESEER-ISREFERNCEDBY = {oai:CiteSeerPSU:56283;
                 oai:CiteSeerPSU:254193; oai:CiteSeerPSU:285677;
                 oai:CiteSeerPSU:546588; oai:CiteSeerPSU:372750},
  CITESEER-REFERENCES = {oai:CiteSeerPSU:328188; oai:CiteSeerPSU:206810;
                 oai:CiteSeerPSU:118642; oai:CiteSeerPSU:247584;
                 oai:CiteSeerPSU:105655; oai:CiteSeerPSU:313021;
                 oai:CiteSeerPSU:210287; oai:CiteSeerPSU:315574;
                 oai:CiteSeerPSU:173884; oai:CiteSeerPSU:248384;
                 oai:CiteSeerPSU:348764; oai:CiteSeerPSU:326524;
                 oai:CiteSeerPSU:260722; oai:CiteSeerPSU:325921;
                 oai:CiteSeerPSU:323502; oai:CiteSeerPSU:417953},
  ANNOTE = {The Pennsylvania State University CiteSeer Archives},
  FORMAT = {pdf},
  LANGUAGE = {en},
  OAI = {oai:CiteSeerPSU:407997},
  RIGHTS = {unrestricted},
  SUBJECT = {Klaus Havelund Using Runtime Analysis to Guide Model
                 Checking of Java Programs},
  URL = {http://citeseer.ist.psu.edu/407997.html;
                 http://ic.arc.nasa.gov/ic/publications/pdf/2000-0177.pdf}
}

@ARTICLE{Havelund:2004:ORV,
  AUTHOR = {K. Havelund and G. Rosu},
  TITLE = {An Overview of the Runtime Verification Tool {Java
                 PathExplorer}: Special Issue on Selected Papers from
                 the {First International Workshop on Runtime
                 Verification Held in Paris, July 2001 (RV01)}},
  JOURNAL = {Formal Methods in System Design},
  VOLUME = {24},
  NUMBER = {2},
  PAGES = {189--215},
  MONTH = MAR,
  YEAR = {2004},
  CODEN = {FMSDE6},
  ISSN = {0925-9856},
  BIBDATE = {Mon Apr 5 09:19:58 MDT 2004},
  ACKNOWLEDGEMENT = ACK-NHFB,
  PAGECOUNT = {27}
}

@INPROCEEDINGS{esterel-methodology,
  AUTHOR = {Lionel Blanc and Amar Bouali and J\'er\^ome Dormoy and Olivier Meunier},
  TITLE = {A Methodology for {SoC} Top-Level Validation using Esterel Studio},
  BOOKTITLE = {Electronic Design Processes},
  YEAR = 2002,
  MONTH = {April}
}

@ARTICLE{Milner:1983:CSA,
  AUTHOR = {R. Milner},
  TITLE = {Calculi for synchrony and asynchrony},
  JOURNAL = {Theoretical Computer Science},
  VOLUME = {25},
  NUMBER = {3},
  PAGES = {267--310},
  MONTH = JUL,
  YEAR = {1983},
  CODEN = {TCSCDI},
  ISSN = {0304-3975},
  BIBDATE = {Sat Nov 22 13:36:07 MST 1997},
  ACKNOWLEDGEMENT = ACK-NHFB,
  CLASSIFICATION = {C4230B (Combinatorial switching theory)},
  CORPSOURCE = {Dept. of Computer Sci., Edinburgh Univ., Edinburgh,
                  UK},
  KEYWORDS = {Abelian group; algebraic theory; asynchrony;
                  bisimulation; calculus; combinatorial switching;
                  combinators; distributed computation; modelling;
                  synchrony},
  PUBCOUNTRY = {Netherlands},
  TREATMENT = {T Theoretical or Mathematical}
}

@INPROCEEDINGS{shiva-test,
  AUTHOR = {Fabrice Baray and Philippe Codognet and Daniel Diaz and Henri Michel},
  TITLE = {Code-based Test Generation for Validation of Functional Processor Descriptions},
  BOOKTITLE = {TACAS},
  YEAR = 2003,
  MONTH = {April}
}

@INPROCEEDINGS{aadebug2003,
  AUTHOR = {E. Jahier and B. Jeannet and F. Gaucher and F. Maraninchi},
  TITLE = {Automatic State Reaching for Debugging Reactive Programs},
  BOOKTITLE = {AADEBUG},
  MONTH = SEP,
  YEAR = 2003,
  ADDRESS = {Ghent}
}

@INPROCEEDINGS{counter-example,
  TITLE = {Counter-Example Generation in Symbolic Abstract Model-Checking},
  AUTHOR = {G. Pace and N. Halbwachs and P. Raymond},
  BOOKTITLE = {FMICS'2001},
  PUBLISHER = {Inria},
  ADDRESS = {Paris},
  MONTH = JUL,
  YEAR = 2001
}

@INPROCEEDINGS{cousot77,
  AUTHOR = {P. Cousot and R. Cousot},
  TITLE = {Abstract Interpretation: a Unified Lattice Model for Static
Analysis of Programs by Construction or Approximation of Fixpoints},
  BOOKTITLE = {POPL'77},
  ADDRESS = {Los Angeles},
  MONTH = JAN,
  YEAR = 1977
}

@INPROCEEDINGS{verif-specc,
  AUTHOR = {T. Sakunkonchak and M. Fujita},
  TITLE = {Verification of Synchronization in {SpecC} Description with the Use of Difference Decision Diagrams},
  BOOKTITLE = {FDL},
  YEAR = 2002
}

@INPROCEEDINGS{static-tlm,
  AUTHOR = {Giovanni Agosta and Francesco Bruschi and Donatella Sciuto},
  TITLE = {Static Analysis of Transaction-Level Models},
  BOOKTITLE = {DAC},
  YEAR = 2003,
  MONTH = {June}
}

@TECHREPORT{MSR-TR-2000-14,
  AUTHOR = {Thomas Ball and Sriram K. Rajamani},
  TITLE = {Boolean Programs: A Model and Process for Software Analysis},
  INSTITUTION = {Microsoft Research},
  YEAR = 2000,
  MONTH = {February}
}

@PHDTHESIS{IB-B961054,
  AUTHOR = {K. L. McMillan},
  TITLE = {Symbolic Model Checking},
  ADDRESS = {Boston},
  YEAR = {1993},
  ISBN = {0-7923-9380-5},
  DESCRIPTOR = {Model-Checking, Verifikationssystem, Verifikation}
}

@MANUAL{smv-man,
  TITLE = {Getting started with {SMV}},
  AUTHOR = {Kenneth L. McMillan},
  ORGANIZATION = {Cadence Berkeley Labs},
  ADDRESS = {Berkeley, CA 94704 {USA}},
  YEAR = {2001}
}

@MISC{oai:CiteSeerPSU:499529,
  TITLE = {The {SMV} system},
  AUTHOR = {K. L. McMillan},
  YEAR = {1992},
  MONTH = NOV # {~06},
  ABSTRACT = {This document describes the syntax and semantics of
                 the SMV input language, and the function of the SMV
                 model checker. It also describes some optional features
                 of the model checker which can be used to fine tune the
                 performance, and gives some examples of its
                 application. All of the examples in this document are
                 made available with the software. For a description of
                 all the model checker options, see the UNIX
                 programmer's manual entry for SMV, which is also
                 included with the software},
  LANGUAGE = {en},
  OAI = {oai:CiteSeerPSU:499529},
  RIGHTS = {unrestricted},
  SUBJECT = {K. L. Mcmillan The SMV system},
  URL = {http://citeseer.ist.psu.edu/499529.html;
                 http://www.cs.cmu.edu/~modelcheck/smv/smvmanual.ps.gz}
}

@TECHREPORT{smv-language,
  AUTHOR = {K. L. McMillan},
  TITLE = {The {SMV} Language},
  INSTITUTION = {Cadence Berkeley Labs},
  YEAR = 1999,
  MONTH = {March}
}

@ARTICLE{Argos-CL,
  AUTHOR = {F. Maraninchi and Y. R\'emond},
  TITLE = {Argos: an Automaton-Based Synchronous Language},
  JOURNAL = {Computer Languages},
  PUBLISHER = {Elsevier},
  NUMBER = {27},
  PAGES = {61-92},
  YEAR = {2001}
}

@ARTICLE{pourmilner:Esterel,
  AUTHOR = {G. Berry},
  TITLE = {The Foundations of {Esterel}},
  JOURNAL = {Proof, Language and Interaction: Essays in Honour of
                 Robin Milner},
  PUBLISHER = {MIT Press},
  YEAR = {2000},
  NOTE = {Editors: G. Plotkin, C. Stirling and M. Tofte}
}

@ARTICLE{lamport77,
  AUTHOR = {L. Lamport},
  TITLE = {Proving the correctness of multiprocess programs},
  JOURNAL = {IEEE Transactions on Software Engineering},
  VOLUME = {SE-3},
  NUMBER = 2,
  PAGES = {125--143},
  YEAR = 1977
}

@MISC{prover-plugin,
  AUTHOR = {{PROVER} Technology},
  TITLE = {Prover Plug-in\texttrademark\ for SCADE\texttrademark},
  NOTE = {{\texttt{http://www.prover.com/products/ppi/sl.xml}}}
}

@MANUAL{gcc-int-man,
  TITLE = {GNU Compiler Collection Internals},
  AUTHOR = {Richard M. Stallman and {the GCC developer community}},
  ORGANIZATION = {Free Software Fundation},
  NOTE = {{\texttt{http://gcc.gnu.org/onlinedocs/gccint/}}}
}

@MISC{philippe-bhdl,
  AUTHOR = {Ammar Aljer Philippe},
  TITLE = {{BHDL}: Circuit design in B},
  URL = {http://citeseer.ist.psu.edu/650917.html},
  YEAR = 2003
}

@BOOK{b-book,
  AUTHOR = {JR Abrial and A Nikolaos},
  TITLE = {The B-book: assigning programs to meanings},
  PUBLISHER = {Cambridge University Press    New York, NY, USA},
  YEAR = 1996,
  NOTE = {ISBN:0-521-49619-5}
}

@MISC{oai:CiteSeerPSU:19422,
  TITLE = {Symbolic Model Checking: $10^{20}$ States and Beyond},
  AUTHOR = {D. L. Dill and E. M. Clarke and J. R. Burch and K. L.
                 Mcmillan and L. J. Hwang},
  YEAR = {1990},
  MONTH = {march},
  ABSTRACT = {Many different methods have been devised for
                 automatically verifying finite state systems by
                 examining state-graph models of system behavior. These
                 methods all depend on decision procedures that
                 explicitly represent the state space using a list or a
                 table that grows in proportion to the number of states.
                 We describe a general method that represents the state
                 space symbolically instead of explicitly. The
                 generality of our method comes from using a dialect of
                 the Mu-Calculus as the primary specification language.
                 We describe a model checking algorithm for Mu-Calculus
                 formulas that uses Bryant's Binary Decision Diagrams
                 (1986) to represent relations and formulas. We then
                 show how our new Mu-Calculus model checking algorithm
                 can be used to derive efficient decision procedures for
                 CTL model checking, satisfiability of linear-time
                 temporal logic formulas, strong and weak observational
                 equivalence of finite transition systems, and language
                 containment for finite !-automata. The fixed point
                 co...},
  CITESEER-REFERENCES = {oai:CiteSeerPSU:311874; oai:CiteSeerPSU:225173;
                 oai:CiteSeerPSU:206738},
  ANNOTE = {The Pennsylvania State University CiteSeer Archives},
  LANGUAGE = {en},
  OAI = {oai:CiteSeerPSU:19422},
  RIGHTS = {unrestricted},
  SUBJECT = {D. L. Dill,E. M. Clarke,J. R. Burch,K. L. Mcmillan,L.
                 J. Hwang Symbolic Model Checking: 10 20 States and
                 Beyond},
  URL = {http://citeseer.ist.psu.edu/19422.html;
                 http://maui.theoinf.tu-ilmenau.de/forschung/links/../doc/SMC.ps.gz}
}

@MISC{oai:CiteSeerPSU:156791,
  TITLE = {Data-Structures for the Verification of Timed
                 Automata},
  AUTHOR = {Alain Kerbrat and Amir Pnueli and Anne Rasse and
                 Eugene Asarin and Marius Bozga and Oded Maler},
  YEAR = {1997},
  MONTH = APR # {~30},
  ABSTRACT = {. In this paper we suggest numerical decision
                 diagrams, a bdd- based data-structure for representing
                 certain subsets of the Euclidean space, namely those
                 encountered in verification of timed automata. Unlike
                 other representation schemes, ndd's are canonical and
                 provide for all the necessary operations needed in the
                 verification and synthesis of timed automata. We report
                 some preliminary experimental results. 1 Introduction
                 Consider a transition system A = (Q; ffi), where Q is
                 the set of states and ffi : Q 7! 2 Q is a transition
                 function, mapping each state q 2 Q into the set of
                 q-successors ffi(q) ` Q. The problem of calculating or
                 characterizing all the states reachable from a subset F
                 ` Q of the state-space is one of the central problems
                 in verification. The basic algorithm to calculate this
                 set of states is the following: F 0 := F for i = 0; 1;
                 : : : ; repeat F i+1 := F i [ ffi(F i ) until F i+1 = F
                 i where ffi(F i ) = S q2F i ffi(q). Symbolic methods
                 [BCM + 93], [M...},
  CITESEER-REFERENCES = {oai:CiteSeerPSU:131548; oai:CiteSeerPSU:28329;
                 oai:CiteSeerPSU:311874; oai:CiteSeerPSU:19422;
                 oai:CiteSeerPSU:224357; oai:CiteSeerPSU:496938;
                 oai:CiteSeerPSU:182869; oai:CiteSeerPSU:422908;
                 oai:CiteSeerPSU:66285; oai:CiteSeerPSU:144751},
  ANNOTE = {Author: Amir Pnueli (Affiliation: Department of
                 Computer Science, Weizmann Inst. Rehovot 76100, Israel;
                 ); Author: Anne Rasse (Affiliation: Institute for
                 Information Transmission Problems; Address: 19 Bol.
                 Karetnyi per ., 101447, Moscow, Russia; ); Author:
                 Eugene Asarin (Affiliation: Institute for Information
                 Transmission Problems; Address: 19 Bol. Karetnyi per .,
                 101447, Moscow, Russia; ); Author: Oded Maler (Address:
                 Verimag, Centre Equation, 2, av. de Vignate, 38610
                 Gi`eres, France; );},
  LANGUAGE = {en},
  OAI = {oai:CiteSeerPSU:156791},
  RIGHTS = {unrestricted},
  SUBJECT = {Alain Kerbrat,Amir Pnueli,Anne Rasse,Eugene
                 Asarin,Marius Bozga,Oded Maler Data-Structures for the
                 Verification of Timed Automata},
  URL = {http://citeseer.ist.psu.edu/156791.html}
}

@TECHREPORT{polyspace,
  AUTHOR = {Dr. Alain Deutsch},
  TITLE = {Static verification of dynamic properties},
  INSTITUTION = {PolySpace Technologies},
  YEAR = 2003,
  MONTH = {November}
}

@BOOK{design-patterns,
  AUTHOR = {Erich Gamma and Richard Helm and Ralph Johnson and John Vlissides},
  TITLE = {Design Patterns: Elements of Reusable Object-Oriented Software},
  PUBLISHER = {Addison-Wesley},
  YEAR = 1994
}

@INPROCEEDINGS{694478,
  AUTHOR = {Moshe Y. Vardi},
  TITLE = {Branching vs. Linear Time: Final Showdown},
  BOOKTITLE = {TACAS 2001: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
  YEAR = {2001},
  ISBN = {3-540-41865-2},
  PAGES = {1--22},
  PUBLISHER = {Springer-Verlag},
  ADDRESS = {London, UK}
}

@TECHREPORT{903577,
  AUTHOR = {A. Pnueli},
  TITLE = {The Temporal Logic of Programs},
  YEAR = {1997},
  SOURCE = {http://www.ncstrl.org:8900/ncstrl/servlet/search?formname=detail\&id=oai%3Ancstrlh%3Aweizmann_il%3Ancstrl.weizmann_il%2F%2FCS97-14},
  PUBLISHER = {Weizmann Science Press of Israel},
  ADDRESS = {Jerusalem, Israel, Israel}
}

@INPROCEEDINGS{graphviz,
  AUTHOR = {John Ellson and Emden Gansner and Lefteris Koutsofios and Stephen C. North and Gordon Woodhull},
  TITLE = {Graphviz - Open Source Graph Drawing Tools},
  BOOKTITLE = {Lecture Notes in Computer Science},
  PAGES = 483,
  YEAR = 2003,
  VOLUME = {Volume 2265 / 2002},
  MONTH = {July},
  PUBLISHER = {Springer-Verlag GmbH},
  ANNOTE = {Graph Drawing : 9th International Symposium}
}

@INPROCEEDINGS{amast93,
  AUTHOR = {N. Halbwachs and F. Lagnier and P. Raymond},
  TITLE = {Synchronous observers and the verification of reactive systems},
  BOOKTITLE = {Third Int. Conf. on Algebraic Methodology and
              Software Technology, AMAST'93},
  ADDRESS = {Twente},
  MONTH = {June },
  EDITOR = {M. Nivat and C. Rattray and T. Rus and G. Scollo},
  PUBLISHER = {Workshops in Computing, Springer Verlag},
  YEAR = 1993
}

@INPROCEEDINGS{halbwachs-emsoft02,
  AUTHOR = {N. Halbwachs and S. Baghdadi},
  TITLE = {Synchronous modeling of asynchronous systems},
  BOOKTITLE = {EMSOFT'02},
  PUBLISHER = {LNCS 2491, Springer Verlag},
  ADDRESS = {Grenoble},
  MONTH = OCT,
  YEAR = 2002
}

@INPROCEEDINGS{BozgaGrafOberSifakis-SFM-04,
  AUTHOR = {Marius Bozga and Susanne Graf and Iulian Ober and Ileana Ober and Joseph Sifakis},
  TITLE = {The IF toolset},
  BOOKTITLE = {4th International School on Formal Methods for the Design of Computer, 
                  Communication and Software Systems: Real Time, SFM-04:RT, Bologna, Sept. 2004},
  SERIES = {LNCS Tutorials, Springer},
  YEAR = 2004
}

@INPROCEEDINGS{88165,
  AUTHOR = {O. Coudert and C. Berthet and J. C. Madre},
  TITLE = {Verification of synchronous sequential machines based on symbolic execution},
  BOOKTITLE = {Proceedings of the international workshop on Automatic verification methods for finite state systems},
  YEAR = {1990},
  ISBN = {0-387-52148-8},
  PAGES = {365--373},
  LOCATION = {Grenoble, France},
  PUBLISHER = {Springer-Verlag New York, Inc.},
  ADDRESS = {New York, NY, USA}
}

@ARTICLE{bryant92symbolic,
  AUTHOR = {Randal E. Bryant},
  TITLE = {Symbolic {Boolean} Manipulation with Ordered Binary-Decision Diagrams},
  JOURNAL = {ACM Computing Surveys},
  VOLUME = {24},
  NUMBER = {3},
  PAGES = {293--318},
  YEAR = {1992},
  URL = {citeseer.ist.psu.edu/bryant92symbolic.html}
}

@BOOK{tlm-book,
  EDITOR = {Ghenassia, Frank (Ed.)},
  TITLE = {Transaction-Level Modeling with {SystemC}. TLM Concepts and Applications for Embedded Systems},
  PUBLISHER = {Springer},
  YEAR = 2005,
  MONTH = {June},
  NOTE = {ISBN 0-387-26232-6}
}

@TECHREPORT{tlm-standard-doc,
  AUTHOR = {Adam Rose and Stuart Swan and John Pierce and Jean-Michel Fernandez and Cadence Design Systems},
  TITLE = {Transaction Level Modeling in SystemC},
  INSTITUTION = {Mentor Graphics; Cadence Design Systems},
  YEAR = 2005
}

@TECHREPORT{pasricha02:_trans_level_model_of_soc,
  AUTHOR = {Sudeep Pasricha},
  TITLE = {Transaction Level Modeling of {SoC} in SystemC 2.0},
  INSTITUTION = {STMicroelectronics Ltd},
  YEAR = 2002
}

@INPROCEEDINGS{944651,
  AUTHOR = {Lukai Cai and Daniel Gajski},
  TITLE = {Transaction level modeling: an overview},
  BOOKTITLE = {CODES+ISSS '03: Proceedings of the 1st IEEE/ACM/IFIP international conference on Hardware/software codesign and system synthesis},
  YEAR = {2003},
  ISBN = {1-58113-742-7},
  PAGES = {19--24},
  LOCATION = {Newport Beach, CA, USA},
  DOI = {http://doi.acm.org/10.1145/944645.944651},
  PUBLISHER = {ACM Press},
  ADDRESS = {New York, NY, USA}
}

@INPROCEEDINGS{pinapa,
  AUTHOR = {Matthieu Moy and Florence Maraninchi and Laurent Maillet-Contoz},
  TITLE = {{Pinapa}: An Extraction Tool for SystemC descriptions of Systems-on-a-Chip},
  BOOKTITLE = {EMSOFT},
  YEAR = 2005,
  MONTH = {September}
}

@INPROCEEDINGS{lussy,
  AUTHOR = {Matthieu Moy and Florence Maraninchi and Laurent Maillet-Contoz},
  TITLE = {{LusSy}: A Toolbox for the Analysis of Systems-on-a-Chip at the Transactional Level},
  BOOKTITLE = {International Conference on Application of Concurrency to System Design},
  YEAR = 2005,
  MONTH = {June}
}

@MISC{oai:CiteSeerPSU:368718,
  TITLE = {Symbolic Model Checking using {SAT} procedures instead
                 of {BDD}s},
  AUTHOR = {A. Biere and A. Cimatti and E. M. Clarke and M. Fujita
                 and Y. Zhu},
  YEAR = {1999},
  MONTH = SEP # {~10},
  ABSTRACT = {In this paper, we study the application of
                 propositional decision procedures in hardware
                 verification. In particular, we apply bounded model
                 checking, as introduced in [1], to equivalence and
                 invariant checking. We present several optimizations
                 that reduce the size of generated propositional
                 formulas. In many instances, our SAT-based approach can
                 significantly outperform BDD-based approaches. We
                 observe that SAT-based techniques are particularly
                 efficient in detecting errors in both combinational and
                 sequential designs. 1 Introduction A complex hardware
                 design can be error-prone and mistakes are costly.
                 Formal verification techniques such as symbolic model
                 checking are gaining wide industrial acceptance.
                 Compared to traditional validation techniques based on
                 simulation, they provide more extensive coverage and
                 can detect subtle errors. Representing and manipulating
                 boolean expressions is critical to many formal
                 verification techniques. BDDs [3] have traditionally
                 been used for this p...},
  CITESEER-REFERENCES = {oai:CiteSeerPSU:155235; oai:CiteSeerPSU:311874;
                 oai:CiteSeerPSU:19422; oai:CiteSeerPSU:42422;
                 oai:CiteSeerPSU:169223},
  ANNOTE = {Author: A. Biere (Affiliation: Istituto per la Ricerca
                 Scientifica e Tecnolgica (IRST); Address: via Sommarive
                 18, 38055 Povo (TN), Italy, Fujitsu Laboratories of
                 America, Inc. 595 Lawrence Expressway, Sunnyvale, CA
                 94086-3922, U.S.A; ); Author: A. Cimatti (Affiliation:
                 Istituto per la Ricerca Scientifica e Tecnolgica
                 (IRST); Address: via Sommarive 18, 38055 Povo (TN),
                 Italy, Fujitsu Laboratories of America, Inc. 595
                 Lawrence Expressway, Sunnyvale, CA 94086-3922, U.S.A;
                 ); Author: E. M. Clarke (Affiliation: Istituto per la
                 Ricerca Scientifica e Tecnolgica (IRST); Address: via
                 Sommarive 18, 38055 Povo (TN), Italy, Fujitsu
                 Laboratories of America, Inc. 595 Lawrence Expressway,
                 Sunnyvale, CA 94086-3922, U.S.A; ); Author: M. Fujita
                 (Affiliation: Istituto per la Ricerca Scientifica e
                 Tecnolgica (IRST); Address: via Sommarive 18, 38055
                 Povo (TN), Italy, Fujitsu Laboratories of America, Inc.
                 595 Lawrence Expressway, Sunnyvale, CA 94086-3922,
                 U.S.A; ); Author: Y. Zhu (Affiliation: Istituto per la
                 Ricerca Scientifica e Tecnolgica (IRST); Address: via
                 Sommarive 18, 38055 Povo (TN), Italy, Fujitsu
                 Laboratories of America, Inc. 595 Lawrence Expressway,
                 Sunnyvale, CA 94086-3922, U.S.A; );},
  LANGUAGE = {en},
  OAI = {oai:CiteSeerPSU:368718},
  RIGHTS = {unrestricted},
  SUBJECT = {A. Biere,A. Cimatti,E. M. Clarke,M. Fujita,Y. Zhu
                 Symbolic Model Checking using SAT procedures instead of
                 BDDs},
  URL = {http://citeseer.ist.psu.edu/368718.html;
                 http://iseran.ira.uka.de/~armin/publications/BiereCimattiClarkeFujitaZhu-DAC99.ps.gz}
}

@MASTERSTHESIS{muzammil-smv,
  AUTHOR = {Muhammad Muzammil Shahbaz},
  TITLE = {Automatic Verification Techniques for System-on-chip using Symbolic Model Verifier},
  SCHOOL = {Universit\'e Joseph Fourier},
  YEAR = 2005,
  ADDRESS = {Grenoble, France},
  MONTH = {June},
  NOTE = {Work performed in Verimag}
}

@INPROCEEDINGS{maraninchi00stepwise,
  AUTHOR = {Florence Maraninchi and Fabien Gaucher},
  TITLE = {Step-wise + Algorithmic debugging for Reactive Programs: Ludic, a debugger for Lustre},
  BOOKTITLE = {Automated and Algorithmic Debugging},
  YEAR = {2000},
  URL = {citeseer.ist.psu.edu/maraninchi00stepwise.html}
}

@INPROCEEDINGS{state-encoding,
  AUTHOR = {Dunoyer Julien, P\'etrot Fr\'ed\'eric, Jacomme Ludovic},
  TITLE = {Intrinsic Limitations of Logarithmic Encodings for Low Power Finite State Machines},
  BOOKTITLE = {Mixed Design of {VLSI} Circuits Conference},
  PAGES = {613-618},
  YEAR = 1997,
  MONTH = {June}
}

@INPROCEEDINGS{1999:sas:bozga,
  AUTHOR = {Marius Bozga and Jean-Claude Fernandez and Lucian
                 Ghirvu},
  TITLE = {State Space Reduction Based on Live Variables
                 Analysis},
  EDITOR = {Agostino Cortesi and Gilberto Fil{\'e}},
  BOOKTITLE = {Static Analysis},
  YEAR = {1999},
  VOLUME = {1694},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer},
  PAGES = {164--178},
  ANNOTE = {incomplete}
}

@ARTICLE{Chaitin:1982:RAS,
  AUTHOR = {G. J. Chaitin},
  TITLE = {Register allocation and spilling via graph coloring},
  JOURNAL = {ACM SIG{\-}PLAN Notices},
  VOLUME = {17},
  NUMBER = {6},
  PAGES = {98--105},
  MONTH = JUN,
  YEAR = {1982},
  CODEN = {SINODQ},
  ISSN = {0362-1340},
  BIBDATE = {Sun Dec 14 09:14:38 MST 2003},
  ACKNOWLEDGEMENT = ACK-NHFB,
  CLASSIFICATION = {C1160 (Combinatorial mathematics); C6150C
                 (Compilers, interpreters and other processors)},
  CONFLOCATION = {Boston, MA, USA; 23-25 June 1982},
  CONFTITLE = {Proceedings of the SIGPLAN '82 Symposium on Compiler
                 Construction},
  CORPSOURCE = {IBM Res., Yorktown Heights, NY, USA},
  KEYWORDS = {global register allocation; graph coloring; graph
                 colouring; machine registers; PL/I; PL/I optimizing
                 compiler; program compilers; register conflict graph;
                 spill code},
  SPONSORORG = {ACM},
  TREATMENT = {P Practical}
}

@MISC{oai:CiteSeerPSU:378053,
  TITLE = {Register Allocation by Graph Coloring: {A} Review},
  AUTHOR = {Frank Mueller},
  YEAR = {1993},
  MONTH = APR # {~14},
  ABSTRACT = {Introduction The problem of register allocation for
                 code generation can be described as follows: Given a
                 set of (hardware) registers, what is the most efficient
                 mapping of registers to program variables in terms of
                 execution time of the program. But let us first define
                 some terms to describe the problem more formally. A
                 variable is defined at a point in a program when a
                 value is assigned to it. A variable is used at a point
                 in a program when its value is referenced in an
                 expression. A variable is said to be live at a point if
                 it has been defined earlier and will be used later. The
                 live range of a variable is the execution range (a set
                 of adjacent vertices of the control flow graph of the
                 program) between definitions and uses of a variable.
                 Two variables are simultaneously live if and only if
                 both are live for the a vertex v of the control flow
                 graph. A proper register allocation<},
  ANNOTE = {Author: Frank Mueller (Affiliation: Department of
                 Computer Science, B-173, Florida State University;
                 Address: Tallahassee, Florida 32306-4019; );},
  LANGUAGE = {en},
  OAI = {oai:CiteSeerPSU:378053},
  RIGHTS = {unrestricted},
  SUBJECT = {Frank Mueller Register Allocation by Graph Coloring: A
                 Review},
  URL = {http://citeseer.ist.psu.edu/378053.html;
                 ftp://ftp.inria.fr/INRIA/Projects/a3/lelait/Haiku/mueller.ps.gz}
}

@MISC{oai:CiteSeerPSU:386333,
  TITLE = {The Simulation Semantics of System{C}},
  AUTHOR = {Dirk Hoffmann and Joachim Gerlach and Juergen Ruf and
                 Thomas Kropf and Wolfgang Mueller and Wolfgang
                 Rosenstiehl},
  YEAR = {2001},
  MONTH = DEC # {~21},
  ABSTRACT = {We present a rigorous but transparent semantics
                 definition of SystemC that covers method, thread, and
                 clocked thread behavior as well as their interaction
                 with the simulation kernel process. The semantics
                 includes watching statements, signal assignment, and
                 wait statements as they are introduced in SystemC V1.0.
                 We present our definition in form of distributed
                 Abstract State Machines (ASMs) rules reflecting the
                 view given in the SystemC User's Manual and the
                 reference implementation. We mainly see our formal
                 semantics as a concise, unambiguous, high--level
                 specification for SystemC--based implementations and
                 for standardization. Additionally, it can be used as a
                 sound basis to investigate SystemC interoperability
                 with Verilog and VHDL. 1. Introduction SystemC is the
                 emerging de-facto-standard for systemlevel modeling and
                 design from the Open SystemC Initiative (OSCI) which is
                 controlled by a steering group and backed by a growing
                 community of currently over 50 charter member
                 companies...},
  CITESEER-REFERENCES = {oai:CiteSeerPSU:428949; oai:CiteSeerPSU:792},
  ANNOTE = {Author: Dirk Hoffmann (Affiliation: University of
                 Tuebingen; Address: Tuebingen, Germany; ); Author:
                 Joachim Gerlach (Affiliation: University of Tuebingen;
                 Address: Tuebingen, Germany; ); Author: Juergen Ruf
                 (Affiliation: University of Tuebingen; Address:
                 Tuebingen, Germany; ); Author: Thomas Kropf
                 (Affiliation: University of Tuebingen; Address:
                 Tuebingen, Germany; ); Author: Wolfgang Mueller
                 (Affiliation: C-LABPaderborn University; Address:
                 Paderborn, Germany; ); Author: Wolfgang Rosenstiehl
                 (Affiliation: University of Tuebingen; Address:
                 Tuebingen, Germany; );},
  LANGUAGE = {en},
  OAI = {oai:CiteSeerPSU:386333},
  RIGHTS = {unrestricted},
  SUBJECT = {Dirk Hoffmann,Joachim Gerlach,Juergen Ruf,Thomas
                 Kropf,Wolfgang Mueller,Wolfgang Rosenstiehl The
                 Simulation Semantics of SystemC},
  URL = {http://citeseer.ist.psu.edu/386333.html;
                 http://www.c-lab.de/~wolfgang/date01.ps.Z}
}

@INPROCEEDINGS{DBLP:conf/date/Salem03,
  AUTHOR = {Ashraf Salem},
  TITLE = {Formal Semantics of Synchronous SystemC.},
  BOOKTITLE = {DATE},
  YEAR = {2003},
  PAGES = {10376-10381},
  EE = {http://csdl.computer.org/comp/proceedings/date/2003/1870/01/187010376abs.htm},
  BIBSOURCE = {DBLP, http://dblp.uni-trier.de}
}

@MISC{c-for-system-level-design,
  AUTHOR = {Guido Arnout {(CoWare, Inc.)}},
  TITLE = {C for System Level Design},
  MONTH = {September},
  YEAR = 1999,
  NOTE = {{\small\texttt{https://www.systemc.org/projects/sitedocs/document/coWare/en/1}}}
}

@INPROCEEDINGS{fujita01standard,
  AUTHOR = {Masahiro Fujita and Hiroshi Nakamura},
  TITLE = {The standard SpecC language},
  BOOKTITLE = {{ISSS}},
  PAGES = {81-86},
  YEAR = {2001},
  URL = {http://citeseer.ist.psu.edu/fujita01standard.html}
}

@INPROCEEDINGS{oai:DBLP:inproceedings.conf/dac/GanapathyNJFWN96,
  TITLE = {Hardware Emulation for Functional Verification of
                 {K5}.},
  AUTHOR = {Gopi Ganapathy and Ram Narayan and Glenn Jorden and
                 Denzil Fernandez and Ming Wang and Jim Nishimura},
  YEAR = {1996},
  OAI = {oai:DBLP:inproceedings.conf/dac/GanapathyNJFWN96},
  CONFERENCE = {Design Automation Conference (DAC)},
  URL = {http://purl.org/CITIDEL/DBLP/db/conf/dac/dac96.html#GanapathyNJFWN96}
}

@INPROCEEDINGS{KS2005,
  AUTHOR = { Kroening, Daniel
                and Sharygina, Natasha },
  TITLE = { Formal Verification of SystemC by Automatic Hardware/Software Partitioning },
  BOOKTITLE = { Proceedings of MEMOCODE 2005 },
  YEAR = { 2005 },
  PUBLISHER = { IEEE },
  PAGES = { 101--110 }
}

@INPROCEEDINGS{graf97construction,
  AUTHOR = {{S. Graf} and {H. Saidi}},
  TITLE = {Construction of Abstract State Graphs with {PVS}},
  BOOKTITLE = {Proc. 9th {INternational} Conference on Computer Aided Verification ({CAV}'97)},
  VOLUME = {1254},
  PUBLISHER = {Springer Verlag},
  EDITOR = {O. Grumberg},
  PAGES = {72--83},
  YEAR = {1997},
  URL = {http://citeseer.ist.psu.edu/graf97construction.html}
}

@MASTERSTHESIS{palix04,
  AUTHOR = {Nicolas Palix},
  TITLE = {Modélisation et Vérification de Systèmes sur Puces à Base de Composants},
  SCHOOL = {ESISAR/INPG},
  YEAR = 2004,
  ADDRESS = {Grenoble, France}
}

@UNPUBLISHED{roux05,
  AUTHOR = {Yvan Roux},
  TITLE = {Rapport intermédiaire du projet Vercors},
  YEAR = 2005,
  MONTH = {June},
  NOTE = {Internal report in INRIA Rh\^one Alpes}
}

@MISC{oai:CiteSeerPSU:494428,
  TITLE = {Prometheus - {A} Compositional Modeling Tool for
                 Real-Time Systems},
  YEAR = {2001},
  MONTH = SEP # {~25},
  ABSTRACT = {Prometheus is a modeling tool allowing the user to
                 specify and compose real-time systems, by means of
                 synchronization and priorization of actions, with a
                 scheduler specified in a high-level description
                 language. The resulting model is checked for
                 consistency of the priorities, safety and liveness
                 properties which can - up to a certain degree - be
                 guaranteed by Prometheus. The composed system can be
                 output in several formats.},
  CITESEER-REFERENCES = {oai:CiteSeerPSU:475929; oai:CiteSeerPSU:305877;
                 oai:CiteSeerPSU:600014; oai:CiteSeerPSU:422234;
                 oai:CiteSeerPSU:2326; oai:CiteSeerPSU:328445},
  LANGUAGE = {en},
  OAI = {oai:CiteSeerPSU:494428},
  RIGHTS = {unrestricted},
  SUBJECT = {Prometheus - A Compositional Modeling Tool for
                 Real-Time Systems},
  URL = {http://citeseer.ist.psu.edu/494428.html;
                 http://www.inrialpes.fr/pop-art/share/Publications/goessler/prometheus.ps}
}

@BOOK{993954,
  AUTHOR = {Yves Bertot and Pierre Casteran},
  TITLE = {Interactive Theorem Proving and Program Development},
  YEAR = {2004},
  ISBN = {3540208542},
  PUBLISHER = {SpringerVerlag}
}

@BOOK{Nipkow-Paulson-Wenzel:2002,
  AUTHOR = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  TITLE = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  PUBLISHER = {Springer},
  SERIES = {LNCS},
  VOLUME = 2283,
  YEAR = 2002
}

@INPROCEEDINGS{cade92-pvs,
  AUTHOR = {{S.} Owre and {J.} {M.} Rushby and and {N.} Shankar},
  TITLE = {{PVS:} {A} Prototype Verification System},
  BOOKTITLE = {11th International Conference on Automated Deduction (CADE)},
  YEAR = {1992},
  EDITOR = {Deepak Kapur},
  SERIES = {Lecture Notes in Artificial Intelligence},
  VOLUME = {607},
  PAGES = {748--752},
  ADDRESS = {Saratoga, {NY}},
  MONTH = {jun},
  PUBLISHER = {Springer-Verlag},
  URL = {http://www.csl.sri.com/papers/cade92-pvs/}
}

@INPROCEEDINGS{ICCAD2000*120,
  AUTHOR = {{Pei-Hsin} Ho and Thomas Shiple and Kevin Harer and
		 James Kukula and Robert Damiano and Valeria Bertacco
		 and Jerry Taylor and Jiang Long},
  TITLE = {Smart Simulation Using Collaborative Formal and
		 Simulation Engines},
  PAGES = {120--126}
}

@MANUAL{formalcheck,
  TITLE = {Formal Verification Using Affirma {FormalCheck}},
  ORGANIZATION = {Cadence},
  MONTH = {October},
  YEAR = 1999
}

@INPROCEEDINGS{DAC96*655,
  AUTHOR = {Ilan Beer and Shoham Ben-David and Cindy Eisner and
		 Avner Landver},
  TITLE = {{RuleBase}: an Industry-Oriented Formal Verification
		 Tool},
  PAGES = {655--660},
  BOOKTITLE = {33rd Design Automation Conference ({DAC}'96)},
  ISBN = {0-89791-779-0},
  MONTH = JUN,
  PUBLISHER = {Association for Computing Machinery},
  ADDRESS = {New York},
  YEAR = {1996}
}


This file has been generated by bibtex2html 1.75