Changes between Version 4 and Version 5 of CompositionalBiblio

Timestamp:

Mar 1, 2012, 1:09:41 PM (13 years ago)

Author:

cecile

Comment:

--

CompositionalBiblio

@@ -670 +670 @@
 <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>
@@ -679 +679 @@
         <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 : 
+<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>
+
+</tr>
+
 <tr id="bib_5374376" class="bibtex noshow">
 <td colspan="7"><b>BibTeX</b>: