Changeset 51

Timestamp:

Mar 7, 2012, 11:42:59 AM (13 years ago)

Author:

cecile

Message:

new articles for components based abstraction and compostion added

Location:

biblio

Files:

• biblio.bib (modified) (11 diffs)
• compositional.bib (modified) (2 diffs)
• compositional.html (modified) (7 diffs)

biblio/biblio.bib

@@ -448 +448 @@
   bibsource = {DBLP, http://dblp.uni-trier.de},
   crossref = {DBLP:conf/cav/2002},
-  ee = {http://link.springer.de/link/service/series/0558/bibs/2404/24040137.htm}
+  ee = {http://link.springer.de/link/service/series/0558/bibs/2404/24040137.htm},
+  keywords = {Abstraction}
 }
 
@@ -1330 +1331 @@
   year = {2007},
   note = {accepted},
+  keywords = {Abstraction, CEGAR, CTL},
   owner = {cecile},
   timestamp = {2007.03.27}
@@ -1481 +1483 @@
   pages = {1686-1691},
   file = {:Composition/Speeding up MC by exploiting Explicit09.PDF:PDF},
+  keywords = {Composition , model checking},
   owner = {cecile},
   timestamp = {2009.04.30}
@@ -1788 +1791 @@
 }
 
+@INPROCEEDINGS{6128043,
+  author = {Yuzhang Feng and Veeramani, A. and Kanagasabai, R. and Seungmin Rho},
+  title = {Automatic Service Composition via Model Checking},
+  booktitle = {Services Computing Conference (APSCC), 2011 IEEE Asia-Pacific},
+  year = {2011},
+  pages = {477 -482},
+  month = {dec.},
+  abstract = {Web service composition is the process of constructing a set of Web
+        services which, when invoked with some user input in a particular
+        order, can produce the output to the user's requirements. This paper
+        proposes a novel model checking based approach for automated service
+        composition. Modeling services as a set of interleaved processes
+        in a class of process algebra, we formulate service composition as
+        model checking asserted on a specific type of property on the model.
+        We show that, under this formulation, correct composition workflows
+        can be constructed from the counter-examples provided by model checking.
+        With a case study on online hotel booking services, we demonstrate
+        that the proposed approach can support directed a cyclic composition
+        graphs and the generated composition graphs are automatically verified.},
+  doi = {10.1109/APSCC.2011.54},
+  file = {:/users/outil/verif/biblio/Composition/AutomaticServiceCompositionViaModelChecking2011.pdf:PDF},
+  keywords = {Web service composition;automated service composition;directed acyclic
+        composition graph;interleaved process;model checking;online hotel
+        booking services;process algebra;user requirements;Web services;directed
+        graphs;formal verification;hotel industry;process algebra;},
+  owner = {cecile},
+  timestamp = {2012.03.07}
+}
+
 @ARTICLE{DBLP:journals/tcad/FeySBD08,
   author = {G{\"o}rschwin Fey and Stefan Staber and Roderick Bloem and Rolf Drechsler},
@@ -2202 +2234 @@
 }
 
+@INCOLLECTION{springerlink:10.1007/978-3-540-68073-4_4,
+  author = {Li, Juncao and Sun, Xiuli and Xie, Fei and Song, Xiaoyu},
+  title = {Component-Based Abstraction and Refinement},
+  booktitle = {High Confidence Software Reuse in Large Systems},
+  publisher = {Springer Berlin / Heidelberg},
+  year = {2008},
+  editor = {Mei, Hong},
+  volume = {5030},
+  series = {Lecture Notes in Computer Science},
+  pages = {39-51},
+  note = {10.1007/978-3},
+  affiliation = {Portland State University Dept. of Computer Science Portland OR 97207},
+  file = {:/users/outil/verif/biblio/Composition/Compponent-Based AbstractionRefinement2008.pdf:PDF},
+  isbn = {978-3-540-68062-8},
+  keyword = {Computer Science},
+  keywords = {Composition, Abstraction, Refinement, verified component, Hardware/software
+        coverification},
+  url = {http://dx.doi.org/10.1007/978-3-540-68073-4_4}
+}
+
 @INPROCEEDINGS{lin91implicit,
   author = {B.~Lin and A.R.~Newton},
@@ -2226 +2278 @@
   address = {Hingham, MA, USA},
   publisher = {Kluwer Academic Publisher}
+}
+
+@INCOLLECTION{springerlink:10.1007/978-3-642-16901-4_15,
+  author = {Lomuscio, Alessio and Strulo, Ben and Walker, Nigel and Wu, Peng},
+  title = {Assume-Guarantee Reasoning with Local Specifications},
+  booktitle = {Formal Methods and Software Engineering},
+  publisher = {Springer Berlin / Heidelberg},
+  year = {2010},
+  editor = {Dong, Jin and Zhu, Huibiao},
+  volume = {6447},
+  series = {Lecture Notes in Computer Science},
+  pages = {204-219},
+  note = {10.1007/978-3-642-16901-4_15},
+  abstract = {We investigate assume-guarantee reasoning for global specifications
+        consisting of conjunctions of local specifications. We present a
+        sound and complete assume-guarantee rule that permits reasoning about
+        individual modules for local specifications and draws conclusions
+        on global specifications. We illustrate our approach with an example
+        from the field of network congestion control, where different agents
+        are responsible for controlling packet flow across a shared infrastructure.
+        In this context, we derive an assume-guarantee rule for system stability,
+        and show that this rule is valuable to reason about any number of
+        agents, any initial flow configuration, and any topology of bounded
+        degree.},
+  affiliation = {Department of Computing, Imperial College London, UK},
+  file = {:/users/outil/verif/biblio/Composition/AGRwithLocalSpecification2010.pdf:PDF},
+  isbn = {978-3-642-16900-7},
+  keyword = {Computer Science},
+  keywords = {Compositional reasoning, composition},
+  owner = {cecile},
+  timestamp = {2012.03.07},
+  url = {http://dx.doi.org/10.1007/978-3-642-16901-4_15}
 }
 
@@ -2448 +2532 @@
   pages = {2-14},
   number = {1},
-  bibsource = {DBLP, http://dblp.uni-trier.de}
+  bibsource = {DBLP, http://dblp.uni-trier.de},
+  keywords = {Abstraction}
 }
 
@@ -2559 +2644 @@
   publisher = {Springer-Verlag},
   url = {http://www.csl.sri.com/papers/cade92-pvs/}
+}
+
+@INCOLLECTION{springerlink:10.1007/3-540-63166-6_5,
+  author = {Pardo, Abelardo and Hachtel, Gary},
+  title = {Automatic abstraction techniques for propositional $\mu$-calculus
+        model checking},
+  booktitle = {Computer Aided Verification},
+  publisher = {Springer Berlin / Heidelberg},
+  year = {1997},
+  editor = {Grumberg, Orna},
+  volume = {1254},
+  series = {Lecture Notes in Computer Science},
+  pages = {12-23},
+  note = {10.1007/3-540-63166-6_5},
+  abstract = {An abstraction/refinement paradigm for the full propositional $\mu$-calculus
+        is presented. No distinction is made between universal or existential
+        fragments. Necessary conditions for conservative verification are
+        provided, along with a fully automatic symbolic model checking abstraction
+        algorithm. The algorithm begins with conservative verification of
+        an initial abstraction. If the conclusion is negative, it derives
+        a ldquogoal setrdquo of states which require further resolution.
+        It then successively refines, with respect to this goal set, the
+        approximations made in the subformulas, until the given formula is
+        verified or computational resources are exhausted.},
+  affiliation = {University of Colorado ECEN Campus Box 425 80309 Boulder CO USA ECEN
+        Campus Box 425 80309 Boulder CO USA},
+  file = {:/users/outil/verif/biblio/Cegar/CAV97_Automatic_Abstraction_Tech_for_Propositional_uCalc_MC.ps:PostScript},
+  isbn = {978-3-540-63166-8},
+  keywords = {Computer Science, Abstraction, model checking, mu-calculus, refinement},
+  owner = {cecile},
+  timestamp = {2012.03.07},
+  url = {http://dx.doi.org/10.1007/3-540-63166-6_5}
+}
+
+@INPROCEEDINGS{Pardo:1998:ICM:277044.277171,
+  author = {Pardo, Abelardo and Hachtel, Gary D.},
+  title = {Incremental CTL model checking using BDD subsetting},
+  booktitle = {Proceedings of the 35th annual Design Automation Conference},
+  year = {1998},
+  series = {DAC '98},
+  pages = {457--462},
+  address = {New York, NY, USA},
+  publisher = {ACM},
+  abstract = {An automatic abstraction/refinement algorithm for symbolic CTL model
+        checking is presented. Conservative model checking is thus done for
+        the full CTL language-no restriction is made to the universal or
+        existen tial fragments. The algorithm begins with conserv ativ everification
+        of an initial abstraction. If the conclusion is negativ e,it deriv
+        es a ¿goal set¿ of states which require further resolution. It then
+        successiv ely refines, with respect to this goal set, the appro ximations
+        made in the sub-formulas, until the giv en form ula is v erified
+        or computational resources are exhausted. This method applies uniformly
+        to the abstractions based in over-appro ximation as well as under-approximations
+        of the model. Both the refinement and the abstraction procedures
+        are based in BDD-subsetting. Note that refinement procedures which
+        are based on error traces, are limited to over-appro ximation on
+        the universal fragment (or for language con tainment), whereas the
+        goal set method is applicable to all consisten t appro ximations,
+        and for all CTL formulas.},
+  acmid = {277171},
+  doi = {10.1145/277044.277171},
+  file = {:/users/outil/verif/biblio/Cegar/DAC98_Incremental CTL Model Checking Using BDD Subsetting.pdf:PDF},
+  isbn = {0-89791-964-5},
+  keywords = {CTL, model checking, Abstraction},
+  location = {San Francisco, California, United States},
+  numpages = {6},
+  url = {http://doi.acm.org/10.1145/277044.277171}
 }
 
@@ -2874 +3026 @@
   publisher = {IEEE Computer Society},
   doi = {http://dx.doi.org/10.1109/LICS.2006.5},
+  keywords = {Abstraction, 3-valued},
   owner = {cecile},
   timestamp = {2007.01.14}
@@ -2935 +3088 @@
   owner = {cecile},
   timestamp = {2006.02.09}
+}
+
+@INPROCEEDINGS{Tripakis201,
+  author = {Tripakis, Stavros and Andrade, Hugo and Ghosal, Arkadeb and Limaye,
+        Rhishikesh and Ravindran, Kaushik and Wang, Guoqiang and Yang, Guang
+        and Kormerup, Jacob and Wong, Ian},
+  title = {Correct and non-defensive glue design using abstract models},
+  booktitle = {Proceedings of the seventh IEEE/ACM/IFIP international conference
+        on Hardware/software codesign and system synthesis},
+  year = {2011},
+  series = {CODES+ISSS '11},
+  pages = {59--68},
+  address = {New York, NY, USA},
+  publisher = {ACM},
+  abstract = { Current hardware design practice often relies on integration of components,
+        some of which may be IP or legacy blocks. While integration eases
+        design by allowing modularization and component reuse, it is still
+        done in a mostly ad hoc manner. Designers work with descriptions
+        of components that are either informal or incomplete (e.g., documents
+        in English, structural but non-behavioral specifications in IP-XACT)
+        or too low-level (e.g., HDL code), and have little to no automatic
+        support for stitching the components together. Providing such support
+        is the glue design problem.
+        
+        This paper addresses this problem using a model-based approach. The
+        key idea is to use high-level models, such as dataflow graphs, that
+        enable efficient automated analysis. The analysis can be used to
+        derive performance properties of the system (e.g., component compatibility,
+        throughput, etc.), optimize resource usage (e.g., buffer sizes),
+        and even synthesize low-level code (e.g., control logic). However,
+        these models are only abstractions of the real system, and often
+        omit critical information. As a result, the analysis outcomes may
+        be defensive (e.g., buffers that are too big) or even incorrect (e.g.,
+        buffers that are too small). The paper examines these situations
+        and proposes a correct and non-defensive design methodology that
+        employs the right models to explore accurate performance and resource
+        trade-offs. },
+  acmid = {2039382},
+  doi = {http://doi.acm.org/10.1145/2039370.2039382},
+  isbn = {978-1-4503-0715-4},
+  keywords = {abstraction, data flow, glue design, non-defensiveness, composition},
+  location = {Taipei, Taiwan},
+  numpages = {10},
+  owner = {cecile},
+  timestamp = {2012.03.07},
+  url = {http://doi.acm.org/10.1145/2039370.2039382}
 }
 
@@ -3029 +3228 @@
 }
 
+@ARTICLE{5374376,
+  author = {Hao Zheng and Haiqiong Yao and Yoneda, T.},
+  title = {Modular Model Checking of Large Asynchronous Designs with Efficient
+        Abstraction Refinement},
+  journal = {Computers, IEEE Transactions on},
+  year = {2010},
+  volume = {59},
+  pages = {561 -573},
+  number = {4},
+  month = {april },
+  abstract = {Divide-and-conquer is essential to address state explosion in model
+        checking. Verifying each individual component in a system, in isolation,
+        efficiently requires an appropriate context, which traditionally
+        is obtained by hand. This paper presents an efficient modular model
+        checking approach for asynchronous design verification. It is equipped
+        with a novel abstraction refinement method that can refine a component
+        abstraction to be accurate enough for successful verification. It
+        is fully automated, and eliminates the need of finding an accurate
+        context when verifying each individual component, although such a
+        context is still highly desirable. This method is also enhanced with
+        additional state space reduction techniques. The experiments on several
+        nontrivial asynchronous designs show that this method efficiently
+        removes impossible behaviors from each component including ones violating
+        correctness requirements.},
+  doi = {10.1109/TC.2009.187},
+  file = {:/users/outil/verif/biblio/Composition/ModularMCLargeAsynchronousDesignwithAR2010.pdf:PDF},
+  issn = {0018-9340},
+  keywords = {abstraction refinement;abstraction refinement method;large asynchronous
+        designs;modular model checking;state explosion;state space reduction
+        techniques;formal verification;state-space methods; composition},
+  owner = {cecile},
+  review = {Verification of a whole system by verifying each components. When
+        verifying each components individually assumptions has to be made
+        on the environnment ot avoid false counter-examples. Use component
+        abstraction to over-approximated the environment. This abastraction
+        must be refined to obtain only the behavior allowed at the interface.
+        They propose : 
+        
+        <ul>
+        
+        <li>     to identify and remove unsynchronized behavior. 
+        
+         <li> to extend the refinement to more than two components itemize
+        
+        
+        </ul>
+        
+        
+        Main contribution : Local synchronization detection method for component
+        based on parallel composition and an AR methof for modular MC.
+        
+        <br>
+        
+        Circuit class : Asynchronous</td>},
+  timestamp = {2012.03.07}
+}
+
 @PROCEEDINGS{DBLP:conf/fmcad/2002,
   title = {Formal Methods in Computer-Aided Design, 4th International Conference,

biblio/compositional.bib

@@ -144 +144 @@
   doi = {http://doi.acm.org/10.1145/2039370.2039382},
   isbn = {978-1-4503-0715-4},
-  keywords = {abstraction, data flow, glue design, non-defensiveness},
+  keywords = {abstraction, data flow, glue design, non-defensiveness, composition},
   location = {Taipei, Taiwan},
   numpages = {10},
@@ -179 +179 @@
   keywords = {abstraction refinement;abstraction refinement method;large asynchronous
         designs;modular model checking;state explosion;state space reduction
-        techniques;formal verification;state-space methods;}
+        techniques;formal verification;state-space methods; composition},
+  review = {Verification of a whole system by verifying each components. When
+        verifying each components individually assumptions has to be made
+        on the environnment ot avoid false counter-examples. Use component
+        abstraction to over-approximated the environment. This abastraction
+        must be refined to obtain only the behavior allowed at the interface.
+        They propose : \begin{itemize} \item to identify and remove unsynchronized
+        behavior. \item to extend the refinement to more than two components
+        \end{itemize} Main contribution : Local synchronization detection
+        method for component based on parallel composition and an AR methof
+        for modular MC. Circuit class : Asynchronous}
 }
 

biblio/compositional.html

@@ -562 +562 @@
 <thead><tr><th width="20%">Author</th><th width="30%">Title</th><th width="4%">Year</th><th width="30%">Journal/Proceedings</th><th width="7%">Reftype</th><th width="4%">DOI/URL</th></tr></thead>
 <tbody>
+<tr id="alder06ticc" class="entry">
+        <td>Adler, B., de Alfaro, L., da Silva, L.D., Faella, M., Legay, A., Raman, V. &amp; Roy, P.&nbsp;Thomas Ball and Robert B. Jones (Ed.)</td>
+        <td>Ticc: A Tool for Interface Compatibility and Composition. <p class="infolinks">[<a href="javascript:toggleInfo('alder06ticc','bibtex')">BibTeX</a>]</p></td>
+        <td>2006</td>
+        <td><br/>Vol. 4144CAV'06: Proceedings of 18th International Conference of Computer Aided Verification, pp. 59-62&nbsp;</td>
+        <td>inproceedings</td>
+        <td>&nbsp;</td>
+</tr>
+<tr id="bib_alder06ticc" class="bibtex noshow">
+<td colspan="7"><b>BibTeX</b>:
+<pre>
+@inproceedings{alder06ticc,
+  author = {B.T.~Adler and L.~de Alfaro and L.~Dias da Silva and M.~Faella and A.~Legay and V.~Raman and P.~Roy},
+  title = {Ticc: A Tool for Interface Compatibility and Composition.},
+  booktitle = {CAV'06: Proceedings of 18th International Conference of Computer Aided Verification},
+  year = {2006},
+  volume = {4144},
+  pages = {59-62}
+}
+</pre></td>
+</tr>
+<tr id="amla01assume" class="entry">
+        <td>Amla, N., Emerson, E.A., Namjoshi, K.S. &amp; Trefler, R.J.&nbsp;</td>
+        <td>Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams <p class="infolinks">[<a href="javascript:toggleInfo('amla01assume','bibtex')">BibTeX</a>]</p></td>
+        <td>2001</td>
+        <td>TACAS 2001: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 465-479&nbsp;</td>
+        <td>inproceedings</td>
+        <td>&nbsp;</td>
+</tr>
+<tr id="bib_amla01assume" class="bibtex noshow">
+<td colspan="7"><b>BibTeX</b>:
+<pre>
+@inproceedings{amla01assume,
+  author = {N.~Amla and E.~A.~Emerson and K.~S.~Namjoshi and R.~J.~Trefler},
+  title = {Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams},
+  booktitle = {TACAS 2001: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
+  publisher = {Springer-Verlag},
+  year = {2001},
+  pages = {465--479}
+}
+</pre></td>
+</tr>
 <tr id="Cabodi09Speeding" class="entry">
         <td>Cabodi, G., Camurati, P., Garcia, L., Murciano, M., Nocco, S. &amp; Quer, S.&nbsp;</td>
-        <td>Speeding up Model Checking by Exploiting Explicit and Hidden Verification Constraints <p class="infolinks">[<a href="javascript:toggleInfo('Cabodi09Speeding','abstract')">Abstract</a>] [<a href="javascript:toggleInfo('Cabodi09Speeding','bibtex')">BibTeX</a>]</p></td>
+        <td>Speeding up Model Checking by Exploiting Explicit and Hidden Verification Constraints <p class="infolinks">[<a href="javascript:toggleInfo('Cabodi09Speeding','bibtex')">BibTeX</a>]</p></td>
         <td>2009</td>
         <td>DATE '09: Proceedings of the conference on Design, Automation and Test in Europe, pp. 1686-1691&nbsp;</td>
         <td>inproceedings</td>
         <td>&nbsp;</td>
-</tr>
-<tr id="abs_Cabodi09Speeding" class="abstract noshow">
-        <td colspan="7"><b>Abstract</b>: Constraints represent a key component of state-<p>of-the-art verification tools based on compositional approaches<p>and assume–guarantee reasoning. In recent years, most of the<p>research efforts on verification constraints have focused on<p>defining formats and techniques to encode, or to synthesize,<p>constraints starting from the specification of the design.<p>In this paper, we analyze the impact of constraints on the<p>performance of model checking tools, and we discuss how to<p>effectively exploit them. We also introduce an approach to<p>explicitly derive verification constraints hidden in the design<p>and/or in the property under verification. Such constraints may<p>simply come from true design constraints, embedded within the<p>properties, or may be generated in the general effort to reduce or<p>partition the state space. Experimental results show that, in both<p>cases, we can reap benefits for the overall verification process<p>in several hard-to-solve designs, where we obtain speed-ups of<p>more than one order of magnitude.</td>
 </tr>
 <tr id="bib_Cabodi09Speeding" class="bibtex noshow">
@@ -582 +621 @@
   year = {2009},
   pages = {1686-1691}
+}
+</pre></td>
+</tr>
+<tr id="Cansell2001AbstractionandRefinementofFeatures" class="entry">
+        <td>Cansell, D. &amp; M&eacute;ry, D.&nbsp;S. Gilmore and M. Ryan (Ed.)</td>
+        <td>Abstraction and Refinement of Features <p class="infolinks">[<a href="javascript:toggleInfo('Cansell2001AbstractionandRefinementofFeatures','abstract')">Abstract</a>] [<a href="javascript:toggleInfo('Cansell2001AbstractionandRefinementofFeatures','bibtex')">BibTeX</a>]</p></td>
+        <td>2001</td>
+        <td>Language Constructs for Designing Features, pp. 65-84&nbsp;</td>
+        <td>incollection</td>
+        <td>&nbsp;</td>
+</tr>
+<tr id="abs_Cansell2001AbstractionandRefinementofFeatures" class="abstract noshow">
+        <td colspan="7"><b>Abstract</b>: The composition of services and features often leads to unwanted situations, because it is a non-monotonic operation over services and features. When a new service is added to an existing system, conditions have to be checked to ensure that the resulting system satisfies a list of required properties. Following the system approach of Abrial, we develop services and features in an incremental way and use refinement to model the composition of services and features. Proof obligations state the preservation or the non-preservation of properties, namely invariant or more generally safety properties. The method helps us in understanding when a service is interfering with another, and allows us to give multiple views of each service according to the level of its refinement. Finally, we validate our method with the Atelier B tool.</td>
+</tr>
+<tr id="bib_Cansell2001AbstractionandRefinementofFeatures" class="bibtex noshow">
+<td colspan="7"><b>BibTeX</b>:
+<pre>
+@incollection{Cansell2001AbstractionandRefinementofFeatures,
+  author = {D.~Cansell and D.~M&eacute;ry},
+  title = {Abstraction and Refinement of Features},
+  booktitle = {Language Constructs for Designing Features},
+  publisher = {Springer-Verlag},
+  year = {2001},
+  pages = {65--84}
+}
+</pre></td>
+</tr>
+<tr id="DBLP:conf/lics/ClarkeLM89" class="entry">
+        <td>Clarke, E.M., Long, D.E. &amp; McMillan, K.L.&nbsp;</td>
+        <td>Compositional Model Checking <p class="infolinks">[<a href="javascript:toggleInfo('DBLP:conf/lics/ClarkeLM89','bibtex')">BibTeX</a>]</p></td>
+        <td>1989</td>
+        <td>LICS'89: Proceedings of the 4th Annual Symposium on Logic in Computer Science, pp. 353-362&nbsp;</td>
+        <td>inproceedings</td>
+        <td>&nbsp;</td>
+</tr>
+<tr id="bib_DBLP:conf/lics/ClarkeLM89" class="bibtex noshow">
+<td colspan="7"><b>BibTeX</b>:
+<pre>
+@inproceedings{DBLP:conf/lics/ClarkeLM89,
+  author = {E.~M.~Clarke and D.~E.~Long and K.~L.~McMillan},
+  title = {Compositional Model Checking},
+  booktitle = {LICS'89: Proceedings of the 4th Annual Symposium on Logic in Computer Science},
+  publisher = {IEEE Computer Society},
+  year = {1989},
+  pages = {353-362}
 }
 </pre></td>
@@ -606 +690 @@
   pages = {477 -482},
   doi = {http://dx.doi.org/10.1109/APSCC.2011.54}
+}
+</pre></td>
+</tr>
+<tr id="jhala01microarchi" class="entry">
+        <td>Jhala, R. &amp; McMillan, K.&nbsp;Alain Finkel G&eacute;rard Berry, Hubert Comon (Ed.)</td>
+        <td>Microarchitecture Verification by Compositional Model Checking. <p class="infolinks">[<a href="javascript:toggleInfo('jhala01microarchi','bibtex')">BibTeX</a>]</p></td>
+        <td>2001</td>
+        <td><br/>Vol. 2102CAV'01: Proceedings of the 13th International Conference on Computer Aided Verification, pp. 396-410&nbsp;</td>
+        <td>inproceedings</td>
+        <td>&nbsp;</td>
+</tr>
+<tr id="bib_jhala01microarchi" class="bibtex noshow">
+<td colspan="7"><b>BibTeX</b>:
+<pre>
+@inproceedings{jhala01microarchi,
+  author = {Jhala, R. and McMillan, K.L.},
+  title = {Microarchitecture Verification by Compositional Model Checking.},
+  booktitle = {CAV'01: Proceedings of the 13th International Conference on Computer Aided Verification},
+  publisher = {Springer},
+  year = {2001},
+  volume = {2102},
+  pages = {396-410}
+}
+</pre></td>
+</tr>
+<tr id="springerlink:10.1007/978-3-540-68073-4_4" class="entry">
+        <td>Li, J., Sun, X., Xie, F. &amp; Song, X.&nbsp;Hong Mei (Ed.)</td>
+        <td>Component-Based Abstraction and Refinement <p class="infolinks">[<a href="javascript:toggleInfo('springerlink:10.1007/978-3-540-68073-4_4','bibtex')">BibTeX</a>]</p></td>
+        <td>2008</td>
+        <td><br/>Vol. 5030High Confidence Software Reuse in Large Systems, pp. 39-51&nbsp;</td>
+        <td>incollection</td>
+        <td><a href="http://dx.doi.org/10.1007/978-3-540-68073-4_4">URL</a>&nbsp;</td>
+</tr>
+<tr id="bib_springerlink:10.1007/978-3-540-68073-4_4" class="bibtex noshow">
+<td colspan="7"><b>BibTeX</b>:
+<pre>
+@incollection{springerlink:10.1007/978-3-540-68073-4_4,
+  author = {Li, Juncao and Sun, Xiuli and Xie, Fei and Song, Xiaoyu},
+  title = {Component-Based Abstraction and Refinement},
+  booktitle = {High Confidence Software Reuse in Large Systems},
+  publisher = {Springer Berlin / Heidelberg},
+  year = {2008},
+  volume = {5030},
+  pages = {39-51},
+  note = {10.1007/978-3},
+  url = {http://dx.doi.org/10.1007/978-3-540-68073-4_4}
 }
 </pre></td>
@@ -636 +766 @@
 </pre></td>
 </tr>
+<tr id="long93thesis" class="entry">
+        <td>Long, D.E.&nbsp;</td>
+        <td>Model Checking, Abstraction, and Compositional Verification <p class="infolinks">[<a href="javascript:toggleInfo('long93thesis','bibtex')">BibTeX</a>]</p></td>
+        <td>1993</td>
+        <td><i>School</i>: Carnegie Mellon University&nbsp;</td>
+        <td>phdthesis</td>
+        <td>&nbsp;</td>
+</tr>
+<tr id="bib_long93thesis" class="bibtex noshow">
+<td colspan="7"><b>BibTeX</b>:
+<pre>
+@phdthesis{long93thesis,
+  author = {D.~E.~Long},
+  title = {Model Checking, Abstraction, and Compositional Verification},
+  school = {Carnegie Mellon University},
+  year = {1993}
+}
+</pre></td>
+</tr>
+<tr id="mcmillan98tomasulo" class="entry">
+        <td>McMillan, K.&nbsp;Moshe Y. Vardi Alan J. Hu (Ed.)</td>
+        <td>Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking. <p class="infolinks">[<a href="javascript:toggleInfo('mcmillan98tomasulo','bibtex')">BibTeX</a>]</p></td>
+        <td>1998</td>
+        <td><br/>Vol. 1427CAV'98: Proceddings of the 10th International Conference on Computer Aided Verification, pp. 110-121&nbsp;</td>
+        <td>inproceedings</td>
+        <td>&nbsp;</td>
+</tr>
+<tr id="bib_mcmillan98tomasulo" class="bibtex noshow">
+<td colspan="7"><b>BibTeX</b>:
+<pre>
+@inproceedings{mcmillan98tomasulo,
+  author = {K.L.~McMillan},
+  title = {Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking.},
+  booktitle = {CAV'98: Proceddings of the 10th International Conference on Computer Aided Verification},
+  publisher = {Springer},
+  year = {1998},
+  volume = {1427},
+  pages = {110-121}
+}
+</pre></td>
+</tr>
+<tr id="mcmillan00methodology" class="entry">
+        <td>McMillan, K.&nbsp;</td>
+        <td>A Methodology for Hardware Verification Using Compositional Model Checking <p class="infolinks">[<a href="javascript:toggleInfo('mcmillan00methodology','bibtex')">BibTeX</a>]</p></td>
+        <td>2000</td>
+        <td>Science of Computer Programming<br/>Vol. 37(1-3), pp. 279-309&nbsp;</td>
+        <td>article</td>
+        <td><a href="citeseer.ist.psu.edu/mcmillan99methodology.html">URL</a>&nbsp;</td>
+</tr>
+<tr id="bib_mcmillan00methodology" class="bibtex noshow">
+<td colspan="7"><b>BibTeX</b>:
+<pre>
+@article{mcmillan00methodology,
+  author = {K.L. McMillan},
+  title = {A Methodology for Hardware Verification Using Compositional Model Checking},
+  journal = {Science of Computer Programming},
+  year = {2000},
+  volume = {37},
+  number = {1--3},
+  pages = {279--309},
+  url = {citeseer.ist.psu.edu/mcmillan99methodology.html}
+}
+</pre></td>
+</tr>
+<tr id="DBLP:conf/cav/McMillan97" class="entry">
+        <td>McMillan, K.L.&nbsp;Orna Grumberg (Ed.)</td>
+        <td>A Compositional Rule for Hardware Design Refinement. <p class="infolinks">[<a href="javascript:toggleInfo('DBLP:conf/cav/McMillan97','bibtex')">BibTeX</a>]</p></td>
+        <td>1997</td>
+        <td><br/>Vol. 1254CAV'97: Proceedings of the 9th International Conference on Computer Aided Verification, pp. 24-35&nbsp;</td>
+        <td>inproceedings</td>
+        <td>&nbsp;</td>
+</tr>
+<tr id="bib_DBLP:conf/cav/McMillan97" class="bibtex noshow">
+<td colspan="7"><b>BibTeX</b>:
+<pre>
+@inproceedings{DBLP:conf/cav/McMillan97,
+  author = {Kenneth L. McMillan},
+  title = {A Compositional Rule for Hardware Design Refinement.},
+  booktitle = {CAV'97: Proceedings of the 9th International Conference on Computer Aided Verification},
+  publisher = {Springer},
+  year = {1997},
+  volume = {1254},
+  pages = {24-35}
+}
+</pre></td>
+</tr>
+<tr id="peng02thesis" class="entry">
+        <td>Peng, H.&nbsp;</td>
+        <td>Improving Compositional Verification through Environment Synthesis and Syntactic Model Reduction <p class="infolinks">[<a href="javascript:toggleInfo('peng02thesis','bibtex')">BibTeX</a>]</p></td>
+        <td>2002</td>
+        <td><i>School</i>: Dept. of Electrical and Computer Engenering, Concordia University, Montreal, Quebec, Canada&nbsp;</td>
+        <td>phdthesis</td>
+        <td>&nbsp;</td>
+</tr>
+<tr id="bib_peng02thesis" class="bibtex noshow">
+<td colspan="7"><b>BibTeX</b>:
+<pre>
+@phdthesis{peng02thesis,
+  author = {H.~Peng},
+  title = {Improving Compositional Verification through Environment Synthesis and Syntactic Model Reduction},
+  school = {Dept. of Electrical and Computer Engenering, Concordia University, Montreal, Quebec, Canada},
+  year = {2002}
+}
+</pre></td>
+</tr>
+<tr id="peng02tableau" class="entry">
+        <td>Peng, H., Mokhtari, Y. &amp; Tahar, S.&nbsp;</td>
+        <td>Environment Synthesis for Compositional Model Checking. <p class="infolinks">[<a href="javascript:toggleInfo('peng02tableau','bibtex')">BibTeX</a>]</p></td>
+        <td>2002</td>
+        <td>ICCD'02: Proceedings of the 20th International Conference on Computer Design, pp. 70-&nbsp;</td>
+        <td>inproceedings</td>
+        <td>&nbsp;</td>
+</tr>
+<tr id="bib_peng02tableau" class="bibtex noshow">
+<td colspan="7"><b>BibTeX</b>:
+<pre>
+@inproceedings{peng02tableau,
+  author = {H.~Peng and Y.~Mokhtari and S.~Tahar},
+  title = {Environment Synthesis for Compositional Model Checking.},
+  booktitle = {ICCD'02: Proceedings of the 20th International Conference on Computer Design},
+  publisher = {IEEE Computer Society},
+  year = {2002},
+  pages = {70-}
+}
+</pre></td>
+</tr>
 <tr id="Tripakis201" class="entry">
         <td>Tripakis, S., Andrade, H., Ghosal, A., Limaye, R., Ravindran, K., Wang, G., Yang, G., Kormerup, J. &amp; Wong, I.&nbsp;</td>
@@ -662 +918 @@
 </pre></td>
 </tr>
+<tr id="xie03verified" class="entry">
+        <td>Xie, F. &amp; Browne, J.&nbsp;</td>
+        <td>Verified Systems by Composition from Verified Components <p class="infolinks">[<a href="javascript:toggleInfo('xie03verified','bibtex')">BibTeX</a>]</p></td>
+        <td>2003</td>
+        <td>ESEC/FSE 2003 : Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering 2003 held jointly with 9th European Software Engineering Conference, pp. 277-286&nbsp;</td>
+        <td>inproceedings</td>
+        <td><a href="http://doi.acm.org/10.1145/940071.940109">DOI</a> &nbsp;</td>
+</tr>
+<tr id="bib_xie03verified" class="bibtex noshow">
+<td colspan="7"><b>BibTeX</b>:
+<pre>
+@inproceedings{xie03verified,
+  author = {F.~Xie and J.C.~Browne},
+  title = {Verified Systems by Composition from Verified Components},
+  booktitle = {ESEC/FSE 2003 : Proceedings of the 11th ACM SIGSOFT Symposium on Foundations of Software Engineering 2003 held jointly with 9th European Software Engineering Conference},
+  publisher = {ACM Press},
+  year = {2003},
+  pages = {277--286},
+  doi = {http://doi.acm.org/10.1145/940071.940109}
+}
+</pre></td>
+</tr>
 <tr id="5374376" class="entry">
         <td>Zheng, H., Yao, H. &amp; Yoneda, T.&nbsp;</td>
-        <td>Modular Model Checking of Large Asynchronous Designs with Efficient Abstraction Refinement <p class="infolinks">[<a href="javascript:toggleInfo('5374376','abstract')">Abstract</a>] [<a href="javascript:toggleInfo('5374376','bibtex')">BibTeX</a>]</p></td>
+        <td>Modular Model Checking of Large Asynchronous Designs with Efficient Abstraction Refinement <p class="infolinks">[<a href="javascript:toggleInfo('5374376','abstract')">Abstract</a>] [<a href="javascript:toggleInfo('5374376','review')">Review</a>] [<a href="javascript:toggleInfo('5374376','bibtex')">BibTeX</a>]</p></td>
         <td>2010</td>
         <td>Computers, IEEE Transactions on<br/>Vol. 59(4), pp. 561 -573&nbsp;</td>
@@ -672 +950 @@
 <tr id="abs_5374376" class="abstract noshow">
         <td colspan="7"><b>Abstract</b>: Divide-and-conquer is essential to address state explosion in model checking. Verifying each individual component in a system, in isolation, efficiently requires an appropriate context, which traditionally is obtained by hand. This paper presents an efficient modular model checking approach for asynchronous design verification. It is equipped with a novel abstraction refinement method that can refine a component abstraction to be accurate enough for successful verification. It is fully automated, and eliminates the need of finding an accurate context when verifying each individual component, although such a context is still highly desirable. This method is also enhanced with additional state space reduction techniques. The experiments on several nontrivial asynchronous designs show that this method efficiently removes impossible behaviors from each component including ones violating correctness requirements.</td>
+</tr>
+<tr id="rev_5374376" class="review noshow">
+        <td colspan="7"><b>Review</b>: Verification of a whole system by verifying each components. When verifying each components individually assumptions has to be made on the environnment ot avoid false counter-examples. Use component abstraction to over-approximated the environment. This abastraction must be refined to obtain only the behavior allowed at the interface. They propose : <p><ul><p><li>     to identify and remove unsynchronized behavior. <p> <li> to extend the refinement to more than two components itemize <p></ul><p>Main contribution : Local synchronization detection method for component based on parallel composition and an AR methof for modular MC.<p><br><p>Circuit class : Asynchronous</td></td>
 </tr>
 <tr id="bib_5374376" class="bibtex noshow">
@@ -688 +969 @@
 </pre></td>
 </tr>
+<tr id="DBLP:conf/compos/1997" class="entry">
+        <td>&nbsp;Willem P. de Roever and Hans Langmaack and Amir Pnueli (Ed.)</td>
+        <td>Compositionality: The Significant Difference, International Symposium, COMPOS'97, Bad Malente, Germany, September 8-12, 1997. Revised Lectures <p class="infolinks">[<a href="javascript:toggleInfo('DBLP:conf/compos/1997','bibtex')">BibTeX</a>]</p></td>
+        <td>1998</td>
+        <td><br/>Vol. 1536COMPOS&nbsp;</td>
+        <td>proceedings</td>
+        <td>&nbsp;</td>
+</tr>
+<tr id="bib_DBLP:conf/compos/1997" class="bibtex noshow">
+<td colspan="7"><b>BibTeX</b>:
+<pre>
+@proceedings{DBLP:conf/compos/1997,,
+  title = {Compositionality: The Significant Difference, International Symposium, COMPOS'97, Bad Malente, Germany, September 8-12, 1997. Revised Lectures},
+  booktitle = {COMPOS},
+  publisher = {Springer},
+  year = {1998},
+  volume = {1536}
+}
+</pre></td>
+</tr>
 </tbody>
 </table>
 
 <p>
- <small>Created by <a href="http://jabref.sourceforge.net">JabRef</a> on 01/03/2012.</small>
+ <small>Created by <a href="http://jabref.sourceforge.net">JabRef</a> on 07/03/2012.</small>
 </p>