Changes between Initial Version and Version 1 of CompositionalBiblio


Ignore:
Timestamp:
Feb 28, 2012, 6:18:29 PM (12 years ago)
Author:
cecile
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • CompositionalBiblio

    v1 v1  
     1
     2{{{
     3#!html
     4
     5<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd">
     6<html lang="en">
     7<head>
     8<title>JabRef References output</title>
     9<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
     10<script type="text/javascript">
     11<!--
     12// QuickSearch script for JabRef HTML export
     13// Version: 2.0
     14//
     15// Copyright (c) 2006-2008, Mark Schenk
     16//
     17// This software is distributed under a Creative Commons Attribution 3.0 License
     18// http://creativecommons.org/licenses/by/3.0/
     19
     20// Some features:
     21// + optionally searches Abstracts and Reviews
     22// + allows RegExp searches
     23//   e.g. to search for entries between 1980 and 1989, type:  198[0-9]
     24//   e.g. for any entry ending with 'symmetry', type:  symmetry$
     25//   e.g. for all reftypes that are books: ^book$, or ^article$
     26//   e.g. for entries by either John or Doe, type john|doe
     27// + easy toggling of Abstract/Review/BibTeX
     28
     29// Search settings
     30var searchAbstract = true;
     31var searchReview = true;
     32
     33// Speed optimisation introduced some esoteric problems with certain RegExp searches
     34// e.g. if the previous search is 200[-7] and the next search is 200[4-7] then the search doesn't work properly until the next 'keyup'
     35// hence the searchOpt can be turned off for RegExp adepts
     36var searchOpt = true;
     37
     38if (window.addEventListener) {
     39        window.addEventListener("load",initSearch,false); }
     40else if (window.attachEvent) {
     41        window.attachEvent("onload", initSearch); }
     42
     43function initSearch() {
     44        // basic object detection
     45        if(!document.getElementById || !document.getElementsByTagName) { return; }
     46        if (!document.getElementById('qstable')||!document.getElementById('qs')) { return; }
     47
     48        // find QS table and appropriate rows
     49        searchTable = document.getElementById('qstable');
     50        var allRows = searchTable.getElementsByTagName('tbody')[0].getElementsByTagName('tr');
     51
     52        // split all rows into entryRows and infoRows (e.g. abstract, review, bibtex)
     53        entryRows = new Array();
     54        infoRows = new Array(); absRows = new Array(); revRows = new Array();
     55
     56        for (var i=0, k=0, j=0; i<allRows.length;i++) {
     57                if (allRows[i].className.match(/entry/)) {
     58                        entryRows[j++] = allRows[i];
     59                } else {
     60                        infoRows[k++] = allRows[i];
     61                        // check for abstract/review
     62                        if (allRows[i].className.match(/abstract/)) {
     63                                absRows.push(allRows[i]);
     64                        } else if (allRows[i].className.match(/review/)) {
     65                                revRows.push(allRows[i]);
     66                        }
     67                }
     68        }
     69
     70        //number of entries and rows
     71        numRows = allRows.length;
     72        numEntries = entryRows.length;
     73        numInfo = infoRows.length;
     74        numAbs = absRows.length;
     75        numRev = revRows.length;
     76
     77        //find the query field
     78        qsfield = document.getElementById('qsfield');
     79
     80        // previous search term; used for speed optimisation
     81        prevSearch = '';
     82
     83        //find statistics location
     84        stats = document.getElementById('stat');
     85        setStatistics(-1);
     86
     87        // creates the appropriate search settings
     88        createQSettingsDialog();
     89
     90        // shows the searchfield
     91        document.getElementById('qs').style.display = 'block';
     92        document.getElementById('qsfield').onkeyup = testEvent;
     93}
     94
     95function quickSearch(tInput){
     96
     97         if (tInput.value.length == 0) {
     98                showAll();
     99                setStatistics(-1);
     100                qsfield.className = '';
     101                return;
     102        } else {
     103                // only search for valid RegExp
     104                try {
     105                        var searchText = new RegExp(tInput.value,"i")
     106                        closeAllInfo();
     107                        qsfield.className = '';
     108                }
     109                catch(err) {
     110                        prevSearch = tInput.value;
     111                        qsfield.className = 'invalidsearch';
     112                        return;
     113                }
     114        }
     115       
     116        // count number of hits
     117        var hits = 0;
     118
     119        // start looping through all entry rows
     120        for (var i = 0; cRow = entryRows[i]; i++){
     121
     122                // only show search the cells if it isn't already hidden OR if the search term is getting shorter, then search all
     123                // some further optimisation is possible: if the search string is getting shorter, and the row is already visible, skip it. Then be careful with hits!
     124                if(!searchOpt || cRow.className.indexOf('noshow')==-1 || tInput.value.length <= prevSearch.length){
     125                        var found = false;
     126
     127                        var inCells = cRow.getElementsByTagName('td');
     128                        var numCols = inCells.length;
     129                               
     130                        for (var j=0; j<numCols; j++) {
     131                                cCell = inCells[j];
     132                                var t = cCell.innerText?cCell.innerText:getTextContent(cCell);
     133                                if (t.search(searchText) != -1){
     134                                        found=true;
     135                                        break;
     136                                }
     137                        }
     138
     139                        // look for further hits in Abstract and Review
     140                        if(!found) {
     141                                var articleid = cRow.id;
     142                                if(searchAbstract && (abs = document.getElementById('abs_'+articleid))) {
     143                                        if (getTextContent(abs).search(searchText) != -1){ found=true; }
     144                                }
     145                                if(searchReview && (rev = document.getElementById('rev_'+articleid))) {
     146                                        if (getTextContent(rev).search(searchText) != -1){ found=true; }
     147                                }
     148                        }
     149                       
     150                        if(found) {
     151                                cRow.className = 'entry show';
     152                                hits++;
     153                        } else {
     154                                cRow.className = 'entry noshow';
     155                        }
     156                }
     157        }
     158
     159        // update statistics
     160        setStatistics(hits)
     161       
     162        // set previous search value
     163        prevSearch = tInput.value;
     164}
     165
     166function toggleInfo(articleid,info) {
     167
     168        var entry = document.getElementById(articleid);
     169        var abs = document.getElementById('abs_'+articleid);
     170        var rev = document.getElementById('rev_'+articleid);
     171        var bib = document.getElementById('bib_'+articleid);
     172                // Get the abstracts/reviews/bibtext in the right location
     173        // in unsorted tables this is always the case, but in sorted tables it is necessary.
     174        // Start moving in reverse order, so we get: entry, abstract,review,bibtex
     175        if (searchTable.className.indexOf('sortable') != -1) {
     176                if(bib) { entry.parentNode.insertBefore(bib,entry.nextSibling); }
     177                if(rev) { entry.parentNode.insertBefore(rev,entry.nextSibling); }
     178                if(abs) { entry.parentNode.insertBefore(abs,entry.nextSibling); }
     179        }
     180
     181        if (abs && info == 'abstract') {
     182                if(abs.className.indexOf('abstract') != -1) {
     183                abs.className.indexOf('noshow') == -1?abs.className = 'abstract noshow':abs.className = 'abstract';
     184                }
     185        } else if (rev && info == 'review') {
     186                if(rev.className.indexOf('review') != -1) {
     187                rev.className.indexOf('noshow') == -1?rev.className = 'review noshow':rev.className = 'review';
     188                }
     189        } else if (bib && info == 'bibtex') {
     190                if(bib.className.indexOf('bibtex') != -1) {
     191                bib.className.indexOf('noshow') == -1?bib.className = 'bibtex noshow':bib.className = 'bibtex';
     192                }               
     193        } else {
     194                return;
     195        }
     196
     197        // check if one or the other is available
     198        var revshow = false;
     199        var absshow = false;
     200        var bibshow = false;
     201        (abs && abs.className.indexOf('noshow') == -1)? absshow = true: absshow = false;
     202        (rev && rev.className.indexOf('noshow') == -1)? revshow = true: revshow = false;       
     203        (bib && bib.className == 'bibtex')? bibshow = true: bibshow = false;
     204       
     205        // highlight original entry
     206        if(entry) {
     207                if (revshow || absshow || bibshow) {
     208                entry.className = 'entry highlight show';
     209                } else {
     210                entry.className = 'entry show';
     211                }               
     212        }
     213       
     214        // When there's a combination of abstract/review/bibtex showing, need to add class for correct styling
     215        if(absshow) {
     216                (revshow||bibshow)?abs.className = 'abstract nextshow':abs.className = 'abstract';
     217        }
     218        if (revshow) {
     219                bibshow?rev.className = 'review nextshow': rev.className = 'review';
     220        }
     221       
     222}
     223
     224function setStatistics (hits) {
     225        if(hits < 0) { hits=numEntries; }
     226        if(stats) { stats.firstChild.data = hits + '/' + numEntries}
     227}
     228
     229function getTextContent(node) {
     230        // Function written by Arve Bersvendsen
     231        // http://www.virtuelvis.com
     232       
     233        if (node.nodeType == 3) {
     234        return node.nodeValue;
     235        } // text node
     236        if (node.nodeType == 1) { // element node
     237        var text = [];
     238        for (var chld = node.firstChild;chld;chld=chld.nextSibling) {
     239                text.push(getTextContent(chld));
     240        }
     241        return text.join("");
     242        } return ""; // some other node, won't contain text nodes.
     243}
     244
     245function showAll(){
     246        // first close all abstracts, reviews, etc.
     247        closeAllInfo();
     248
     249        for (var i = 0; i < numEntries; i++){
     250                entryRows[i].className = 'entry show';
     251        }
     252}
     253
     254function closeAllInfo(){
     255        for (var i=0; i < numInfo; i++){
     256                if (infoRows[i].className.indexOf('noshow') ==-1) {
     257                        infoRows[i].className = infoRows[i].className + ' noshow';
     258                }
     259        }
     260}
     261
     262function testEvent(e){
     263        if (!e) var e = window.event;
     264        quickSearch(this);
     265}
     266
     267function clearQS() {
     268        qsfield.value = '';
     269        quickSearch(qsfield);
     270}
     271
     272function redoQS(){
     273        showAll();
     274        quickSearch(qsfield);
     275}
     276
     277// Create Search Settings
     278
     279function toggleQSettingsDialog() {
     280
     281        var qssettings = document.getElementById('qssettings');
     282       
     283        if(qssettings.className.indexOf('active')==-1) {
     284                qssettings.className = 'active';
     285
     286                if(absCheckBox && searchAbstract == true) { absCheckBox.checked = 'checked'; }
     287                if(revCheckBox && searchReview == true) { revCheckBox.checked = 'checked'; }
     288
     289        } else {
     290                qssettings.className= '';
     291        }
     292}
     293
     294function createQSettingsDialog(){
     295        var qssettingslist = document.getElementById('qssettings').getElementsByTagName('ul')[0];
     296       
     297        if(numAbs!=0) {
     298                var x = document.createElement('input');
     299                x.id = "searchAbs";
     300                x.type = "checkbox";
     301                x.onclick = toggleQSetting;
     302                var y = qssettingslist.appendChild(document.createElement('li')).appendChild(document.createElement('label'));
     303                y.appendChild(x);
     304                y.appendChild(document.createTextNode('search abstracts'));             
     305        }
     306        if(numRev!=0) {
     307                var x = document.createElement('input');
     308                x.id = "searchRev";
     309                x.type = "checkbox";           
     310                x.onclick = toggleQSetting;
     311                var y = qssettingslist.appendChild(document.createElement('li')).appendChild(document.createElement('label'));         
     312                y.appendChild(x);               
     313                y.appendChild(document.createTextNode('search reviews'));
     314        }
     315               
     316        // global variables
     317        absCheckBox = document.getElementById('searchAbs');
     318        revCheckBox = document.getElementById('searchRev');
     319       
     320        // show search settings
     321        if(absCheckBox||revCheckBox) {
     322                document.getElementById('qssettings').style.display = 'block';
     323        }
     324}
     325
     326function toggleQSetting() {
     327        if(this.id=='searchAbs') { searchAbstract = !searchAbstract; }
     328        if(this.id=='searchRev') { searchReview = !searchReview; }
     329        redoQS()
     330}
     331-->
     332</script>
     333<script type="text/javascript">
     334<!--
     335// Sort Table Script
     336// Version: 1.1
     337//
     338// Copyright (c) 2006-2008, Mark Schenk
     339//
     340// This software is distributed under a Creative Commons Attribution 3.0 License
     341// http://creativecommons.org/licenses/by/3.0/
     342
     343// NB: slow as molasses in FireFox, especially when sorting columns with a lot of text.
     344// An optimization is implemented which makes speed bearable, toggled by the following variable
     345var SORT_SPEED_OPT = true;
     346// a bit of browser preference: Opera does not need optimization
     347if(window.opera) { SORT_SPEED_OPT=false; }
     348// the optimization has one limitation on the functionality: when sorting search
     349// results, the expanded info, e.g. bibtex/review, is collapsed. In the non-optimized
     350// version they remain visible.
     351
     352
     353if (window.addEventListener) {
     354        window.addEventListener("load",initSortTable,false) }
     355else if (window.attachEvent) {
     356        window.attachEvent("onload", initSortTable); }
     357
     358function initSortTable() {
     359var alltables = document.getElementsByTagName('table');
     360for(i=0;i<alltables.length;i++) {
     361        var currentTable = alltables[i];
     362        if(currentTable.className.indexOf('sortable') !=-1) {
     363                var thead = currentTable.getElementsByTagName('thead')[0];
     364                thead.title = 'Click on any column header to sort';
     365                for (var i=0;cell = thead.getElementsByTagName('th')[i];i++) {
     366                        cell.onclick = function () { resortTable(this); };
     367                        // make it possible to have a default sort column
     368                        if(cell.className.indexOf('sort')!=-1) {
     369                                resortTable(cell)
     370                        }
     371                }
     372        }
     373}
     374}
     375
     376var SORT_COLUMN_INDEX
     377
     378function resortTable(td) {
     379        var column = td.cellIndex;
     380        var table = getParent(td,'TABLE');
     381
     382        var allRows = table.getElementsByTagName('tbody')[0].getElementsByTagName('tr');
     383        var newRows = new Array();
     384
     385        for (var i=0, k=0; i<allRows.length;i++) {
     386
     387                var rowclass = allRows[i].className;
     388
     389                if (rowclass.indexOf('entry') != -1) {
     390                newRows[k++] = allRows[i];
     391                }
     392               
     393                if (SORT_SPEED_OPT) {
     394                // remove highlight class
     395                allRows[i].className = rowclass.replace(/highlight/,'');
     396                // close information
     397                if(rowclass.indexOf('entry') == -1 && rowclass.indexOf('noshow') == -1) { allRows[i].className = rowclass + ' noshow';}
     398                }
     399        }
     400
     401
     402        // If other sort functions are deemed necessary (e.g. for
     403        // dates and currencies) they can be added.
     404        var sortfn = ts_sort_firstchild_caseinsensitive;
     405        SORT_COLUMN_INDEX = column;
     406        newRows.sort(sortfn);
     407
     408        // create a container for showing sort arrow
     409        var arrow =  td.getElementsByTagName('span')[0];
     410        if (!arrow) { var arrow = td.appendChild(document.createElement('span'));}
     411       
     412        if (td.className) {
     413                if (td.className.indexOf('sort_asc') !=-1) {
     414                        td.className = td.className.replace(/_asc/,"_des");
     415                        newRows.reverse();
     416                        arrow.innerHTML = '&uArr;';
     417                } else if (td.className.indexOf('sort_des') !=-1) {
     418                        td.className = td.className.replace(/_des/,"_asc");
     419                        arrow.innerHTML = '&dArr;';
     420                } else {
     421                        td.className += ' sort_asc';
     422                        arrow.innerHTML = '&dArr;';
     423                }
     424        } else {
     425                td.className += 'sort_asc';
     426                arrow.innerHTML = '&dArr;';
     427        }
     428       
     429        // Remove the classnames and up/down arrows for the other headers
     430        var ths = table.getElementsByTagName('thead')[0].getElementsByTagName('th');
     431        for (var i=0; i<ths.length; i++) {
     432                if(ths[i]!=td && ths[i].className.indexOf('sort_')!=-1) {
     433                // argh, moronic JabRef thinks (backslash)w is an output field!!
     434                //ths[i].className = ths[i].className.replace(/sort_(backslash)w{3}/,"");
     435                ths[i].className = ths[i].className.replace(/sort_asc/,"");
     436                ths[i].className = ths[i].className.replace(/sort_des/,"");
     437
     438                // remove span
     439                var arrow =  ths[i].getElementsByTagName('span')[0];
     440                if (arrow) { ths[i].removeChild(arrow); }
     441                }
     442        }
     443
     444        // We appendChild rows that already exist to the tbody, so it moves them rather than creating new ones
     445        for (i=0;i<newRows.length;i++) {
     446                table.getElementsByTagName('tbody')[0].appendChild(newRows[i]);
     447
     448                if(!SORT_SPEED_OPT){
     449                // moving additional information, e.g. bibtex/abstract to right locations
     450                // this allows to sort, even with abstract/review/etc. still open
     451                var articleid = newRows[i].id;
     452
     453                var entry = document.getElementById(articleid);
     454                var abs = document.getElementById('abs_'+articleid);
     455                var rev = document.getElementById('rev_'+articleid);
     456                var bib = document.getElementById('bib_'+articleid);           
     457       
     458                var tbody = table.getElementsByTagName('tbody')[0];
     459                // mind the order of adding the entries
     460                if(abs) { tbody.appendChild(abs); }
     461                if(rev) { tbody.appendChild(rev); }
     462                if(bib) { tbody.appendChild(bib); }
     463                }
     464        }
     465}
     466
     467function ts_sort_firstchild_caseinsensitive(a,b) {
     468        // only search in .firstChild of the cells. Speeds things up tremendously in FF
     469        // problem is that it won't find all the text in a cell if the firstChild is an element
     470        // or if there are other elements in the cell. Risky fix, but the speed boost is worth it.
     471        var acell = a.cells[SORT_COLUMN_INDEX];
     472        var bcell = b.cells[SORT_COLUMN_INDEX];
     473       
     474        acell.firstChild? aa = getTextContent(acell.firstChild).toLowerCase():aa = "";
     475        bcell.firstChild? bb = getTextContent(bcell.firstChild).toLowerCase():bb = "";
     476
     477        if (aa==bb) return 0;
     478        if (aa<bb) return -1;
     479        return 1;
     480}
     481
     482function ts_sort_caseinsensitive(a,b) {
     483        aa = getTextContent(a.cells[SORT_COLUMN_INDEX]).toLowerCase();
     484        bb = getTextContent(b.cells[SORT_COLUMN_INDEX]).toLowerCase();
     485        if (aa==bb) return 0;
     486        if (aa<bb) return -1;
     487        return 1;
     488}
     489
     490function ts_sort_default(a,b) {
     491        aa = getTextContent(a.cells[SORT_COLUMN_INDEX]);
     492        bb = getTextContent(b.cells[SORT_COLUMN_INDEX]);
     493        if (aa==bb) return 0;
     494        if (aa<bb) return -1;
     495        return 1;
     496}
     497
     498function getParent(el, pTagName) {
     499        if (el == null) {
     500                return null;
     501        } else if (el.nodeType == 1 && el.tagName.toLowerCase() == pTagName.toLowerCase()) {
     502                return el;
     503        } else {
     504                return getParent(el.parentNode, pTagName);
     505        }
     506}
     507-->
     508</script>
     509
     510<style type="text/css">
     511body { background-color: white; font-family: "Trebuchet MS", Arial, sans-serif; font-size: 12px; line-height: 1.2; padding: 1em; color: #2E2E2E; }
     512
     513#qs { width: auto; border-style: solid; border-color: gray; border-width: 1px 1px 0px 1px; padding: 0.5em 0.5em; display:none; position:relative; }
     514#qs form { padding: 0px; margin: 0px; }
     515#qs form p { padding: 0px; margin: 0px; }
     516
     517.invalidsearch { background-color: red; }
     518
     519table { border: 1px gray solid; width: 100%; empty-cells: show; }
     520th, td { border: 1px gray solid; padding: 0.5em; vertical-align: top;  }
     521td { text-align: left; vertical-align: top; }
     522th { background-color: #EFEFEF; }
     523
     524td a { color: navy; text-decoration: none; }
     525td a:hover  { text-decoration: underline; }
     526
     527tr.noshow { display: none;}
     528
     529tr.highlight td { background-color: #F1F1F1; border-top: 2px black solid; font-weight: bold; }
     530tr.abstract td, tr.review td, tr.bibtex td { background-color: #F1F1F1; border-bottom: 2px black solid; }
     531tr.nextshow td { border-bottom: 1px gray solid; }
     532
     533tr.bibtex pre { width: 100%; overflow: auto;}
     534
     535p.infolinks { margin: 0.5em 0em 0em 0em; padding: 0px; }
     536
     537#qssettings { padding: 0.5em; position: absolute; top: 0.2em; right: 0.2em; border: 1px gray solid; background-color: white; display: none; }
     538#qssettings p { font-weight: bold; cursor: pointer; }
     539#qssettings ul { display: none; list-style-type: none; padding-left: 0; margin: 0; }
     540#qssettings.active ul { display: block; }
     541
     542@media print {
     543        p.infolinks, #qssettings, #qs { display: none !important; }
     544        table { border-width: 0px; }
     545        tr { page-break-inside: avoid; }
     546        tr > * + * + * + * + * {display: none; }
     547        thead tr::before { content: "Reference"; border: 1px gray solid; padding: 0.5em; vertical-align: top; font-weight: bold; text-align: center; display: table-cell; background-color: #EFEFEF; }
     548        tr[id]::before { content: attr(id); display: table-cell; border: 1px gray solid; padding: 0.5em; vertical-align: top; font-style: italic; }
     549}
     550th.sort_asc, th.sort_des { border: 2px black solid; }
     551
     552</style>
     553</head>
     554<body>
     555
     556<div id="qs">
     557        <form action="">
     558        <p>QuickSearch: <input type="text" name="qsfield" id="qsfield" autocomplete="off" title="Allows plain text as well as RegExp searches" /><input type="button" onclick="clearQS()" value="clear" />&nbsp; Number of matching entries: <span id="stat">0</span>.</p>
     559        <div id="qssettings">
     560                <p onclick="toggleQSettingsDialog()">Search Settings</p>
     561                <ul></ul>
     562        </div>
     563        </form>
     564</div>
     565<table id="qstable" class="sortable" border="1">
     566<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>
     567<tbody>
     568<tr id="Cabodi09Speeding" class="entry">
     569        <td>Cabodi, G., Camurati, P., Garcia, L., Murciano, M., Nocco, S. &amp; Quer, S.&nbsp;</td>
     570        <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>
     571        <td>2009</td>
     572        <td>DATE '09: Proceedings of the conference on Design, Automation and Test in Europe, pp. 1686-1691&nbsp;</td>
     573        <td>inproceedings</td>
     574        <td>&nbsp;</td>
     575</tr>
     576<tr id="abs_Cabodi09Speeding" class="abstract noshow">
     577        <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>
     578</tr>
     579<tr id="bib_Cabodi09Speeding" class="bibtex noshow">
     580<td colspan="7"><b>BibTeX</b>:
     581<pre>
     582@inproceedings{Cabodi09Speeding,
     583  author = {G. Cabodi and P. Camurati and L. Garcia and M. Murciano and S. Nocco and S. Quer},
     584  title = {Speeding up Model Checking by Exploiting Explicit and Hidden Verification Constraints},
     585  booktitle = {DATE '09: Proceedings of the conference on Design, Automation and Test in Europe},
     586  year = {2009},
     587  pages = {1686-1691}
     588}
     589</pre></td>
     590</tr>
     591<tr id="springerlink:10.1007/978-3-642-16901-4_15" class="entry">
     592        <td>Lomuscio, A., Strulo, B., Walker, N. &amp; Wu, P.&nbsp;Jin Dong and Huibiao Zhu (Ed.)</td>
     593        <td>Assume-Guarantee Reasoning with Local Specifications <p class="infolinks">[<a href="javascript:toggleInfo('springerlink:10.1007/978-3-642-16901-4_15','abstract')">Abstract</a>] [<a href="javascript:toggleInfo('springerlink:10.1007/978-3-642-16901-4_15','bibtex')">BibTeX</a>]</p></td>
     594        <td>2010</td>
     595        <td><br/>Vol. 6447Formal Methods and Software Engineering, pp. 204-219&nbsp;</td>
     596        <td>incollection</td>
     597        <td><a href="http://dx.doi.org/10.1007/978-3-642-16901-4_15">URL</a>&nbsp;</td>
     598</tr>
     599<tr id="abs_springerlink:10.1007/978-3-642-16901-4_15" class="abstract noshow">
     600        <td colspan="7"><b>Abstract</b>: 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.</td>
     601</tr>
     602<tr id="bib_springerlink:10.1007/978-3-642-16901-4_15" class="bibtex noshow">
     603<td colspan="7"><b>BibTeX</b>:
     604<pre>
     605@incollection{springerlink:10.1007/978-3-642-16901-4_15,
     606  author = {Lomuscio, Alessio and Strulo, Ben and Walker, Nigel and Wu, Peng},
     607  title = {Assume-Guarantee Reasoning with Local Specifications},
     608  booktitle = {Formal Methods and Software Engineering},
     609  publisher = {Springer Berlin / Heidelberg},
     610  year = {2010},
     611  volume = {6447},
     612  pages = {204-219},
     613  note = {10.1007/978-3-642-16901-4_15},
     614  url = {http://dx.doi.org/10.1007/978-3-642-16901-4_15}
     615}
     616</pre></td>
     617</tr>
     618<tr id="Tripakis201" class="entry">
     619        <td>Tripakis, S., Andrade, H., Ghosal, A., Limaye, R., Ravindran, K., Wang, G., Yang, G., Kormerup, J. &amp; Wong, I.&nbsp;</td>
     620        <td>Correct and non-defensive glue design using abstract models <p class="infolinks">[<a href="javascript:toggleInfo('Tripakis201','abstract')">Abstract</a>] [<a href="javascript:toggleInfo('Tripakis201','bibtex')">BibTeX</a>]</p></td>
     621        <td>2011</td>
     622        <td>Proceedings of the seventh IEEE/ACM/IFIP international conference on Hardware/software codesign and system synthesis, pp. 59-68&nbsp;</td>
     623        <td>inproceedings</td>
     624        <td><a href="http://doi.acm.org/10.1145/2039370.2039382">DOI</a> <a href="http://doi.acm.org/10.1145/2039370.2039382">URL</a>&nbsp;</td>
     625</tr>
     626<tr id="abs_Tripakis201" class="abstract noshow">
     627        <td colspan="7"><b>Abstract</b>:  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.<p>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. </td>
     628</tr>
     629<tr id="bib_Tripakis201" class="bibtex noshow">
     630<td colspan="7"><b>BibTeX</b>:
     631<pre>
     632@inproceedings{Tripakis201,
     633  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},
     634  title = {Correct and non-defensive glue design using abstract models},
     635  booktitle = {Proceedings of the seventh IEEE/ACM/IFIP international conference on Hardware/software codesign and system synthesis},
     636  publisher = {ACM},
     637  year = {2011},
     638  pages = {59--68},
     639  url = {http://doi.acm.org/10.1145/2039370.2039382},
     640  doi = {http://doi.acm.org/10.1145/2039370.2039382}
     641}
     642</pre></td>
     643</tr>
     644</tbody>
     645</table>
     646
     647<p>
     648 <small>Created by <a href="http://jabref.sourceforge.net">JabRef</a> on 28/02/2012.</small>
     649</p>
     650
     651</body>
     652</html>
     653
     654<!-- File generated by JabRef ; Export Filter written by Mark Schenk -->
     655
     656}}}