Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm
Identifieur interne : 001D20 ( Istex/Corpus ); précédent : 001D19; suivant : 001D21Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm
Auteurs : Michaël Rusinowitch ; Sorin Stratulat ; Francis KlaySource :
- Journal of Automated Reasoning [ 0168-7433 ] ; 2003-02-01.
English descriptors
Abstract
Abstract: The Available Bit Rate protocol (ABR) for ATM networks is well adapted to data traffic by providing minimum rate guarantees and low cell loss to the ABR source end system. An ABR conformance algorithm for controlling the source rates through an interface has been defined by ATM Forum, and a more efficient version of it has been designed by Rabadan and Klay. We present in this work the first complete mechanical verification of the equivalence between these two algorithms. The proof is involved and has been supported by the PVS theorem prover. It has required many lemmas, case analysis, and induction reasoning for the manipulation of unbounded scheduling lists. Some ABR conformance protocols have been verified in previous works. However, these protocols are approximations of the one we consider here. In particular, the algorithms assume a bound on the number of rates to be scheduled.
Url:
DOI: 10.1023/A:1023251327012
Links to Exploration step
ISTEX:7D3A15E739ABB9074DA25DB14FF8816664BC9D76Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm</title><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name><affiliation><mods:affiliation>LORIA-INRIA, 54506, Vandœuvre-les-Nancy Cedex, France</mods:affiliation></affiliation></author><author><name sortKey="Stratulat, Sorin" sort="Stratulat, Sorin" uniqKey="Stratulat S" first="Sorin" last="Stratulat">Sorin Stratulat</name><affiliation><mods:affiliation>INRIA–Sophia Antipolis, 2004 Route des Lucioles, 06092, Sophia Antipolis, France</mods:affiliation></affiliation></author><author><name sortKey="Klay, Francis" sort="Klay, Francis" uniqKey="Klay F" first="Francis" last="Klay">Francis Klay</name><affiliation><mods:affiliation>Technopole Anticipa, France Telecom CNET DTL/MSV, 2 av. Pierre Marzin, 22307, Lannion, France</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:7D3A15E739ABB9074DA25DB14FF8816664BC9D76</idno><date when="2003" year="2003">2003</date><idno type="doi">10.1023/A:1023251327012</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-P5HVP0B2-1/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001D20</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001D20</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm</title><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name><affiliation><mods:affiliation>LORIA-INRIA, 54506, Vandœuvre-les-Nancy Cedex, France</mods:affiliation></affiliation></author><author><name sortKey="Stratulat, Sorin" sort="Stratulat, Sorin" uniqKey="Stratulat S" first="Sorin" last="Stratulat">Sorin Stratulat</name><affiliation><mods:affiliation>INRIA–Sophia Antipolis, 2004 Route des Lucioles, 06092, Sophia Antipolis, France</mods:affiliation></affiliation></author><author><name sortKey="Klay, Francis" sort="Klay, Francis" uniqKey="Klay F" first="Francis" last="Klay">Francis Klay</name><affiliation><mods:affiliation>Technopole Anticipa, France Telecom CNET DTL/MSV, 2 av. Pierre Marzin, 22307, Lannion, France</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="j">Journal of Automated Reasoning</title><title level="j" type="abbrev">Journal of Automated Reasoning</title><idno type="ISSN">0168-7433</idno><idno type="eISSN">1573-0670</idno><imprint><publisher>Kluwer Academic Publishers</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="2003-02-01">2003-02-01</date><biblScope unit="volume">30</biblScope><biblScope unit="issue">2</biblScope><biblScope unit="page" from="153">153</biblScope><biblScope unit="page" to="177">177</biblScope></imprint><idno type="ISSN">0168-7433</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0168-7433</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>ABR conformance algorithm</term><term>PVS theorem prover</term><term>mechanical verification</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: The Available Bit Rate protocol (ABR) for ATM networks is well adapted to data traffic by providing minimum rate guarantees and low cell loss to the ABR source end system. An ABR conformance algorithm for controlling the source rates through an interface has been defined by ATM Forum, and a more efficient version of it has been designed by Rabadan and Klay. We present in this work the first complete mechanical verification of the equivalence between these two algorithms. The proof is involved and has been supported by the PVS theorem prover. It has required many lemmas, case analysis, and induction reasoning for the manipulation of unbounded scheduling lists. Some ABR conformance protocols have been verified in previous works. However, these protocols are approximations of the one we consider here. In particular, the algorithms assume a bound on the number of rates to be scheduled.</div></front></TEI><istex><corpusName>springer-journals</corpusName><author><json:item><name>Michaël Rusinowitch</name><affiliations><json:string>LORIA-INRIA, 54506, Vandœuvre-les-Nancy Cedex, France</json:string></affiliations></json:item><json:item><name>Sorin Stratulat</name><affiliations><json:string>INRIA–Sophia Antipolis, 2004 Route des Lucioles, 06092, Sophia Antipolis, France</json:string></affiliations></json:item><json:item><name>Francis Klay</name><affiliations><json:string>Technopole Anticipa, France Telecom CNET DTL/MSV, 2 av. Pierre Marzin, 22307, Lannion, France</json:string></affiliations></json:item></author><subject><json:item><lang><json:string>eng</json:string></lang><value>ABR conformance algorithm</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>mechanical verification</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>PVS theorem prover</value></json:item></subject><articleId><json:string>5112135</json:string><json:string>Art2</json:string></articleId><arkIstex>ark:/67375/VQC-P5HVP0B2-1</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: The Available Bit Rate protocol (ABR) for ATM networks is well adapted to data traffic by providing minimum rate guarantees and low cell loss to the ABR source end system. An ABR conformance algorithm for controlling the source rates through an interface has been defined by ATM Forum, and a more efficient version of it has been designed by Rabadan and Klay. We present in this work the first complete mechanical verification of the equivalence between these two algorithms. The proof is involved and has been supported by the PVS theorem prover. It has required many lemmas, case analysis, and induction reasoning for the manipulation of unbounded scheduling lists. Some ABR conformance protocols have been verified in previous works. However, these protocols are approximations of the one we consider here. In particular, the algorithms assume a bound on the number of rates to be scheduled.</abstract><qualityIndicators><score>8.752</score><pdfWordCount>8396</pdfWordCount><pdfCharCount>44861</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>25</pdfPageCount><pdfPageSize>595 x 842 pts (A4)</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>146</abstractWordCount><abstractCharCount>904</abstractCharCount><keywordCount>3</keywordCount></qualityIndicators><title>Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm</title><genre><json:string>research-article</json:string></genre><host><title>Journal of Automated Reasoning</title><language><json:string>unknown</json:string></language><publicationDate>2003</publicationDate><copyrightDate>2003</copyrightDate><issn><json:string>0168-7433</json:string></issn><eissn><json:string>1573-0670</json:string></eissn><journalId><json:string>10817</json:string></journalId><volume>30</volume><issue>2</issue><pages><first>153</first><last>177</last></pages><genre><json:string>journal</json:string></genre><subject><json:item><value>Logic</value></json:item><json:item><value>Symbolic and Algebraic Manipulation</value></json:item><json:item><value>Artificial Intelligence (incl. Robotics)</value></json:item><json:item><value>Mathematical Logic and Foundations</value></json:item></subject></host><ark><json:string>ark:/67375/VQC-P5HVP0B2-1</json:string></ark><publicationDate>2003</publicationDate><copyrightDate>2003</copyrightDate><doi><json:string>10.1023/A:1023251327012</json:string></doi><id>7D3A15E739ABB9074DA25DB14FF8816664BC9D76</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/ark:/67375/VQC-P5HVP0B2-1/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/VQC-P5HVP0B2-1/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/VQC-P5HVP0B2-1/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm</title></titleStmt><publicationStmt><authority>ISTEX</authority><publisher scheme="https://scientific-publisher.data.istex.fr">Kluwer Academic Publishers</publisher><pubPlace>Dordrecht</pubPlace><availability><licence><p>Kluwer Academic Publishers, 2003</p></licence><p scheme="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-3XSW68JL-F">springer</p></availability><date>2003</date></publicationStmt><notesStmt><note type="research-article" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</note><note type="journal" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</note></notesStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm</title><author xml:id="author-0000"><persName><forename type="first">Michaël</forename><surname>Rusinowitch</surname></persName><affiliation>LORIA-INRIA, 54506, Vandœuvre-les-Nancy Cedex, France</affiliation></author><author xml:id="author-0001"><persName><forename type="first">Sorin</forename><surname>Stratulat</surname></persName><affiliation>INRIA–Sophia Antipolis, 2004 Route des Lucioles, 06092, Sophia Antipolis, France</affiliation></author><author xml:id="author-0002"><persName><forename type="first">Francis</forename><surname>Klay</surname></persName><affiliation>Technopole Anticipa, France Telecom CNET DTL/MSV, 2 av. Pierre Marzin, 22307, Lannion, France</affiliation></author><idno type="istex">7D3A15E739ABB9074DA25DB14FF8816664BC9D76</idno><idno type="ark">ark:/67375/VQC-P5HVP0B2-1</idno><idno type="DOI">10.1023/A:1023251327012</idno><idno type="article-id">5112135</idno><idno type="article-id">Art2</idno></analytic><monogr><title level="j">Journal of Automated Reasoning</title><title level="j" type="abbrev">Journal of Automated Reasoning</title><idno type="pISSN">0168-7433</idno><idno type="eISSN">1573-0670</idno><idno type="journal-ID">true</idno><idno type="issue-article-count">4</idno><idno type="volume-issue-count">4</idno><imprint><publisher>Kluwer Academic Publishers</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="2003-02-01"></date><biblScope unit="volume">30</biblScope><biblScope unit="issue">2</biblScope><biblScope unit="page" from="153">153</biblScope><biblScope unit="page" to="177">177</biblScope></imprint></monogr></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>2003</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>Abstract: The Available Bit Rate protocol (ABR) for ATM networks is well adapted to data traffic by providing minimum rate guarantees and low cell loss to the ABR source end system. An ABR conformance algorithm for controlling the source rates through an interface has been defined by ATM Forum, and a more efficient version of it has been designed by Rabadan and Klay. We present in this work the first complete mechanical verification of the equivalence between these two algorithms. The proof is involved and has been supported by the PVS theorem prover. It has required many lemmas, case analysis, and induction reasoning for the manipulation of unbounded scheduling lists. Some ABR conformance protocols have been verified in previous works. However, these protocols are approximations of the one we consider here. In particular, the algorithms assume a bound on the number of rates to be scheduled.</p></abstract><textClass xml:lang="en"><keywords scheme="keyword"><list><item><term>ABR conformance algorithm</term></item><item><term>mechanical verification</term></item><item><term>PVS theorem prover</term></item></list></keywords></textClass><textClass><keywords scheme="Journal Subject"><list><head>Philosophy</head><item><term>Logic</term></item><item><term>Symbolic and Algebraic Manipulation</term></item><item><term>Artificial Intelligence (incl. Robotics)</term></item><item><term>Mathematical Logic and Foundations</term></item></list></keywords></textClass></profileDesc><revisionDesc><change when="2003-02-01">Published</change></revisionDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/ark:/67375/VQC-P5HVP0B2-1/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="corpus springer-journals not found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType><istex:document><Publisher><PublisherInfo><PublisherName>Kluwer Academic Publishers</PublisherName><PublisherLocation>Dordrecht</PublisherLocation></PublisherInfo><Journal><JournalInfo JournalProductType="ArchiveJournal" NumberingStyle="Unnumbered"><JournalID>10817</JournalID><JournalPrintISSN>0168-7433</JournalPrintISSN><JournalElectronicISSN>1573-0670</JournalElectronicISSN><JournalTitle>Journal of Automated Reasoning</JournalTitle><JournalAbbreviatedTitle>Journal of Automated Reasoning</JournalAbbreviatedTitle><JournalSubjectGroup><JournalSubject Type="Primary">Philosophy</JournalSubject><JournalSubject Type="Secondary">Logic</JournalSubject><JournalSubject Type="Secondary">Symbolic and Algebraic Manipulation</JournalSubject><JournalSubject Type="Secondary">Artificial Intelligence (incl. Robotics)</JournalSubject><JournalSubject Type="Secondary">Mathematical Logic and Foundations</JournalSubject></JournalSubjectGroup></JournalInfo><Volume><VolumeInfo VolumeType="Regular" TocLevels="0"><VolumeIDStart>30</VolumeIDStart><VolumeIDEnd>30</VolumeIDEnd><VolumeIssueCount>4</VolumeIssueCount></VolumeInfo><Issue IssueType="Regular"><IssueInfo TocLevels="0"><IssueIDStart>2</IssueIDStart><IssueIDEnd>2</IssueIDEnd><IssueArticleCount>4</IssueArticleCount><IssueHistory><CoverDate><Year>2003</Year><Month>2</Month></CoverDate></IssueHistory><IssueCopyright><CopyrightHolderName>Kluwer Academic Publishers</CopyrightHolderName><CopyrightYear>2003</CopyrightYear></IssueCopyright></IssueInfo><Article ID="Art2"><ArticleInfo Language="En" ArticleType="OriginalPaper" NumberingStyle="Unnumbered" TocLevels="0" ContainsESM="No"><ArticleID>5112135</ArticleID><ArticleDOI>10.1023/A:1023251327012</ArticleDOI><ArticleSequenceNumber>2</ArticleSequenceNumber><ArticleTitle Language="En">Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm</ArticleTitle><ArticleFirstPage>153</ArticleFirstPage><ArticleLastPage>177</ArticleLastPage><ArticleHistory><RegistrationDate><Year>2004</Year><Month>10</Month><Day>10</Day></RegistrationDate></ArticleHistory><ArticleCopyright><CopyrightHolderName>Kluwer Academic Publishers</CopyrightHolderName><CopyrightYear>2003</CopyrightYear></ArticleCopyright><ArticleGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant><AbstractGrant Grant="OpenAccess"></AbstractGrant><BodyPDFGrant Grant="Restricted"></BodyPDFGrant><BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant><BibliographyGrant Grant="Restricted"></BibliographyGrant><ESMGrant Grant="Restricted"></ESMGrant></ArticleGrants><ArticleContext><JournalID>10817</JournalID><VolumeIDStart>30</VolumeIDStart><VolumeIDEnd>30</VolumeIDEnd><IssueIDStart>2</IssueIDStart><IssueIDEnd>2</IssueIDEnd></ArticleContext></ArticleInfo><ArticleHeader><AuthorGroup><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Michaël</GivenName><FamilyName>Rusinowitch</FamilyName></AuthorName></Author><Author AffiliationIDS="Aff2"><AuthorName DisplayOrder="Western"><GivenName>Sorin</GivenName><FamilyName>Stratulat</FamilyName></AuthorName></Author><Author AffiliationIDS="Aff3"><AuthorName DisplayOrder="Western"><GivenName>Francis</GivenName><FamilyName>Klay</FamilyName></AuthorName></Author><Affiliation ID="Aff1"><OrgName>LORIA-INRIA</OrgName><OrgAddress><Postcode>54506</Postcode><City>Vandœuvre-les-Nancy Cedex</City><Country>France</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgName>INRIA–Sophia Antipolis</OrgName><OrgAddress><Street>2004 Route des Lucioles</Street><Postcode>06092</Postcode><City>Sophia Antipolis</City><Country>France</Country></OrgAddress></Affiliation><Affiliation ID="Aff3"><OrgDivision>Technopole Anticipa</OrgDivision><OrgName>France Telecom CNET DTL/MSV</OrgName><OrgAddress><Street>2 av. Pierre Marzin</Street><Postcode>22307</Postcode><City>Lannion</City><Country>France</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>The Available Bit Rate protocol (ABR) for ATM networks is well adapted to data traffic by providing minimum rate guarantees and low cell loss to the ABR source end system. An ABR conformance algorithm for controlling the source rates through an interface has been defined by ATM Forum, and a more efficient version of it has been designed by Rabadan and Klay. We present in this work the first complete mechanical verification of the equivalence between these two algorithms. The proof is involved and has been supported by the PVS theorem prover. It has required many lemmas, case analysis, and induction reasoning for the manipulation of unbounded scheduling lists. Some ABR conformance protocols have been verified in previous works. However, these protocols are approximations of the one we consider here. In particular, the algorithms assume a bound on the number of rates to be scheduled.</Para></Abstract><KeywordGroup Language="En"><Keyword>ABR conformance algorithm</Keyword><Keyword>mechanical verification</Keyword><Keyword>PVS theorem prover</Keyword></KeywordGroup></ArticleHeader><NoBody></NoBody></Article></Issue></Volume></Journal></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm</title></titleInfo><name type="personal"><namePart type="given">Michaël</namePart><namePart type="family">Rusinowitch</namePart><affiliation>LORIA-INRIA, 54506, Vandœuvre-les-Nancy Cedex, France</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Sorin</namePart><namePart type="family">Stratulat</namePart><affiliation>INRIA–Sophia Antipolis, 2004 Route des Lucioles, 06092, Sophia Antipolis, France</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Francis</namePart><namePart type="family">Klay</namePart><affiliation>Technopole Anticipa, France Telecom CNET DTL/MSV, 2 av. Pierre Marzin, 22307, Lannion, France</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre type="research-article" displayLabel="OriginalPaper" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</genre><originInfo><publisher>Kluwer Academic Publishers</publisher><place><placeTerm type="text">Dordrecht</placeTerm></place><dateIssued encoding="w3cdtf">2003-02-01</dateIssued><copyrightDate encoding="w3cdtf">2003</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">Abstract: The Available Bit Rate protocol (ABR) for ATM networks is well adapted to data traffic by providing minimum rate guarantees and low cell loss to the ABR source end system. An ABR conformance algorithm for controlling the source rates through an interface has been defined by ATM Forum, and a more efficient version of it has been designed by Rabadan and Klay. We present in this work the first complete mechanical verification of the equivalence between these two algorithms. The proof is involved and has been supported by the PVS theorem prover. It has required many lemmas, case analysis, and induction reasoning for the manipulation of unbounded scheduling lists. Some ABR conformance protocols have been verified in previous works. However, these protocols are approximations of the one we consider here. In particular, the algorithms assume a bound on the number of rates to be scheduled.</abstract><subject lang="en"><topic>ABR conformance algorithm</topic><topic>mechanical verification</topic><topic>PVS theorem prover</topic></subject><relatedItem type="host"><titleInfo><title>Journal of Automated Reasoning</title></titleInfo><titleInfo type="abbreviated"><title>Journal of Automated Reasoning</title></titleInfo><genre type="journal" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</genre><originInfo><publisher>Springer</publisher><dateIssued encoding="w3cdtf">2003-02-01</dateIssued><copyrightDate encoding="w3cdtf">2003</copyrightDate></originInfo><subject><genre>Philosophy</genre><topic>Logic</topic><topic>Symbolic and Algebraic Manipulation</topic><topic>Artificial Intelligence (incl. Robotics)</topic><topic>Mathematical Logic and Foundations</topic></subject><identifier type="ISSN">0168-7433</identifier><identifier type="eISSN">1573-0670</identifier><identifier type="JournalID">10817</identifier><identifier type="IssueArticleCount">4</identifier><identifier type="VolumeIssueCount">4</identifier><part><date>2003</date><detail type="volume"><number>30</number><caption>vol.</caption></detail><detail type="issue"><number>2</number><caption>no.</caption></detail><extent unit="pages"><start>153</start><end>177</end></extent></part><recordInfo><recordOrigin>Kluwer Academic Publishers, 2003</recordOrigin></recordInfo></relatedItem><identifier type="istex">7D3A15E739ABB9074DA25DB14FF8816664BC9D76</identifier><identifier type="ark">ark:/67375/VQC-P5HVP0B2-1</identifier><identifier type="DOI">10.1023/A:1023251327012</identifier><identifier type="ArticleID">5112135</identifier><identifier type="ArticleID">Art2</identifier><accessCondition type="use and reproduction" contentType="copyright">Kluwer Academic Publishers, 2003</accessCondition><recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-3XSW68JL-F">springer</recordContentSource><recordOrigin>Kluwer Academic Publishers, 2003</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/VQC-P5HVP0B2-1/record.json</uri></json:item></metadata><serie></serie></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001D20 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 001D20 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Corpus
|type= RBID
|clé= ISTEX:7D3A15E739ABB9074DA25DB14FF8816664BC9D76
|texte= Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm
}}
| This area was generated with Dilib version V0.6.33. |  |