Ignore:
Timestamp:
Mar 7, 2012, 11:42:59 AM (12 years ago)
Author:
cecile
Message:

new articles for components based abstraction and compostion added

File:
1 edited

Legend:

Unmodified
Added
Removed

  • biblio/compositional.html

    r46 r51  
    562562<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>
    563563<tbody>
     564<tr id="alder06ticc" class="entry">
     565        <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>
     566        <td>Ticc: A Tool for Interface Compatibility and Composition. <p class="infolinks">[<a href="javascript:toggleInfo('alder06ticc','bibtex')">BibTeX</a>]</p></td>
     567        <td>2006</td>
     568        <td><br/>Vol. 4144CAV'06: Proceedings of 18th International Conference of Computer Aided Verification, pp. 59-62&nbsp;</td>
     569        <td>inproceedings</td>
     570        <td>&nbsp;</td>
     571</tr>
     572<tr id="bib_alder06ticc" class="bibtex noshow">
     573<td colspan="7"><b>BibTeX</b>:
     574<pre>
     575@inproceedings{alder06ticc,
     576  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},
     577  title = {Ticc: A Tool for Interface Compatibility and Composition.},
     578  booktitle = {CAV'06: Proceedings of 18th International Conference of Computer Aided Verification},
     579  year = {2006},
     580  volume = {4144},
     581  pages = {59-62}
     582}
     583</pre></td>
     584</tr>
     585<tr id="amla01assume" class="entry">
     586        <td>Amla, N., Emerson, E.A., Namjoshi, K.S. &amp; Trefler, R.J.&nbsp;</td>
     587        <td>Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams <p class="infolinks">[<a href="javascript:toggleInfo('amla01assume','bibtex')">BibTeX</a>]</p></td>
     588        <td>2001</td>
     589        <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>
     590        <td>inproceedings</td>
     591        <td>&nbsp;</td>
     592</tr>
     593<tr id="bib_amla01assume" class="bibtex noshow">
     594<td colspan="7"><b>BibTeX</b>:
     595<pre>
     596@inproceedings{amla01assume,
     597  author = {N.~Amla and E.~A.~Emerson and K.~S.~Namjoshi and R.~J.~Trefler},
     598  title = {Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams},
     599  booktitle = {TACAS 2001: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems},
     600  publisher = {Springer-Verlag},
     601  year = {2001},
     602  pages = {465--479}
     603}
     604</pre></td>
     605</tr>
    564606<tr id="Cabodi09Speeding" class="entry">
    565607        <td>Cabodi, G., Camurati, P., Garcia, L., Murciano, M., Nocco, S. &amp; Quer, S.&nbsp;</td>
    566         <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>
     608        <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>
    567609        <td>2009</td>
    568610        <td>DATE '09: Proceedings of the conference on Design, Automation and Test in Europe, pp. 1686-1691&nbsp;</td>
    569611        <td>inproceedings</td>
    570612        <td>&nbsp;</td>
    571 </tr>
    572 <tr id="abs_Cabodi09Speeding" class="abstract noshow">
    573         <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>
    574613</tr>
    575614<tr id="bib_Cabodi09Speeding" class="bibtex noshow">
    … …  
    582621  year = {2009},
    583622  pages = {1686-1691}
     623}
     624</pre></td>
     625</tr>
     626<tr id="Cansell2001AbstractionandRefinementofFeatures" class="entry">
     627        <td>Cansell, D. &amp; M&eacute;ry, D.&nbsp;S. Gilmore and M. Ryan (Ed.)</td>
     628        <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>
     629        <td>2001</td>
     630        <td>Language Constructs for Designing Features, pp. 65-84&nbsp;</td>
     631        <td>incollection</td>
     632        <td>&nbsp;</td>
     633</tr>
     634<tr id="abs_Cansell2001AbstractionandRefinementofFeatures" class="abstract noshow">
     635        <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>
     636</tr>
     637<tr id="bib_Cansell2001AbstractionandRefinementofFeatures" class="bibtex noshow">
     638<td colspan="7"><b>BibTeX</b>:
     639<pre>
     640@incollection{Cansell2001AbstractionandRefinementofFeatures,
     641  author = {D.~Cansell and D.~M&eacute;ry},
     642  title = {Abstraction and Refinement of Features},
     643  booktitle = {Language Constructs for Designing Features},
     644  publisher = {Springer-Verlag},
     645  year = {2001},
     646  pages = {65--84}
     647}
     648</pre></td>
     649</tr>
     650<tr id="DBLP:conf/lics/ClarkeLM89" class="entry">
     651        <td>Clarke, E.M., Long, D.E. &amp; McMillan, K.L.&nbsp;</td>
     652        <td>Compositional Model Checking <p class="infolinks">[<a href="javascript:toggleInfo('DBLP:conf/lics/ClarkeLM89','bibtex')">BibTeX</a>]</p></td>
     653        <td>1989</td>
     654        <td>LICS'89: Proceedings of the 4th Annual Symposium on Logic in Computer Science, pp. 353-362&nbsp;</td>
     655        <td>inproceedings</td>
     656        <td>&nbsp;</td>
     657</tr>
     658<tr id="bib_DBLP:conf/lics/ClarkeLM89" class="bibtex noshow">
     659<td colspan="7"><b>BibTeX</b>:
     660<pre>
     661@inproceedings{DBLP:conf/lics/ClarkeLM89,
     662  author = {E.~M.~Clarke and D.~E.~Long and K.~L.~McMillan},
     663  title = {Compositional Model Checking},
     664  booktitle = {LICS'89: Proceedings of the 4th Annual Symposium on Logic in Computer Science},
     665  publisher = {IEEE Computer Society},
     666  year = {1989},
     667  pages = {353-362}
    584668}
    585669</pre></td>
    … …  
    606690  pages = {477 -482},
    607691  doi = {http://dx.doi.org/10.1109/APSCC.2011.54}
     692}
     693</pre></td>
     694</tr>
     695<tr id="jhala01microarchi" class="entry">
     696        <td>Jhala, R. &amp; McMillan, K.&nbsp;Alain Finkel G&eacute;rard Berry, Hubert Comon (Ed.)</td>
     697        <td>Microarchitecture Verification by Compositional Model Checking. <p class="infolinks">[<a href="javascript:toggleInfo('jhala01microarchi','bibtex')">BibTeX</a>]</p></td>
     698        <td>2001</td>
     699        <td><br/>Vol. 2102CAV'01: Proceedings of the 13th International Conference on Computer Aided Verification, pp. 396-410&nbsp;</td>
     700        <td>inproceedings</td>
     701        <td>&nbsp;</td>
     702</tr>
     703<tr id="bib_jhala01microarchi" class="bibtex noshow">
     704<td colspan="7"><b>BibTeX</b>:
     705<pre>
     706@inproceedings{jhala01microarchi,
     707  author = {Jhala, R. and McMillan, K.L.},
     708  title = {Microarchitecture Verification by Compositional Model Checking.},
     709  booktitle = {CAV'01: Proceedings of the 13th International Conference on Computer Aided Verification},
     710  publisher = {Springer},
     711  year = {2001},
     712  volume = {2102},
     713  pages = {396-410}
     714}
     715</pre></td>
     716</tr>
     717<tr id="springerlink:10.1007/978-3-540-68073-4_4" class="entry">
     718        <td>Li, J., Sun, X., Xie, F. &amp; Song, X.&nbsp;Hong Mei (Ed.)</td>
     719        <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>
     720        <td>2008</td>
     721        <td><br/>Vol. 5030High Confidence Software Reuse in Large Systems, pp. 39-51&nbsp;</td>
     722        <td>incollection</td>
     723        <td><a href="http://dx.doi.org/10.1007/978-3-540-68073-4_4">URL</a>&nbsp;</td>
     724</tr>
     725<tr id="bib_springerlink:10.1007/978-3-540-68073-4_4" class="bibtex noshow">
     726<td colspan="7"><b>BibTeX</b>:
     727<pre>
     728@incollection{springerlink:10.1007/978-3-540-68073-4_4,
     729  author = {Li, Juncao and Sun, Xiuli and Xie, Fei and Song, Xiaoyu},
     730  title = {Component-Based Abstraction and Refinement},
     731  booktitle = {High Confidence Software Reuse in Large Systems},
     732  publisher = {Springer Berlin / Heidelberg},
     733  year = {2008},
     734  volume = {5030},
     735  pages = {39-51},
     736  note = {10.1007/978-3},
     737  url = {http://dx.doi.org/10.1007/978-3-540-68073-4_4}
    608738}
    609739</pre></td>
    … …  
    636766</pre></td>
    637767</tr>
     768<tr id="long93thesis" class="entry">
     769        <td>Long, D.E.&nbsp;</td>
     770        <td>Model Checking, Abstraction, and Compositional Verification <p class="infolinks">[<a href="javascript:toggleInfo('long93thesis','bibtex')">BibTeX</a>]</p></td>
     771        <td>1993</td>
     772        <td><i>School</i>: Carnegie Mellon University&nbsp;</td>
     773        <td>phdthesis</td>
     774        <td>&nbsp;</td>
     775</tr>
     776<tr id="bib_long93thesis" class="bibtex noshow">
     777<td colspan="7"><b>BibTeX</b>:
     778<pre>
     779@phdthesis{long93thesis,
     780  author = {D.~E.~Long},
     781  title = {Model Checking, Abstraction, and Compositional Verification},
     782  school = {Carnegie Mellon University},
     783  year = {1993}
     784}
     785</pre></td>
     786</tr>
     787<tr id="mcmillan98tomasulo" class="entry">
     788        <td>McMillan, K.&nbsp;Moshe Y. Vardi Alan J. Hu (Ed.)</td>
     789        <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>
     790        <td>1998</td>
     791        <td><br/>Vol. 1427CAV'98: Proceddings of the 10th International Conference on Computer Aided Verification, pp. 110-121&nbsp;</td>
     792        <td>inproceedings</td>
     793        <td>&nbsp;</td>
     794</tr>
     795<tr id="bib_mcmillan98tomasulo" class="bibtex noshow">
     796<td colspan="7"><b>BibTeX</b>:
     797<pre>
     798@inproceedings{mcmillan98tomasulo,
     799  author = {K.L.~McMillan},
     800  title = {Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking.},
     801  booktitle = {CAV'98: Proceddings of the 10th International Conference on Computer Aided Verification},
     802  publisher = {Springer},
     803  year = {1998},
     804  volume = {1427},
     805  pages = {110-121}
     806}
     807</pre></td>
     808</tr>
     809<tr id="mcmillan00methodology" class="entry">
     810        <td>McMillan, K.&nbsp;</td>
     811        <td>A Methodology for Hardware Verification Using Compositional Model Checking <p class="infolinks">[<a href="javascript:toggleInfo('mcmillan00methodology','bibtex')">BibTeX</a>]</p></td>
     812        <td>2000</td>
     813        <td>Science of Computer Programming<br/>Vol. 37(1-3), pp. 279-309&nbsp;</td>
     814        <td>article</td>
     815        <td><a href="citeseer.ist.psu.edu/mcmillan99methodology.html">URL</a>&nbsp;</td>
     816</tr>
     817<tr id="bib_mcmillan00methodology" class="bibtex noshow">
     818<td colspan="7"><b>BibTeX</b>:
     819<pre>
     820@article{mcmillan00methodology,
     821  author = {K.L. McMillan},
     822  title = {A Methodology for Hardware Verification Using Compositional Model Checking},
     823  journal = {Science of Computer Programming},
     824  year = {2000},
     825  volume = {37},
     826  number = {1--3},
     827  pages = {279--309},
     828  url = {citeseer.ist.psu.edu/mcmillan99methodology.html}
     829}
     830</pre></td>
     831</tr>
     832<tr id="DBLP:conf/cav/McMillan97" class="entry">
     833        <td>McMillan, K.L.&nbsp;Orna Grumberg (Ed.)</td>
     834        <td>A Compositional Rule for Hardware Design Refinement. <p class="infolinks">[<a href="javascript:toggleInfo('DBLP:conf/cav/McMillan97','bibtex')">BibTeX</a>]</p></td>
     835        <td>1997</td>
     836        <td><br/>Vol. 1254CAV'97: Proceedings of the 9th International Conference on Computer Aided Verification, pp. 24-35&nbsp;</td>
     837        <td>inproceedings</td>
     838        <td>&nbsp;</td>
     839</tr>
     840<tr id="bib_DBLP:conf/cav/McMillan97" class="bibtex noshow">
     841<td colspan="7"><b>BibTeX</b>:
     842<pre>
     843@inproceedings{DBLP:conf/cav/McMillan97,
     844  author = {Kenneth L. McMillan},
     845  title = {A Compositional Rule for Hardware Design Refinement.},
     846  booktitle = {CAV'97: Proceedings of the 9th International Conference on Computer Aided Verification},
     847  publisher = {Springer},
     848  year = {1997},
     849  volume = {1254},
     850  pages = {24-35}
     851}
     852</pre></td>
     853</tr>
     854<tr id="peng02thesis" class="entry">
     855        <td>Peng, H.&nbsp;</td>
     856        <td>Improving Compositional Verification through Environment Synthesis and Syntactic Model Reduction <p class="infolinks">[<a href="javascript:toggleInfo('peng02thesis','bibtex')">BibTeX</a>]</p></td>
     857        <td>2002</td>
     858        <td><i>School</i>: Dept. of Electrical and Computer Engenering, Concordia University, Montreal, Quebec, Canada&nbsp;</td>
     859        <td>phdthesis</td>
     860        <td>&nbsp;</td>
     861</tr>
     862<tr id="bib_peng02thesis" class="bibtex noshow">
     863<td colspan="7"><b>BibTeX</b>:
     864<pre>
     865@phdthesis{peng02thesis,
     866  author = {H.~Peng},
     867  title = {Improving Compositional Verification through Environment Synthesis and Syntactic Model Reduction},
     868  school = {Dept. of Electrical and Computer Engenering, Concordia University, Montreal, Quebec, Canada},
     869  year = {2002}
     870}
     871</pre></td>
     872</tr>
     873<tr id="peng02tableau" class="entry">
     874        <td>Peng, H., Mokhtari, Y. &amp; Tahar, S.&nbsp;</td>
     875        <td>Environment Synthesis for Compositional Model Checking. <p class="infolinks">[<a href="javascript:toggleInfo('peng02tableau','bibtex')">BibTeX</a>]</p></td>
     876        <td>2002</td>
     877        <td>ICCD'02: Proceedings of the 20th International Conference on Computer Design, pp. 70-&nbsp;</td>
     878        <td>inproceedings</td>
     879        <td>&nbsp;</td>
     880</tr>
     881<tr id="bib_peng02tableau" class="bibtex noshow">
     882<td colspan="7"><b>BibTeX</b>:
     883<pre>
     884@inproceedings{peng02tableau,
     885  author = {H.~Peng and Y.~Mokhtari and S.~Tahar},
     886  title = {Environment Synthesis for Compositional Model Checking.},
     887  booktitle = {ICCD'02: Proceedings of the 20th International Conference on Computer Design},
     888  publisher = {IEEE Computer Society},
     889  year = {2002},
     890  pages = {70-}
     891}
     892</pre></td>
     893</tr>
    638894<tr id="Tripakis201" class="entry">
    639895        <td>Tripakis, S., Andrade, H., Ghosal, A., Limaye, R., Ravindran, K., Wang, G., Yang, G., Kormerup, J. &amp; Wong, I.&nbsp;</td>
    … …  
    662918</pre></td>
    663919</tr>
     920<tr id="xie03verified" class="entry">
     921        <td>Xie, F. &amp; Browne, J.&nbsp;</td>
     922        <td>Verified Systems by Composition from Verified Components <p class="infolinks">[<a href="javascript:toggleInfo('xie03verified','bibtex')">BibTeX</a>]</p></td>
     923        <td>2003</td>
     924        <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>
     925        <td>inproceedings</td>
     926        <td><a href="http://doi.acm.org/10.1145/940071.940109">DOI</a> &nbsp;</td>
     927</tr>
     928<tr id="bib_xie03verified" class="bibtex noshow">
     929<td colspan="7"><b>BibTeX</b>:
     930<pre>
     931@inproceedings{xie03verified,
     932  author = {F.~Xie and J.C.~Browne},
     933  title = {Verified Systems by Composition from Verified Components},
     934  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},
     935  publisher = {ACM Press},
     936  year = {2003},
     937  pages = {277--286},
     938  doi = {http://doi.acm.org/10.1145/940071.940109}
     939}
     940</pre></td>
     941</tr>
    664942<tr id="5374376" class="entry">
    665943        <td>Zheng, H., Yao, H. &amp; Yoneda, T.&nbsp;</td>
    666         <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>
     944        <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>
    667945        <td>2010</td>
    668946        <td>Computers, IEEE Transactions on<br/>Vol. 59(4), pp. 561 -573&nbsp;</td>
    … …  
    672950<tr id="abs_5374376" class="abstract noshow">
    673951        <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>
     952</tr>
     953<tr id="rev_5374376" class="review noshow">
     954        <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>
    674955</tr>
    675956<tr id="bib_5374376" class="bibtex noshow">
    … …  
    688969</pre></td>
    689970</tr>
     971<tr id="DBLP:conf/compos/1997" class="entry">
     972        <td>&nbsp;Willem P. de Roever and Hans Langmaack and Amir Pnueli (Ed.)</td>
     973        <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>
     974        <td>1998</td>
     975        <td><br/>Vol. 1536COMPOS&nbsp;</td>
     976        <td>proceedings</td>
     977        <td>&nbsp;</td>
     978</tr>
     979<tr id="bib_DBLP:conf/compos/1997" class="bibtex noshow">
     980<td colspan="7"><b>BibTeX</b>:
     981<pre>
     982@proceedings{DBLP:conf/compos/1997,,
     983  title = {Compositionality: The Significant Difference, International Symposium, COMPOS'97, Bad Malente, Germany, September 8-12, 1997. Revised Lectures},
     984  booktitle = {COMPOS},
     985  publisher = {Springer},
     986  year = {1998},
     987  volume = {1536}
     988}
     989</pre></td>
     990</tr>
    690991</tbody>
    691992</table>
    692993
    693994<p>
    694  <small>Created by <a href="http://jabref.sourceforge.net">JabRef</a> on 01/03/2012.</small>
     995 <small>Created by <a href="http://jabref.sourceforge.net">JabRef</a> on 07/03/2012.</small>
    695996</p>
    696997
Note: See TracChangeset for help on using the changeset viewer.