Automated verification by induction with associative-commutative operators
Identifieur interne : 003799 ( Istex/Corpus ); précédent : 003798; suivant : 003800Automated verification by induction with associative-commutative operators
Auteurs : Narjes Berregeb ; Adel Bouhoula ; Michaël RusinowitchSource :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Theories with associative and commutative (AC) operators, such as arithmetic, process algebras, boolean algebras, sets, ... are ubiquitous in software and hardware verification. These AC operators are difficult to handle by automatic deduction since they generate complex proofs. In this paper, we present new techniques for combining induction and AC reasoning, in a rewrite-based theorem prover. The resulting system has proved to be quite successful for verification tasks. Thanks to its careful rewriting strategy, it needs less interaction on typical verification problems than well known tools like NQTHM, LP or PVS. We also believe that our approach can easily be integrated as an efficient tactic in other proof systems.
Url:
DOI: 10.1007/3-540-61474-5_71
Links to Exploration step
ISTEX:E9F123D3ED03599B657089AE9C5A6838E505D6BFLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Automated verification by induction with associative-commutative operators</title><author><name sortKey="Berregeb, Narjes" sort="Berregeb, Narjes" uniqKey="Berregeb N" first="Narjes" last="Berregeb">Narjes Berregeb</name><affiliation><mods:affiliation>INRIA Lorraine & CRIN, Campus Scientifique 615, rue du Jardin Botanique, B.P. 101, 54602, Villers-lès-Nancy Cedex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: berregeb@loria.fr</mods:affiliation></affiliation></author><author><name sortKey="Bouhoula, Adel" sort="Bouhoula, Adel" uniqKey="Bouhoula A" first="Adel" last="Bouhoula">Adel Bouhoula</name><affiliation><mods:affiliation>INRIA Lorraine & CRIN, Campus Scientifique 615, rue du Jardin Botanique, B.P. 101, 54602, Villers-lès-Nancy Cedex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: bouhoula@loria.fr</mods:affiliation></affiliation></author><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name><affiliation><mods:affiliation>Computer Science Laboratory, SRI International, 333 Ravenswood Avenue, 94025, Menlo Park, California, USA</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: rusi@loria.fr</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:E9F123D3ED03599B657089AE9C5A6838E505D6BF</idno><date when="1996" year="1996">1996</date><idno type="doi">10.1007/3-540-61474-5_71</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-71NSFP69-K/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003799</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003799</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Automated verification by induction with associative-commutative operators</title><author><name sortKey="Berregeb, Narjes" sort="Berregeb, Narjes" uniqKey="Berregeb N" first="Narjes" last="Berregeb">Narjes Berregeb</name><affiliation><mods:affiliation>INRIA Lorraine & CRIN, Campus Scientifique 615, rue du Jardin Botanique, B.P. 101, 54602, Villers-lès-Nancy Cedex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: berregeb@loria.fr</mods:affiliation></affiliation></author><author><name sortKey="Bouhoula, Adel" sort="Bouhoula, Adel" uniqKey="Bouhoula A" first="Adel" last="Bouhoula">Adel Bouhoula</name><affiliation><mods:affiliation>INRIA Lorraine & CRIN, Campus Scientifique 615, rue du Jardin Botanique, B.P. 101, 54602, Villers-lès-Nancy Cedex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: bouhoula@loria.fr</mods:affiliation></affiliation></author><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name><affiliation><mods:affiliation>Computer Science Laboratory, SRI International, 333 Ravenswood Avenue, 94025, Menlo Park, California, USA</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: rusi@loria.fr</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><title level="s" type="abbrev">Lect Notes Comput Sci</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Theories with associative and commutative (AC) operators, such as arithmetic, process algebras, boolean algebras, sets, ... are ubiquitous in software and hardware verification. These AC operators are difficult to handle by automatic deduction since they generate complex proofs. In this paper, we present new techniques for combining induction and AC reasoning, in a rewrite-based theorem prover. The resulting system has proved to be quite successful for verification tasks. Thanks to its careful rewriting strategy, it needs less interaction on typical verification problems than well known tools like NQTHM, LP or PVS. We also believe that our approach can easily be integrated as an efficient tactic in other proof systems.</div></front></TEI><istex><corpusName>springer-ebooks</corpusName><author><json:item><name>Narjes Berregeb</name><affiliations><json:string>INRIA Lorraine & CRIN, Campus Scientifique 615, rue du Jardin Botanique, B.P. 101, 54602, Villers-lès-Nancy Cedex, France</json:string><json:string>E-mail: berregeb@loria.fr</json:string></affiliations></json:item><json:item><name>Adel Bouhoula</name><affiliations><json:string>INRIA Lorraine & CRIN, Campus Scientifique 615, rue du Jardin Botanique, B.P. 101, 54602, Villers-lès-Nancy Cedex, France</json:string><json:string>E-mail: bouhoula@loria.fr</json:string></affiliations></json:item><json:item><name>Michaël Rusinowitch</name><affiliations><json:string>Computer Science Laboratory, SRI International, 333 Ravenswood Avenue, 94025, Menlo Park, California, USA</json:string><json:string>E-mail: rusi@loria.fr</json:string></affiliations></json:item></author><arkIstex>ark:/67375/HCB-71NSFP69-K</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>ReviewPaper</json:string></originalGenre><abstract>Abstract: Theories with associative and commutative (AC) operators, such as arithmetic, process algebras, boolean algebras, sets, ... are ubiquitous in software and hardware verification. These AC operators are difficult to handle by automatic deduction since they generate complex proofs. In this paper, we present new techniques for combining induction and AC reasoning, in a rewrite-based theorem prover. The resulting system has proved to be quite successful for verification tasks. Thanks to its careful rewriting strategy, it needs less interaction on typical verification problems than well known tools like NQTHM, LP or PVS. We also believe that our approach can easily be integrated as an efficient tactic in other proof systems.</abstract><qualityIndicators><refBibsNative>false</refBibsNative><abstractWordCount>110</abstractWordCount><abstractCharCount>738</abstractCharCount><keywordCount>0</keywordCount><score>8.32</score><pdfWordCount>5637</pdfWordCount><pdfCharCount>24837</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>12</pdfPageCount><pdfPageSize>439.28 x 666 pts</pdfPageSize></qualityIndicators><title>Automated verification by induction with associative-commutative operators</title><chapterId><json:string>19</json:string><json:string>Chap19</json:string></chapterId><genre><json:string>conference</json:string></genre><serie><title>Lecture Notes in Computer Science</title><language><json:string>unknown</json:string></language><copyrightDate>1996</copyrightDate><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><editor><json:item><name>Gerhard Goos</name></json:item><json:item><name>Juris Hartmanis</name></json:item><json:item><name>Jan van Leeuwen</name></json:item></editor></serie><host><title>Computer Aided Verification</title><language><json:string>unknown</json:string></language><copyrightDate>1996</copyrightDate><doi><json:string>10.1007/3-540-61474-5</json:string></doi><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><eisbn><json:string>978-3-540-68599-9</json:string></eisbn><bookId><json:string>3540614745</json:string></bookId><isbn><json:string>978-3-540-61474-6</json:string></isbn><volume>1102</volume><pages><first>220</first><last>231</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Rajeev Alur</name></json:item><json:item><name>Thomas A. Henzinger</name></json:item></editor><subject><json:item><value>Computer Science</value></json:item><json:item><value>Computer Science</value></json:item><json:item><value>Logics and Meanings of Programs</value></json:item><json:item><value>Software Engineering</value></json:item><json:item><value>Mathematical Logic and Formal Languages</value></json:item><json:item><value>Special Purpose and Application-Based Systems</value></json:item><json:item><value>Artificial Intelligence (incl. Robotics)</value></json:item></subject></host><ark><json:string>ark:/67375/HCB-71NSFP69-K</json:string></ark><publicationDate>1996</publicationDate><copyrightDate>1996</copyrightDate><doi><json:string>10.1007/3-540-61474-5_71</json:string></doi><id>E9F123D3ED03599B657089AE9C5A6838E505D6BF</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-71NSFP69-K/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-71NSFP69-K/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-71NSFP69-K/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Automated verification by induction with associative-commutative operators</title></titleStmt><publicationStmt><authority>ISTEX</authority><availability><licence>Springer-Verlag</licence></availability><date when="1996">1996</date></publicationStmt><notesStmt><note type="conference" source="proceedings" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</note><note type="publication-type" subtype="book-series" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</note></notesStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Automated verification by induction with associative-commutative operators</title><author><persName><forename type="first">Narjes</forename><surname>Berregeb</surname></persName><email>berregeb@loria.fr</email><affiliation><orgName type="institution">INRIA Lorraine & CRIN</orgName><address><street>Campus Scientifique 615, rue du Jardin Botanique</street><postBox>B.P. 101</postBox><postCode>54602</postCode><settlement>Villers-lès-Nancy Cedex</settlement><country key="FR">FRANCE</country></address></affiliation></author><author><persName><forename type="first">Adel</forename><surname>Bouhoula</surname></persName><email>bouhoula@loria.fr</email><affiliation><orgName type="institution">INRIA Lorraine & CRIN</orgName><address><street>Campus Scientifique 615, rue du Jardin Botanique</street><postBox>B.P. 101</postBox><postCode>54602</postCode><settlement>Villers-lès-Nancy Cedex</settlement><country key="FR">FRANCE</country></address></affiliation></author><author><persName><forename type="first">Michaël</forename><surname>Rusinowitch</surname></persName><email>rusi@loria.fr</email><affiliation><orgName type="department">Computer Science Laboratory</orgName><orgName type="institution">SRI International</orgName><address><street>333 Ravenswood Avenue</street><postCode>94025</postCode><settlement>Menlo Park</settlement><region>California</region><country key="US">UNITED STATES</country></address></affiliation></author><idno type="istex">E9F123D3ED03599B657089AE9C5A6838E505D6BF</idno><idno type="ark">ark:/67375/HCB-71NSFP69-K</idno><idno type="DOI">10.1007/3-540-61474-5_71</idno></analytic><monogr><title level="m" type="main">Computer Aided Verification</title><title level="m" type="sub">8th International Conference, CAV '96 New Brunswick, NJ, USA, July 31– August 3, 1996 Proceedings</title><idno type="DOI">10.1007/3-540-61474-5</idno><idno type="book-id">3540614745</idno><idno type="ISBN">978-3-540-61474-6</idno><idno type="eISBN">978-3-540-68599-9</idno><idno type="chapter-id">Chap19</idno><editor><persName><forename type="first">Rajeev</forename><surname>Alur</surname></persName></editor><editor><persName><forename type="first">Thomas</forename><forename type="first">A.</forename><surname>Henzinger</surname></persName></editor><imprint><biblScope unit="vol">1102</biblScope><biblScope unit="page" from="220">220</biblScope><biblScope unit="page" to="231">231</biblScope><biblScope unit="chapter-count">52</biblScope></imprint></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><title level="s" type="abbrev">Lect Notes Comput Sci</title><editor><persName><forename type="first">Gerhard</forename><surname>Goos</surname></persName></editor><editor><persName><forename type="first">Juris</forename><surname>Hartmanis</surname></persName></editor><editor><persName><forename type="first">Jan</forename><nameLink>van</nameLink><surname>Leeuwen</surname></persName></editor><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="seriesID">558</idno></series></biblStruct></sourceDesc></fileDesc><profileDesc><abstract xml:lang="en"><head>Abstract</head><p>Theories with associative and commutative (AC) operators, such as arithmetic, process algebras, boolean algebras, sets, ... are ubiquitous in software and hardware verification. These AC operators are difficult to handle by automatic deduction since they generate complex proofs. In this paper, we present new techniques for combining induction and AC reasoning, in a rewrite-based theorem prover. The resulting system has proved to be quite successful for verification tasks. Thanks to its careful rewriting strategy, it needs less interaction on typical verification problems than well known tools like NQTHM, LP or PVS. We also believe that our approach can easily be integrated as an efficient tactic in other proof systems.</p></abstract><textClass ana="subject"><keywords scheme="book-subject-collection"><list><label>SUCO11645</label><item><term>Computer Science</term></item></list></keywords></textClass><textClass ana="subject"><keywords scheme="book-subject"><list><label>I</label><item><term type="Primary">Computer Science</term></item><label>I1603X</label><item><term type="Secondary" subtype="priority-1">Logics and Meanings of Programs</term></item><label>I14029</label><item><term type="Secondary" subtype="priority-2">Software Engineering</term></item><label>I16048</label><item><term type="Secondary" subtype="priority-3">Mathematical Logic and Formal Languages</term></item><label>I13030</label><item><term type="Secondary" subtype="priority-4">Special Purpose and Application-Based Systems</term></item><label>I21017</label><item><term type="Secondary" subtype="priority-5">Artificial Intelligence (incl. Robotics)</term></item></list></keywords></textClass><langUsage><language ident="EN"></language></langUsage></profileDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-71NSFP69-K/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="corpus springer-ebooks 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>Springer Berlin Heidelberg</PublisherName><PublisherLocation>Berlin, Heidelberg</PublisherLocation></PublisherInfo><Series><SeriesInfo TocLevels="0"><SeriesID>558</SeriesID><SeriesPrintISSN>0302-9743</SeriesPrintISSN><SeriesElectronicISSN>1611-3349</SeriesElectronicISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle><SeriesAbbreviatedTitle>Lect Notes Comput Sci</SeriesAbbreviatedTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName><FamilyName>Goos</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Juris</GivenName><FamilyName>Hartmanis</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Jan</GivenName><Particle>van</Particle><FamilyName>Leeuwen</FamilyName></EditorName></Editor></EditorGroup></SeriesHeader><Book Language="En"><BookInfo MediaType="eBook" Language="En" BookProductType="Proceedings" TocLevels="0" NumberingStyle="Unnumbered"><BookID>3540614745</BookID><BookTitle>Computer Aided Verification</BookTitle><BookSubTitle>8th International Conference, CAV '96 New Brunswick, NJ, USA, July 31– August 3, 1996 Proceedings</BookSubTitle><BookVolumeNumber>1102</BookVolumeNumber><BookDOI>10.1007/3-540-61474-5</BookDOI><BookTitleID>45026</BookTitleID><BookPrintISBN>978-3-540-61474-6</BookPrintISBN><BookElectronicISBN>978-3-540-68599-9</BookElectronicISBN><BookChapterCount>52</BookChapterCount><BookCopyright><CopyrightHolderName>Springer-Verlag</CopyrightHolderName><CopyrightYear>1996</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I1603X" Priority="1" Type="Secondary">Logics and Meanings of Programs</BookSubject><BookSubject Code="I14029" Priority="2" Type="Secondary">Software Engineering</BookSubject><BookSubject Code="I16048" Priority="3" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject><BookSubject Code="I13030" Priority="4" Type="Secondary">Special Purpose and Application-Based Systems</BookSubject><BookSubject Code="I21017" Priority="5" Type="Secondary">Artificial Intelligence (incl. Robotics)</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup></BookInfo><BookHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>Rajeev</GivenName><FamilyName>Alur</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Thomas</GivenName><GivenName>A.</GivenName><FamilyName>Henzinger</FamilyName></EditorName></Editor></EditorGroup></BookHeader><Chapter ID="Chap19" Language="En"><ChapterInfo ChapterType="ReviewPaper" NumberingStyle="Unnumbered" TocLevels="0" ContainsESM="No"><ChapterID>19</ChapterID><ChapterDOI>10.1007/3-540-61474-5_71</ChapterDOI><ChapterSequenceNumber>19</ChapterSequenceNumber><ChapterTitle Language="En">Automated verification by induction with associative-commutative operators</ChapterTitle><ChapterFirstPage>220</ChapterFirstPage><ChapterLastPage>231</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag</CopyrightHolderName><CopyrightYear>1996</CopyrightYear></ChapterCopyright><ChapterHistory><OnlineDate><Year>2005</Year><Month>6</Month><Day>3</Day></OnlineDate></ChapterHistory><ChapterGrants 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></ChapterGrants><ChapterContext><SeriesID>558</SeriesID><BookID>3540614745</BookID><BookTitle>Computer Aided Verification</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Narjes</GivenName><FamilyName>Berregeb</FamilyName></AuthorName><Contact><Email>berregeb@loria.fr</Email></Contact></Author><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Adel</GivenName><FamilyName>Bouhoula</FamilyName></AuthorName><Contact><Email>bouhoula@loria.fr</Email></Contact></Author><Author AffiliationIDS="Aff2"><AuthorName DisplayOrder="Western"><GivenName>Michaël</GivenName><FamilyName>Rusinowitch</FamilyName></AuthorName><Contact><Email>rusi@loria.fr</Email></Contact></Author><Affiliation ID="Aff1"><OrgName>INRIA Lorraine & CRIN</OrgName><OrgAddress><Street>Campus Scientifique 615, rue du Jardin Botanique</Street><Postbox>B.P. 101</Postbox><Postcode>54602</Postcode><City>Villers-lès-Nancy Cedex</City><Country>France</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgDivision>Computer Science Laboratory</OrgDivision><OrgName>SRI International</OrgName><OrgAddress><Street>333 Ravenswood Avenue</Street><Postcode>94025</Postcode><City>Menlo Park</City><State>California</State><Country>USA</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>Theories with associative and commutative (AC) operators, such as arithmetic, process algebras, boolean algebras, sets, ... are ubiquitous in software and hardware verification. These AC operators are difficult to handle by automatic deduction since they generate complex proofs. In this paper, we present new techniques for combining induction and AC reasoning, in a rewrite-based theorem prover. The resulting system has proved to be quite successful for verification tasks. Thanks to its careful rewriting strategy, it needs less interaction on typical verification problems than well known tools like NQTHM, LP or PVS. We also believe that our approach can easily be integrated as an efficient tactic in other proof systems.</Para></Abstract></ChapterHeader><NoBody></NoBody></Chapter></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Automated verification by induction with associative-commutative operators</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Automated verification by induction with associative-commutative operators</title></titleInfo><name type="personal"><namePart type="given">Narjes</namePart><namePart type="family">Berregeb</namePart><affiliation>INRIA Lorraine & CRIN, Campus Scientifique 615, rue du Jardin Botanique, B.P. 101, 54602, Villers-lès-Nancy Cedex, France</affiliation><affiliation>E-mail: berregeb@loria.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Adel</namePart><namePart type="family">Bouhoula</namePart><affiliation>INRIA Lorraine & CRIN, Campus Scientifique 615, rue du Jardin Botanique, B.P. 101, 54602, Villers-lès-Nancy Cedex, France</affiliation><affiliation>E-mail: bouhoula@loria.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Michaël</namePart><namePart type="family">Rusinowitch</namePart><affiliation>Computer Science Laboratory, SRI International, 333 Ravenswood Avenue, 94025, Menlo Park, California, USA</affiliation><affiliation>E-mail: rusi@loria.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre displayLabel="ReviewPaper" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" type="conference" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</genre><originInfo><publisher>Springer Berlin Heidelberg</publisher><place><placeTerm type="text">Berlin, Heidelberg</placeTerm></place><dateIssued encoding="w3cdtf">1996</dateIssued><copyrightDate encoding="w3cdtf">1996</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">Abstract: Theories with associative and commutative (AC) operators, such as arithmetic, process algebras, boolean algebras, sets, ... are ubiquitous in software and hardware verification. These AC operators are difficult to handle by automatic deduction since they generate complex proofs. In this paper, we present new techniques for combining induction and AC reasoning, in a rewrite-based theorem prover. The resulting system has proved to be quite successful for verification tasks. Thanks to its careful rewriting strategy, it needs less interaction on typical verification problems than well known tools like NQTHM, LP or PVS. We also believe that our approach can easily be integrated as an efficient tactic in other proof systems.</abstract><relatedItem type="host"><titleInfo><title>Computer Aided Verification</title><subTitle>8th International Conference, CAV '96 New Brunswick, NJ, USA, July 31– August 3, 1996 Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Rajeev</namePart><namePart type="family">Alur</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Thomas</namePart><namePart type="given">A.</namePart><namePart type="family">Henzinger</namePart><role><roleTerm type="text">editor</roleTerm></role></name><genre type="book-series" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</genre><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">1996</copyrightDate><issuance>monographic</issuance></originInfo><subject><genre>Book-Subject-Collection</genre><topic authority="SpringerSubjectCodes" authorityURI="SUCO11645">Computer Science</topic></subject><subject><genre>Book-Subject-Group</genre><topic authority="SpringerSubjectCodes" authorityURI="I">Computer Science</topic><topic authority="SpringerSubjectCodes" authorityURI="I1603X">Logics and Meanings of Programs</topic><topic authority="SpringerSubjectCodes" authorityURI="I14029">Software Engineering</topic><topic authority="SpringerSubjectCodes" authorityURI="I16048">Mathematical Logic and Formal Languages</topic><topic authority="SpringerSubjectCodes" authorityURI="I13030">Special Purpose and Application-Based Systems</topic><topic authority="SpringerSubjectCodes" authorityURI="I21017">Artificial Intelligence (incl. Robotics)</topic></subject><identifier type="DOI">10.1007/3-540-61474-5</identifier><identifier type="ISBN">978-3-540-61474-6</identifier><identifier type="eISBN">978-3-540-68599-9</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="BookTitleID">45026</identifier><identifier type="BookID">3540614745</identifier><identifier type="BookChapterCount">52</identifier><identifier type="BookVolumeNumber">1102</identifier><part><date>1996</date><detail type="volume"><number>1102</number><caption>vol.</caption></detail><extent unit="pages"><start>220</start><end>231</end></extent></part><recordInfo><recordOrigin>Springer-Verlag, 1996</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Goos</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Juris</namePart><namePart type="family">Hartmanis</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jan</namePart><namePart type="family">van Leeuwen</namePart><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">1996</copyrightDate><issuance>serial</issuance></originInfo><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag, 1996</recordOrigin></recordInfo></relatedItem><identifier type="istex">E9F123D3ED03599B657089AE9C5A6838E505D6BF</identifier><identifier type="ark">ark:/67375/HCB-71NSFP69-K</identifier><identifier type="DOI">10.1007/3-540-61474-5_71</identifier><identifier type="ChapterID">19</identifier><identifier type="ChapterID">Chap19</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag, 1996</accessCondition><recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-RLRX46XW-4">springer</recordContentSource><recordOrigin>Springer-Verlag, 1996</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-71NSFP69-K/record.json</uri></json:item></metadata></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 003799 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 003799 | 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:E9F123D3ED03599B657089AE9C5A6838E505D6BF
|texte= Automated verification by induction with associative-commutative operators
}}
| This area was generated with Dilib version V0.6.33. |  |