Changeset 51 for biblio


Ignore:
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:
3 edited

Legend:

Unmodified
Added
Removed
  • biblio/biblio.bib

    r45 r51  
    448448  bibsource = {DBLP, http://dblp.uni-trier.de},
    449449  crossref = {DBLP:conf/cav/2002},
    450   ee = {http://link.springer.de/link/service/series/0558/bibs/2404/24040137.htm}
     450  ee = {http://link.springer.de/link/service/series/0558/bibs/2404/24040137.htm},
     451  keywords = {Abstraction}
    451452}
    452453
     
    13301331  year = {2007},
    13311332  note = {accepted},
     1333  keywords = {Abstraction, CEGAR, CTL},
    13321334  owner = {cecile},
    13331335  timestamp = {2007.03.27}
     
    14811483  pages = {1686-1691},
    14821484  file = {:Composition/Speeding up MC by exploiting Explicit09.PDF:PDF},
     1485  keywords = {Composition , model checking},
    14831486  owner = {cecile},
    14841487  timestamp = {2009.04.30}
     
    17881791}
    17891792
     1793@INPROCEEDINGS{6128043,
     1794  author = {Yuzhang Feng and Veeramani, A. and Kanagasabai, R. and Seungmin Rho},
     1795  title = {Automatic Service Composition via Model Checking},
     1796  booktitle = {Services Computing Conference (APSCC), 2011 IEEE Asia-Pacific},
     1797  year = {2011},
     1798  pages = {477 -482},
     1799  month = {dec.},
     1800  abstract = {Web service composition is the process of constructing a set of Web
     1801        services which, when invoked with some user input in a particular
     1802        order, can produce the output to the user's requirements. This paper
     1803        proposes a novel model checking based approach for automated service
     1804        composition. Modeling services as a set of interleaved processes
     1805        in a class of process algebra, we formulate service composition as
     1806        model checking asserted on a specific type of property on the model.
     1807        We show that, under this formulation, correct composition workflows
     1808        can be constructed from the counter-examples provided by model checking.
     1809        With a case study on online hotel booking services, we demonstrate
     1810        that the proposed approach can support directed a cyclic composition
     1811        graphs and the generated composition graphs are automatically verified.},
     1812  doi = {10.1109/APSCC.2011.54},
     1813  file = {:/users/outil/verif/biblio/Composition/AutomaticServiceCompositionViaModelChecking2011.pdf:PDF},
     1814  keywords = {Web service composition;automated service composition;directed acyclic
     1815        composition graph;interleaved process;model checking;online hotel
     1816        booking services;process algebra;user requirements;Web services;directed
     1817        graphs;formal verification;hotel industry;process algebra;},
     1818  owner = {cecile},
     1819  timestamp = {2012.03.07}
     1820}
     1821
    17901822@ARTICLE{DBLP:journals/tcad/FeySBD08,
    17911823  author = {G{\"o}rschwin Fey and Stefan Staber and Roderick Bloem and Rolf Drechsler},
     
    22022234}
    22032235
     2236@INCOLLECTION{springerlink:10.1007/978-3-540-68073-4_4,
     2237  author = {Li, Juncao and Sun, Xiuli and Xie, Fei and Song, Xiaoyu},
     2238  title = {Component-Based Abstraction and Refinement},
     2239  booktitle = {High Confidence Software Reuse in Large Systems},
     2240  publisher = {Springer Berlin / Heidelberg},
     2241  year = {2008},
     2242  editor = {Mei, Hong},
     2243  volume = {5030},
     2244  series = {Lecture Notes in Computer Science},
     2245  pages = {39-51},
     2246  note = {10.1007/978-3},
     2247  affiliation = {Portland State University Dept. of Computer Science Portland OR 97207},
     2248  file = {:/users/outil/verif/biblio/Composition/Compponent-Based AbstractionRefinement2008.pdf:PDF},
     2249  isbn = {978-3-540-68062-8},
     2250  keyword = {Computer Science},
     2251  keywords = {Composition, Abstraction, Refinement, verified component, Hardware/software
     2252        coverification},
     2253  url = {http://dx.doi.org/10.1007/978-3-540-68073-4_4}
     2254}
     2255
    22042256@INPROCEEDINGS{lin91implicit,
    22052257  author = {B.~Lin and A.R.~Newton},
     
    22262278  address = {Hingham, MA, USA},
    22272279  publisher = {Kluwer Academic Publisher}
     2280}
     2281
     2282@INCOLLECTION{springerlink:10.1007/978-3-642-16901-4_15,
     2283  author = {Lomuscio, Alessio and Strulo, Ben and Walker, Nigel and Wu, Peng},
     2284  title = {Assume-Guarantee Reasoning with Local Specifications},
     2285  booktitle = {Formal Methods and Software Engineering},
     2286  publisher = {Springer Berlin / Heidelberg},
     2287  year = {2010},
     2288  editor = {Dong, Jin and Zhu, Huibiao},
     2289  volume = {6447},
     2290  series = {Lecture Notes in Computer Science},
     2291  pages = {204-219},
     2292  note = {10.1007/978-3-642-16901-4_15},
     2293  abstract = {We investigate assume-guarantee reasoning for global specifications
     2294        consisting of conjunctions of local specifications. We present a
     2295        sound and complete assume-guarantee rule that permits reasoning about
     2296        individual modules for local specifications and draws conclusions
     2297        on global specifications. We illustrate our approach with an example
     2298        from the field of network congestion control, where different agents
     2299        are responsible for controlling packet flow across a shared infrastructure.
     2300        In this context, we derive an assume-guarantee rule for system stability,
     2301        and show that this rule is valuable to reason about any number of
     2302        agents, any initial flow configuration, and any topology of bounded
     2303        degree.},
     2304  affiliation = {Department of Computing, Imperial College London, UK},
     2305  file = {:/users/outil/verif/biblio/Composition/AGRwithLocalSpecification2010.pdf:PDF},
     2306  isbn = {978-3-642-16900-7},
     2307  keyword = {Computer Science},
     2308  keywords = {Compositional reasoning, composition},
     2309  owner = {cecile},
     2310  timestamp = {2012.03.07},
     2311  url = {http://dx.doi.org/10.1007/978-3-642-16901-4_15}
    22282312}
    22292313
     
    24482532  pages = {2-14},
    24492533  number = {1},
    2450   bibsource = {DBLP, http://dblp.uni-trier.de}
     2534  bibsource = {DBLP, http://dblp.uni-trier.de},
     2535  keywords = {Abstraction}
    24512536}
    24522537
     
    25592644  publisher = {Springer-Verlag},
    25602645  url = {http://www.csl.sri.com/papers/cade92-pvs/}
     2646}
     2647
     2648@INCOLLECTION{springerlink:10.1007/3-540-63166-6_5,
     2649  author = {Pardo, Abelardo and Hachtel, Gary},
     2650  title = {Automatic abstraction techniques for propositional $\mu$-calculus
     2651        model checking},
     2652  booktitle = {Computer Aided Verification},
     2653  publisher = {Springer Berlin / Heidelberg},
     2654  year = {1997},
     2655  editor = {Grumberg, Orna},
     2656  volume = {1254},
     2657  series = {Lecture Notes in Computer Science},
     2658  pages = {12-23},
     2659  note = {10.1007/3-540-63166-6_5},
     2660  abstract = {An abstraction/refinement paradigm for the full propositional $\mu$-calculus
     2661        is presented. No distinction is made between universal or existential
     2662        fragments. Necessary conditions for conservative verification are
     2663        provided, along with a fully automatic symbolic model checking abstraction
     2664        algorithm. The algorithm begins with conservative verification of
     2665        an initial abstraction. If the conclusion is negative, it derives
     2666        a ldquogoal setrdquo of states which require further resolution.
     2667        It then successively refines, with respect to this goal set, the
     2668        approximations made in the subformulas, until the given formula is
     2669        verified or computational resources are exhausted.},
     2670  affiliation = {University of Colorado ECEN Campus Box 425 80309 Boulder CO USA ECEN
     2671        Campus Box 425 80309 Boulder CO USA},
     2672  file = {:/users/outil/verif/biblio/Cegar/CAV97_Automatic_Abstraction_Tech_for_Propositional_uCalc_MC.ps:PostScript},
     2673  isbn = {978-3-540-63166-8},
     2674  keywords = {Computer Science, Abstraction, model checking, mu-calculus, refinement},
     2675  owner = {cecile},
     2676  timestamp = {2012.03.07},
     2677  url = {http://dx.doi.org/10.1007/3-540-63166-6_5}
     2678}
     2679
     2680@INPROCEEDINGS{Pardo:1998:ICM:277044.277171,
     2681  author = {Pardo, Abelardo and Hachtel, Gary D.},
     2682  title = {Incremental CTL model checking using BDD subsetting},
     2683  booktitle = {Proceedings of the 35th annual Design Automation Conference},
     2684  year = {1998},
     2685  series = {DAC '98},
     2686  pages = {457--462},
     2687  address = {New York, NY, USA},
     2688  publisher = {ACM},
     2689  abstract = {An automatic abstraction/refinement algorithm for symbolic CTL model
     2690        checking is presented. Conservative model checking is thus done for
     2691        the full CTL language-no restriction is made to the universal or
     2692        existen tial fragments. The algorithm begins with conserv ativ everification
     2693        of an initial abstraction. If the conclusion is negativ e,it deriv
     2694        es a ¿goal set¿ of states which require further resolution. It then
     2695        successiv ely refines, with respect to this goal set, the appro ximations
     2696        made in the sub-formulas, until the giv en form ula is v erified
     2697        or computational resources are exhausted. This method applies uniformly
     2698        to the abstractions based in over-appro ximation as well as under-approximations
     2699        of the model. Both the refinement and the abstraction procedures
     2700        are based in BDD-subsetting. Note that refinement procedures which
     2701        are based on error traces, are limited to over-appro ximation on
     2702        the universal fragment (or for language con tainment), whereas the
     2703        goal set method is applicable to all consisten t appro ximations,
     2704        and for all CTL formulas.},
     2705  acmid = {277171},
     2706  doi = {10.1145/277044.277171},
     2707  file = {:/users/outil/verif/biblio/Cegar/DAC98_Incremental CTL Model Checking Using BDD Subsetting.pdf:PDF},
     2708  isbn = {0-89791-964-5},
     2709  keywords = {CTL, model checking, Abstraction},
     2710  location = {San Francisco, California, United States},
     2711  numpages = {6},
     2712  url = {http://doi.acm.org/10.1145/277044.277171}
    25612713}
    25622714
     
    28743026  publisher = {IEEE Computer Society},
    28753027  doi = {http://dx.doi.org/10.1109/LICS.2006.5},
     3028  keywords = {Abstraction, 3-valued},
    28763029  owner = {cecile},
    28773030  timestamp = {2007.01.14}
     
    29353088  owner = {cecile},
    29363089  timestamp = {2006.02.09}
     3090}
     3091
     3092@INPROCEEDINGS{Tripakis201,
     3093  author = {Tripakis, Stavros and Andrade, Hugo and Ghosal, Arkadeb and Limaye,
     3094        Rhishikesh and Ravindran, Kaushik and Wang, Guoqiang and Yang, Guang
     3095        and Kormerup, Jacob and Wong, Ian},
     3096  title = {Correct and non-defensive glue design using abstract models},
     3097  booktitle = {Proceedings of the seventh IEEE/ACM/IFIP international conference
     3098        on Hardware/software codesign and system synthesis},
     3099  year = {2011},
     3100  series = {CODES+ISSS '11},
     3101  pages = {59--68},
     3102  address = {New York, NY, USA},
     3103  publisher = {ACM},
     3104  abstract = { Current hardware design practice often relies on integration of components,
     3105        some of which may be IP or legacy blocks. While integration eases
     3106        design by allowing modularization and component reuse, it is still
     3107        done in a mostly ad hoc manner. Designers work with descriptions
     3108        of components that are either informal or incomplete (e.g., documents
     3109        in English, structural but non-behavioral specifications in IP-XACT)
     3110        or too low-level (e.g., HDL code), and have little to no automatic
     3111        support for stitching the components together. Providing such support
     3112        is the glue design problem.
     3113       
     3114        This paper addresses this problem using a model-based approach. The
     3115        key idea is to use high-level models, such as dataflow graphs, that
     3116        enable efficient automated analysis. The analysis can be used to
     3117        derive performance properties of the system (e.g., component compatibility,
     3118        throughput, etc.), optimize resource usage (e.g., buffer sizes),
     3119        and even synthesize low-level code (e.g., control logic). However,
     3120        these models are only abstractions of the real system, and often
     3121        omit critical information. As a result, the analysis outcomes may
     3122        be defensive (e.g., buffers that are too big) or even incorrect (e.g.,
     3123        buffers that are too small). The paper examines these situations
     3124        and proposes a correct and non-defensive design methodology that
     3125        employs the right models to explore accurate performance and resource
     3126        trade-offs. },
     3127  acmid = {2039382},
     3128  doi = {http://doi.acm.org/10.1145/2039370.2039382},
     3129  isbn = {978-1-4503-0715-4},
     3130  keywords = {abstraction, data flow, glue design, non-defensiveness, composition},
     3131  location = {Taipei, Taiwan},
     3132  numpages = {10},
     3133  owner = {cecile},
     3134  timestamp = {2012.03.07},
     3135  url = {http://doi.acm.org/10.1145/2039370.2039382}
    29373136}
    29383137
     
    30293228}
    30303229
     3230@ARTICLE{5374376,
     3231  author = {Hao Zheng and Haiqiong Yao and Yoneda, T.},
     3232  title = {Modular Model Checking of Large Asynchronous Designs with Efficient
     3233        Abstraction Refinement},
     3234  journal = {Computers, IEEE Transactions on},
     3235  year = {2010},
     3236  volume = {59},
     3237  pages = {561 -573},
     3238  number = {4},
     3239  month = {april },
     3240  abstract = {Divide-and-conquer is essential to address state explosion in model
     3241        checking. Verifying each individual component in a system, in isolation,
     3242        efficiently requires an appropriate context, which traditionally
     3243        is obtained by hand. This paper presents an efficient modular model
     3244        checking approach for asynchronous design verification. It is equipped
     3245        with a novel abstraction refinement method that can refine a component
     3246        abstraction to be accurate enough for successful verification. It
     3247        is fully automated, and eliminates the need of finding an accurate
     3248        context when verifying each individual component, although such a
     3249        context is still highly desirable. This method is also enhanced with
     3250        additional state space reduction techniques. The experiments on several
     3251        nontrivial asynchronous designs show that this method efficiently
     3252        removes impossible behaviors from each component including ones violating
     3253        correctness requirements.},
     3254  doi = {10.1109/TC.2009.187},
     3255  file = {:/users/outil/verif/biblio/Composition/ModularMCLargeAsynchronousDesignwithAR2010.pdf:PDF},
     3256  issn = {0018-9340},
     3257  keywords = {abstraction refinement;abstraction refinement method;large asynchronous
     3258        designs;modular model checking;state explosion;state space reduction
     3259        techniques;formal verification;state-space methods; composition},
     3260  owner = {cecile},
     3261  review = {Verification of a whole system by verifying each components. When
     3262        verifying each components individually assumptions has to be made
     3263        on the environnment ot avoid false counter-examples. Use component
     3264        abstraction to over-approximated the environment. This abastraction
     3265        must be refined to obtain only the behavior allowed at the interface.
     3266        They propose :
     3267       
     3268        <ul>
     3269       
     3270        <li>     to identify and remove unsynchronized behavior.
     3271       
     3272         <li> to extend the refinement to more than two components itemize
     3273       
     3274       
     3275        </ul>
     3276       
     3277       
     3278        Main contribution : Local synchronization detection method for component
     3279        based on parallel composition and an AR methof for modular MC.
     3280       
     3281        <br>
     3282       
     3283        Circuit class : Asynchronous</td>},
     3284  timestamp = {2012.03.07}
     3285}
     3286
    30313287@PROCEEDINGS{DBLP:conf/fmcad/2002,
    30323288  title = {Formal Methods in Computer-Aided Design, 4th International Conference,
  • biblio/compositional.bib

    r46 r51  
    144144  doi = {http://doi.acm.org/10.1145/2039370.2039382},
    145145  isbn = {978-1-4503-0715-4},
    146   keywords = {abstraction, data flow, glue design, non-defensiveness},
     146  keywords = {abstraction, data flow, glue design, non-defensiveness, composition},
    147147  location = {Taipei, Taiwan},
    148148  numpages = {10},
     
    179179  keywords = {abstraction refinement;abstraction refinement method;large asynchronous
    180180        designs;modular model checking;state explosion;state space reduction
    181         techniques;formal verification;state-space methods;}
     181        techniques;formal verification;state-space methods; composition},
     182  review = {Verification of a whole system by verifying each components. When
     183        verifying each components individually assumptions has to be made
     184        on the environnment ot avoid false counter-examples. Use component
     185        abstraction to over-approximated the environment. This abastraction
     186        must be refined to obtain only the behavior allowed at the interface.
     187        They propose : \begin{itemize} \item to identify and remove unsynchronized
     188        behavior. \item to extend the refinement to more than two components
     189        \end{itemize} Main contribution : Local synchronization detection
     190        method for component based on parallel composition and an AR methof
     191        for modular MC. Circuit class : Asynchronous}
    182192}
    183193
  • 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.