@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