InforLorV4, Istex, Corpus, bibRecord, 000408

Decision Procedures for the Formal Analysis of Software

Identifieur interne : 000408 ( Istex/Corpus ); précédent : 000407; suivant : 000409

Decision Procedures for the Formal Analysis of Software

Auteurs : David Déharbe ; Pascal Fontaine ; Silvio Ranise ; Christophe Ringeissen

Source :

Lecture Notes in Computer Science [ 0302-9743 ]

RBID : ISTEX:1249FAC26F49FBD522B1C62A11767C491F01D85D

Abstract

Abstract: Catching bugs in programs is difficult and time-consuming. The effort of debugging and proving correct even small units of code can surpass the effort of programming. Bugs inserted while “programming in the small” can have dramatic consequences for the consistency of a whole software system as shown, e.g., by viruses which can spread by exploiting buffer overflows, a bug which typically arises while coding a small portion of code. To detect this kind of errors, many verification techniques have been put forward such as static analysis and model checking.

Url:

https://api.istex.fr/ark:/67375/HCB-C9SH85Z6-K/fulltext.pdf

DOI: 10.1007/11921240_26

Links to Exploration step

ISTEX:1249FAC26F49FBD522B1C62A11767C491F01D85D

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Decision Procedures for the Formal Analysis of Software</title>
<author><name sortKey="Deharbe, David" sort="Deharbe, David" uniqKey="Deharbe D" first="David" last="Déharbe">David Déharbe</name>
<affiliation><mods:affiliation>UFRN/DIMAp, Natal, Brazil</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: david@dimap.ufrn.br</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Fontaine, Pascal" sort="Fontaine, Pascal" uniqKey="Fontaine P" first="Pascal" last="Fontaine">Pascal Fontaine</name>
<affiliation><mods:affiliation>LORIA, Nancy, France</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: fontaine@loria.fr</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name>
<affiliation><mods:affiliation>LORIA, Nancy, France</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>Univerisità di Milano, Italy</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: ranise@loria.fr</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name>
<affiliation><mods:affiliation>LORIA, Nancy, France</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: ringeiss@loria.fr</mods:affiliation>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:1249FAC26F49FBD522B1C62A11767C491F01D85D</idno>
<date when="2006" year="2006">2006</date>
<idno type="doi">10.1007/11921240_26</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-C9SH85Z6-K/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">000408</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000408</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Decision Procedures for the Formal Analysis of Software</title>
<author><name sortKey="Deharbe, David" sort="Deharbe, David" uniqKey="Deharbe D" first="David" last="Déharbe">David Déharbe</name>
<affiliation><mods:affiliation>UFRN/DIMAp, Natal, Brazil</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: david@dimap.ufrn.br</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Fontaine, Pascal" sort="Fontaine, Pascal" uniqKey="Fontaine P" first="Pascal" last="Fontaine">Pascal Fontaine</name>
<affiliation><mods:affiliation>LORIA, Nancy, France</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: fontaine@loria.fr</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name>
<affiliation><mods:affiliation>LORIA, Nancy, France</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>Univerisità di Milano, Italy</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: ranise@loria.fr</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name>
<affiliation><mods:affiliation>LORIA, Nancy, France</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: ringeiss@loria.fr</mods:affiliation>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</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: Catching bugs in programs is difficult and time-consuming. The effort of debugging and proving correct even small units of code can surpass the effort of programming. Bugs inserted while “programming in the small” can have dramatic consequences for the consistency of a whole software system as shown, e.g., by viruses which can spread by exploiting buffer overflows, a bug which typically arises while coding a small portion of code. To detect this kind of errors, many verification techniques have been put forward such as static analysis and model checking.</div>
</front>
</TEI>
<istex><corpusName>springer-ebooks</corpusName>
<author><json:item><name>David Déharbe</name>
<affiliations><json:string>UFRN/DIMAp, Natal, Brazil</json:string>
<json:string>E-mail: david@dimap.ufrn.br</json:string>
</affiliations>
</json:item>
<json:item><name>Pascal Fontaine</name>
<affiliations><json:string>LORIA, Nancy, France</json:string>
<json:string>E-mail: fontaine@loria.fr</json:string>
</affiliations>
</json:item>
<json:item><name>Silvio Ranise</name>
<affiliations><json:string>LORIA, Nancy, France</json:string>
<json:string>Univerisità di Milano, Italy</json:string>
<json:string>E-mail: ranise@loria.fr</json:string>
</affiliations>
</json:item>
<json:item><name>Christophe Ringeissen</name>
<affiliations><json:string>LORIA, Nancy, France</json:string>
<json:string>E-mail: ringeiss@loria.fr</json:string>
</affiliations>
</json:item>
</author>
<arkIstex>ark:/67375/HCB-C9SH85Z6-K</arkIstex>
<language><json:string>eng</json:string>
</language>
<originalGenre><json:string>OriginalPaper</json:string>
</originalGenre>
<abstract>Abstract: Catching bugs in programs is difficult and time-consuming. The effort of debugging and proving correct even small units of code can surpass the effort of programming. Bugs inserted while “programming in the small” can have dramatic consequences for the consistency of a whole software system as shown, e.g., by viruses which can spread by exploiting buffer overflows, a bug which typically arises while coding a small portion of code. To detect this kind of errors, many verification techniques have been put forward such as static analysis and model checking.</abstract>
<qualityIndicators><score>5.072</score>
<pdfWordCount>1992</pdfWordCount>
<pdfCharCount>12518</pdfCharCount>
<pdfVersion>1.3</pdfVersion>
<pdfPageCount>5</pdfPageCount>
<pdfPageSize>430 x 660 pts</pdfPageSize>
<refBibsNative>false</refBibsNative>
<abstractWordCount>90</abstractWordCount>
<abstractCharCount>570</abstractCharCount>
<keywordCount>0</keywordCount>
</qualityIndicators>
<title>Decision Procedures for the Formal Analysis of Software</title>
<chapterId><json:string>26</json:string>
<json:string>Chap26</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>2006</copyrightDate>
<issn><json:string>0302-9743</json:string>
</issn>
<eissn><json:string>1611-3349</json:string>
</eissn>
<editor><json:item><name>David Hutchison</name>
<affiliations><json:string>Lancaster University, UK</json:string>
</affiliations>
</json:item>
<json:item><name>Takeo Kanade</name>
<affiliations><json:string>Carnegie Mellon University, Pittsburgh, PA, USA</json:string>
</affiliations>
</json:item>
<json:item><name>Josef Kittler</name>
<affiliations><json:string>University of Surrey, Guildford, UK</json:string>
</affiliations>
</json:item>
<json:item><name>Jon M. Kleinberg</name>
<affiliations><json:string>Cornell University, Ithaca, NY, USA</json:string>
</affiliations>
</json:item>
<json:item><name>Friedemann Mattern</name>
<affiliations><json:string>ETH Zurich, Switzerland</json:string>
</affiliations>
</json:item>
<json:item><name>John C. Mitchell</name>
<affiliations><json:string>Stanford University, CA, USA</json:string>
</affiliations>
</json:item>
<json:item><name>Moni Naor</name>
<affiliations><json:string>Weizmann Institute of Science, Rehovot, Israel</json:string>
</affiliations>
</json:item>
<json:item><name>Oscar Nierstrasz</name>
<affiliations><json:string>University of Bern, Switzerland</json:string>
</affiliations>
</json:item>
<json:item><name>C. Pandu Rangan</name>
<affiliations><json:string>Indian Institute of Technology, Madras, India</json:string>
</affiliations>
</json:item>
<json:item><name>Bernhard Steffen</name>
<affiliations><json:string>University of Dortmund, Germany</json:string>
</affiliations>
</json:item>
<json:item><name>Madhu Sudan</name>
<affiliations><json:string>Massachusetts Institute of Technology, MA, USA</json:string>
</affiliations>
</json:item>
<json:item><name>Demetri Terzopoulos</name>
<affiliations><json:string>University of California, Los Angeles, CA, USA</json:string>
</affiliations>
</json:item>
<json:item><name>Dough Tygar</name>
<affiliations><json:string>University of California, Berkeley, CA, USA</json:string>
</affiliations>
</json:item>
<json:item><name>Moshe Y. Vardi</name>
<affiliations><json:string>Rice University, Houston, TX, USA</json:string>
</affiliations>
</json:item>
<json:item><name>Gerhard Weikum</name>
<affiliations><json:string>Max-Planck Institute of Computer Science, Saarbruecken, Germany</json:string>
</affiliations>
</json:item>
</editor>
</serie>
<host><title>Theoretical Aspects of Computing - ICTAC 2006</title>
<language><json:string>unknown</json:string>
</language>
<copyrightDate>2006</copyrightDate>
<doi><json:string>10.1007/11921240</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-48816-3</json:string>
</eisbn>
<bookId><json:string>978-3-540-48816-3</json:string>
</bookId>
<isbn><json:string>978-3-540-48815-6</json:string>
</isbn>
<volume>4281</volume>
<pages><first>366</first>
<last>370</last>
</pages>
<genre><json:string>book-series</json:string>
</genre>
<editor><json:item><name>Kamel Barkaoui</name>
<affiliations><json:string>Laboratoire CEDRIC, Conservatoire National des Arts et Métiers, 192 rue Saint Martin, Paris Cedex 03, France</json:string>
<json:string>E-mail: kamel.barkaoui@cnam.fr</json:string>
</affiliations>
</json:item>
<json:item><name>Ana Cavalcanti</name>
<affiliations><json:string>Department of Computer Science, University of York, York, UK</json:string>
<json:string>E-mail: alcc@cs.york.ac.uk</json:string>
</affiliations>
</json:item>
<json:item><name>Antonio Cerone</name>
<affiliations><json:string>UNU-IIST, Macau SAR, China</json:string>
<json:string>E-mail: antonio@iist.unu.edu</json:string>
</affiliations>
</json:item>
</editor>
<subject><json:item><value>Computer Science</value>
</json:item>
<json:item><value>Computer Science</value>
</json:item>
<json:item><value>Computation by Abstract Devices</value>
</json:item>
<json:item><value>Logics and Meanings of Programs</value>
</json:item>
<json:item><value>Mathematical Logic and Formal Languages</value>
</json:item>
<json:item><value>Programming Languages, Compilers, Interpreters</value>
</json:item>
<json:item><value>Software Engineering</value>
</json:item>
<json:item><value>Computer Communication Networks</value>
</json:item>
</subject>
</host>
<ark><json:string>ark:/67375/HCB-C9SH85Z6-K</json:string>
</ark>
<publicationDate>2006</publicationDate>
<copyrightDate>2006</copyrightDate>
<doi><json:string>10.1007/11921240_26</json:string>
</doi>
<id>1249FAC26F49FBD522B1C62A11767C491F01D85D</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-C9SH85Z6-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-C9SH85Z6-K/bundle.zip</uri>
</json:item>
<istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-C9SH85Z6-K/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Decision Procedures for the Formal Analysis of Software</title>
</titleStmt>
<publicationStmt><authority>ISTEX</authority>
<availability><licence>Springer-Verlag Berlin Heidelberg</licence>
</availability>
<date when="2006">2006</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">Decision Procedures for the Formal Analysis of Software</title>
<author><persName><forename type="first">David</forename>
<surname>Déharbe</surname>
</persName>
<email>david@dimap.ufrn.br</email>
<affiliation><orgName type="institution">UFRN/DIMAp, Natal</orgName>
<address><country key="BR">BRAZIL</country>
</address>
</affiliation>
</author>
<author><persName><forename type="first">Pascal</forename>
<surname>Fontaine</surname>
</persName>
<email>fontaine@loria.fr</email>
<affiliation><orgName type="institution">LORIA, Nancy</orgName>
<address><country key="FR">FRANCE</country>
</address>
</affiliation>
</author>
<author><persName><forename type="first">Silvio</forename>
<surname>Ranise</surname>
</persName>
<email>ranise@loria.fr</email>
<affiliation><orgName type="institution">LORIA, Nancy</orgName>
<address><country key="FR">FRANCE</country>
</address>
</affiliation>
<affiliation><orgName type="institution">Univerisità di Milano</orgName>
<address><country key="IT">ITALY</country>
</address>
</affiliation>
</author>
<author><persName><forename type="first">Christophe</forename>
<surname>Ringeissen</surname>
</persName>
<email>ringeiss@loria.fr</email>
<affiliation><orgName type="institution">LORIA, Nancy</orgName>
<address><country key="FR">FRANCE</country>
</address>
</affiliation>
</author>
<idno type="istex">1249FAC26F49FBD522B1C62A11767C491F01D85D</idno>
<idno type="ark">ark:/67375/HCB-C9SH85Z6-K</idno>
<idno type="DOI">10.1007/11921240_26</idno>
</analytic>
<monogr><title level="m" type="main">Theoretical Aspects of Computing - ICTAC 2006</title>
<title level="m" type="sub">Third International Colloquium, Tunis, Tunisia, November 20-24, 2006. Proceedings</title>
<title level="m" type="part">Tutorials: Extended Abstracts</title>
<idno type="DOI">10.1007/11921240</idno>
<idno type="book-id">978-3-540-48816-3</idno>
<idno type="ISBN">978-3-540-48815-6</idno>
<idno type="eISBN">978-3-540-48816-3</idno>
<idno type="chapter-id">Chap26</idno>
<idno type="part-id">Part8</idno>
<editor><persName><forename type="first">Kamel</forename>
<surname>Barkaoui</surname>
</persName>
<email>kamel.barkaoui@cnam.fr</email>
<affiliation><orgName type="institution">Laboratoire CEDRIC, Conservatoire National des Arts et Métiers</orgName>
<address><street>192 rue Saint Martin</street>
<postCode>Paris Cedex 03</postCode>
<country key="FR">FRANCE</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Ana</forename>
<surname>Cavalcanti</surname>
</persName>
<email>alcc@cs.york.ac.uk</email>
<affiliation><orgName type="department">Department of Computer Science</orgName>
<orgName type="institution">University of York</orgName>
<address><settlement>York</settlement>
<country key="GB">UNITED KINGDOM</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Antonio</forename>
<surname>Cerone</surname>
</persName>
<email>antonio@iist.unu.edu</email>
<affiliation><orgName type="institution">UNU-IIST, Macau SAR</orgName>
<address><country key="CN">CHINA</country>
</address>
</affiliation>
</editor>
<imprint><biblScope unit="vol">4281</biblScope>
<biblScope unit="page" from="366">366</biblScope>
<biblScope unit="page" to="370">370</biblScope>
<biblScope unit="chapter-count">26</biblScope>
<biblScope unit="part-chapter-count">2</biblScope>
</imprint>
</monogr>
<series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title>
<editor><persName><forename type="first">David</forename>
<surname>Hutchison</surname>
</persName>
<affiliation><orgName type="institution">Lancaster University</orgName>
<address><country key="GB">UNITED KINGDOM</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Takeo</forename>
<surname>Kanade</surname>
</persName>
<affiliation><orgName type="institution">Carnegie Mellon University</orgName>
<address><settlement>Pittsburgh</settlement>
<region>PA</region>
<country key="US">UNITED STATES</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Josef</forename>
<surname>Kittler</surname>
</persName>
<affiliation><orgName type="institution">University of Surrey</orgName>
<address><settlement>Guildford</settlement>
<country key="GB">UNITED KINGDOM</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Jon</forename>
<forename type="first">M.</forename>
<surname>Kleinberg</surname>
</persName>
<affiliation><orgName type="institution">Cornell University</orgName>
<address><settlement>Ithaca</settlement>
<region>NY</region>
<country key="US">UNITED STATES</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Friedemann</forename>
<surname>Mattern</surname>
</persName>
<affiliation><orgName type="institution">ETH Zurich</orgName>
<address><country key="CH">SWITZERLAND</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">John</forename>
<forename type="first">C.</forename>
<surname>Mitchell</surname>
</persName>
<affiliation><orgName type="institution">Stanford University</orgName>
<address><settlement>CA</settlement>
<country key="US">UNITED STATES</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Moni</forename>
<surname>Naor</surname>
</persName>
<affiliation><orgName type="institution">Weizmann Institute of Science</orgName>
<address><settlement>Rehovot</settlement>
<country key="IL">ISRAEL</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Oscar</forename>
<surname>Nierstrasz</surname>
</persName>
<affiliation><orgName type="institution">University of Bern</orgName>
<address><country key="CH">SWITZERLAND</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">C.</forename>
<surname>Pandu Rangan</surname>
</persName>
<affiliation><orgName type="institution">Indian Institute of Technology</orgName>
<address><settlement>Madras</settlement>
<country key="IN">INDIA</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Bernhard</forename>
<surname>Steffen</surname>
</persName>
<affiliation><orgName type="institution">University of Dortmund</orgName>
<address><country key="DE">GERMANY</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Madhu</forename>
<surname>Sudan</surname>
</persName>
<affiliation><orgName type="institution">Massachusetts Institute of Technology</orgName>
<address><settlement>MA</settlement>
<country key="US">UNITED STATES</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Demetri</forename>
<surname>Terzopoulos</surname>
</persName>
<affiliation><orgName type="institution">University of California</orgName>
<address><settlement>Los Angeles</settlement>
<region>CA</region>
<country key="US">UNITED STATES</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Dough</forename>
<surname>Tygar</surname>
</persName>
<affiliation><orgName type="institution">University of California</orgName>
<address><settlement>Berkeley</settlement>
<region>CA</region>
<country key="US">UNITED STATES</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Moshe</forename>
<forename type="first">Y.</forename>
<surname>Vardi</surname>
</persName>
<affiliation><orgName type="institution">Rice University</orgName>
<address><settlement>Houston</settlement>
<region>TX</region>
<country key="US">UNITED STATES</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Gerhard</forename>
<surname>Weikum</surname>
</persName>
<affiliation><orgName type="institution">Max-Planck Institute of Computer Science</orgName>
<address><settlement>Saarbruecken</settlement>
<country key="DE">GERMANY</country>
</address>
</affiliation>
</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>Catching bugs in programs is difficult and time-consuming. The effort of debugging and proving correct even small units of code can surpass the effort of programming. Bugs inserted while “programming in the small” can have dramatic consequences for the consistency of a whole software system as shown, e.g., by viruses which can spread by exploiting buffer overflows, a bug which typically arises while coding a small portion of code. To detect this kind of errors, many verification techniques have been put forward such as static analysis and model checking.</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>I16013</label>
<item><term type="Secondary" subtype="priority-1">Computation by Abstract Devices</term>
</item>
<label>I1603X</label>
<item><term type="Secondary" subtype="priority-2">Logics and Meanings of Programs</term>
</item>
<label>I16048</label>
<item><term type="Secondary" subtype="priority-3">Mathematical Logic and Formal Languages</term>
</item>
<label>I14037</label>
<item><term type="Secondary" subtype="priority-4">Programming Languages, Compilers, Interpreters</term>
</item>
<label>I14029</label>
<item><term type="Secondary" subtype="priority-5">Software Engineering</term>
</item>
<label>I13022</label>
<item><term type="Secondary" subtype="priority-6">Computer Communication Networks</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-C9SH85Z6-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 SeriesType="Series" TocLevels="0"><SeriesID>558</SeriesID>
<SeriesPrintISSN>0302-9743</SeriesPrintISSN>
<SeriesElectronicISSN>1611-3349</SeriesElectronicISSN>
<SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle>
</SeriesInfo>
<SeriesHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>David</GivenName>
<FamilyName>Hutchison</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Takeo</GivenName>
<FamilyName>Kanade</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Josef</GivenName>
<FamilyName>Kittler</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Jon</GivenName>
<GivenName>M.</GivenName>
<FamilyName>Kleinberg</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Friedemann</GivenName>
<FamilyName>Mattern</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff6"><EditorName DisplayOrder="Western"><GivenName>John</GivenName>
<GivenName>C.</GivenName>
<FamilyName>Mitchell</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff7"><EditorName DisplayOrder="Western"><GivenName>Moni</GivenName>
<FamilyName>Naor</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff8"><EditorName DisplayOrder="Western"><GivenName>Oscar</GivenName>
<FamilyName>Nierstrasz</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff9"><EditorName DisplayOrder="Western"><GivenName>C.</GivenName>
<FamilyName>Pandu Rangan</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff10"><EditorName DisplayOrder="Western"><GivenName>Bernhard</GivenName>
<FamilyName>Steffen</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff11"><EditorName DisplayOrder="Western"><GivenName>Madhu</GivenName>
<FamilyName>Sudan</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff12"><EditorName DisplayOrder="Western"><GivenName>Demetri</GivenName>
<FamilyName>Terzopoulos</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff13"><EditorName DisplayOrder="Western"><GivenName>Dough</GivenName>
<FamilyName>Tygar</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff14"><EditorName DisplayOrder="Western"><GivenName>Moshe</GivenName>
<GivenName>Y.</GivenName>
<FamilyName>Vardi</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff15"><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName>
<FamilyName>Weikum</FamilyName>
</EditorName>
</Editor>
<Affiliation ID="Aff1"><OrgName>Lancaster University</OrgName>
<OrgAddress><Country>UK</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff2"><OrgName>Carnegie Mellon University</OrgName>
<OrgAddress><City>Pittsburgh</City>
<State>PA</State>
<Country>USA</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff3"><OrgName>University of Surrey</OrgName>
<OrgAddress><City>Guildford</City>
<Country>UK</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff4"><OrgName>Cornell University</OrgName>
<OrgAddress><City>Ithaca</City>
<State>NY</State>
<Country>USA</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff5"><OrgName>ETH Zurich</OrgName>
<OrgAddress><Country>Switzerland</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff6"><OrgName>Stanford University</OrgName>
<OrgAddress><City>CA</City>
<Country>USA</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff7"><OrgName>Weizmann Institute of Science</OrgName>
<OrgAddress><City>Rehovot</City>
<Country>Israel</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff8"><OrgName>University of Bern</OrgName>
<OrgAddress><Country>Switzerland</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff9"><OrgName>Indian Institute of Technology</OrgName>
<OrgAddress><City>Madras</City>
<Country>India</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff10"><OrgName>University of Dortmund</OrgName>
<OrgAddress><Country>Germany</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff11"><OrgName>Massachusetts Institute of Technology</OrgName>
<OrgAddress><City>MA</City>
<Country>USA</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff12"><OrgName>University of California</OrgName>
<OrgAddress><City>Los Angeles</City>
<State>CA</State>
<Country>USA</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff13"><OrgName>University of California</OrgName>
<OrgAddress><City>Berkeley</City>
<State>CA</State>
<Country>USA</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff14"><OrgName>Rice University</OrgName>
<OrgAddress><City>Houston</City>
<State>TX</State>
<Country>USA</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff15"><OrgName>Max-Planck Institute of Computer Science</OrgName>
<OrgAddress><City>Saarbruecken</City>
<Country>Germany</Country>
</OrgAddress>
</Affiliation>
</EditorGroup>
</SeriesHeader>
<Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingDepth="2" NumberingStyle="ContentOnly" OutputMedium="All" TocLevels="0"><BookID>978-3-540-48816-3</BookID>
<BookTitle>Theoretical Aspects of Computing - ICTAC 2006</BookTitle>
<BookSubTitle>Third International Colloquium, Tunis, Tunisia, November 20-24, 2006. Proceedings</BookSubTitle>
<BookVolumeNumber>4281</BookVolumeNumber>
<BookSequenceNumber>4281</BookSequenceNumber>
<BookDOI>10.1007/11921240</BookDOI>
<BookTitleID>142446</BookTitleID>
<BookPrintISBN>978-3-540-48815-6</BookPrintISBN>
<BookElectronicISBN>978-3-540-48816-3</BookElectronicISBN>
<BookChapterCount>26</BookChapterCount>
<BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName>
<CopyrightYear>2006</CopyrightYear>
</BookCopyright>
<BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject>
<BookSubject Code="I16013" Priority="1" Type="Secondary">Computation by Abstract Devices</BookSubject>
<BookSubject Code="I1603X" Priority="2" Type="Secondary">Logics and Meanings of Programs</BookSubject>
<BookSubject Code="I16048" Priority="3" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject>
<BookSubject Code="I14037" Priority="4" Type="Secondary">Programming Languages, Compilers, Interpreters</BookSubject>
<BookSubject Code="I14029" Priority="5" Type="Secondary">Software Engineering</BookSubject>
<BookSubject Code="I13022" Priority="6" Type="Secondary">Computer Communication Networks</BookSubject>
<SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection>
</BookSubjectGroup>
<BookContext><SeriesID>558</SeriesID>
</BookContext>
</BookInfo>
<BookHeader><EditorGroup><Editor AffiliationIDS="Aff16"><EditorName DisplayOrder="Western"><GivenName>Kamel</GivenName>
<FamilyName>Barkaoui</FamilyName>
</EditorName>
<Contact><Email>kamel.barkaoui@cnam.fr</Email>
</Contact>
</Editor>
<Editor AffiliationIDS="Aff17"><EditorName DisplayOrder="Western"><GivenName>Ana</GivenName>
<FamilyName>Cavalcanti</FamilyName>
</EditorName>
<Contact><Email>alcc@cs.york.ac.uk</Email>
</Contact>
</Editor>
<Editor AffiliationIDS="Aff18"><EditorName DisplayOrder="Western"><GivenName>Antonio</GivenName>
<FamilyName>Cerone</FamilyName>
</EditorName>
<Contact><Email>antonio@iist.unu.edu</Email>
</Contact>
</Editor>
<Affiliation ID="Aff16"><OrgName>Laboratoire CEDRIC, Conservatoire National des Arts et Métiers</OrgName>
<OrgAddress><Street>192 rue Saint Martin</Street>
<Postcode>Paris Cedex 03</Postcode>
<Country>France</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff17"><OrgDivision>Department of Computer Science</OrgDivision>
<OrgName>University of York</OrgName>
<OrgAddress><City>York</City>
<Country>UK</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff18"><OrgName>UNU-IIST, Macau SAR</OrgName>
<OrgAddress><Country>China</Country>
</OrgAddress>
</Affiliation>
</EditorGroup>
</BookHeader>
<Part ID="Part8"><PartInfo TocLevels="0"><PartID>8</PartID>
<PartSequenceNumber>8</PartSequenceNumber>
<PartTitle>Tutorials: Extended Abstracts</PartTitle>
<PartChapterCount>2</PartChapterCount>
<PartContext><SeriesID>558</SeriesID>
<BookTitle>Theoretical Aspects of Computing - ICTAC 2006</BookTitle>
</PartContext>
</PartInfo>
<Chapter ID="Chap26" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" NumberingDepth="2" NumberingStyle="ContentOnly" TocLevels="0"><ChapterID>26</ChapterID>
<ChapterDOI>10.1007/11921240_26</ChapterDOI>
<ChapterSequenceNumber>26</ChapterSequenceNumber>
<ChapterTitle Language="En">Decision Procedures for the Formal Analysis of Software</ChapterTitle>
<ChapterFirstPage>366</ChapterFirstPage>
<ChapterLastPage>370</ChapterLastPage>
<ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName>
<CopyrightYear>2006</CopyrightYear>
</ChapterCopyright>
<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>
<PartID>8</PartID>
<BookID>978-3-540-48816-3</BookID>
<BookTitle>Theoretical Aspects of Computing - ICTAC 2006</BookTitle>
</ChapterContext>
</ChapterInfo>
<ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff19"><AuthorName DisplayOrder="Western"><GivenName>David</GivenName>
<FamilyName>Déharbe</FamilyName>
</AuthorName>
<Contact><Email>david@dimap.ufrn.br</Email>
</Contact>
</Author>
<Author AffiliationIDS="Aff20"><AuthorName DisplayOrder="Western"><GivenName>Pascal</GivenName>
<FamilyName>Fontaine</FamilyName>
</AuthorName>
<Contact><Email>fontaine@loria.fr</Email>
</Contact>
</Author>
<Author AffiliationIDS="Aff20 Aff21"><AuthorName DisplayOrder="Western"><GivenName>Silvio</GivenName>
<FamilyName>Ranise</FamilyName>
</AuthorName>
<Contact><Email>ranise@loria.fr</Email>
</Contact>
</Author>
<Author AffiliationIDS="Aff20"><AuthorName DisplayOrder="Western"><GivenName>Christophe</GivenName>
<FamilyName>Ringeissen</FamilyName>
</AuthorName>
<Contact><Email>ringeiss@loria.fr</Email>
</Contact>
</Author>
<Affiliation ID="Aff19"><OrgName>UFRN/DIMAp, Natal</OrgName>
<OrgAddress><Country>Brazil</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff20"><OrgName>LORIA, Nancy</OrgName>
<OrgAddress><Country>France</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff21"><OrgName>Univerisità di Milano</OrgName>
<OrgAddress><Country>Italy</Country>
</OrgAddress>
</Affiliation>
</AuthorGroup>
<Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading>
<Para>Catching bugs in programs is difficult and time-consuming. The effort of debugging and proving correct even small units of code can surpass the effort of programming. Bugs inserted while “programming in the small” can have dramatic consequences for the consistency of a whole software system as shown, e.g., by viruses which can spread by exploiting buffer overflows, a bug which typically arises while coding a small portion of code. To detect this kind of errors, many verification techniques have been put forward such as static analysis and model checking.</Para>
</Abstract>
</ChapterHeader>
<NoBody></NoBody>
</Chapter>
</Part>
</Book>
</Series>
</Publisher>
</istex:document>
</istex:metadataXml>
<mods version="3.6"><titleInfo lang="en"><title>Decision Procedures for the Formal Analysis of Software</title>
</titleInfo>
<titleInfo type="alternative" contentType="CDATA"><title>Decision Procedures for the Formal Analysis of Software</title>
</titleInfo>
<name type="personal"><namePart type="given">David</namePart>
<namePart type="family">Déharbe</namePart>
<affiliation>UFRN/DIMAp, Natal, Brazil</affiliation>
<affiliation>E-mail: david@dimap.ufrn.br</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Pascal</namePart>
<namePart type="family">Fontaine</namePart>
<affiliation>LORIA, Nancy, France</affiliation>
<affiliation>E-mail: fontaine@loria.fr</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Silvio</namePart>
<namePart type="family">Ranise</namePart>
<affiliation>LORIA, Nancy, France</affiliation>
<affiliation>Univerisità di Milano, Italy</affiliation>
<affiliation>E-mail: ranise@loria.fr</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Christophe</namePart>
<namePart type="family">Ringeissen</namePart>
<affiliation>LORIA, Nancy, France</affiliation>
<affiliation>E-mail: ringeiss@loria.fr</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<typeOfResource>text</typeOfResource>
<genre displayLabel="OriginalPaper" 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">2006</dateIssued>
<copyrightDate encoding="w3cdtf">2006</copyrightDate>
</originInfo>
<language><languageTerm type="code" authority="rfc3066">en</languageTerm>
<languageTerm type="code" authority="iso639-2b">eng</languageTerm>
</language>
<abstract lang="en">Abstract: Catching bugs in programs is difficult and time-consuming. The effort of debugging and proving correct even small units of code can surpass the effort of programming. Bugs inserted while “programming in the small” can have dramatic consequences for the consistency of a whole software system as shown, e.g., by viruses which can spread by exploiting buffer overflows, a bug which typically arises while coding a small portion of code. To detect this kind of errors, many verification techniques have been put forward such as static analysis and model checking.</abstract>
<relatedItem type="host"><titleInfo><title>Theoretical Aspects of Computing - ICTAC 2006</title>
<subTitle>Third International Colloquium, Tunis, Tunisia, November 20-24, 2006. Proceedings</subTitle>
</titleInfo>
<name type="personal"><namePart type="given">Kamel</namePart>
<namePart type="family">Barkaoui</namePart>
<affiliation>Laboratoire CEDRIC, Conservatoire National des Arts et Métiers, 192 rue Saint Martin, Paris Cedex 03, France</affiliation>
<affiliation>E-mail: kamel.barkaoui@cnam.fr</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Ana</namePart>
<namePart type="family">Cavalcanti</namePart>
<affiliation>Department of Computer Science, University of York, York, UK</affiliation>
<affiliation>E-mail: alcc@cs.york.ac.uk</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Antonio</namePart>
<namePart type="family">Cerone</namePart>
<affiliation>UNU-IIST, Macau SAR, China</affiliation>
<affiliation>E-mail: antonio@iist.unu.edu</affiliation>
<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">2006</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="I16013">Computation by Abstract Devices</topic>
<topic authority="SpringerSubjectCodes" authorityURI="I1603X">Logics and Meanings of Programs</topic>
<topic authority="SpringerSubjectCodes" authorityURI="I16048">Mathematical Logic and Formal Languages</topic>
<topic authority="SpringerSubjectCodes" authorityURI="I14037">Programming Languages, Compilers, Interpreters</topic>
<topic authority="SpringerSubjectCodes" authorityURI="I14029">Software Engineering</topic>
<topic authority="SpringerSubjectCodes" authorityURI="I13022">Computer Communication Networks</topic>
</subject>
<identifier type="DOI">10.1007/11921240</identifier>
<identifier type="ISBN">978-3-540-48815-6</identifier>
<identifier type="eISBN">978-3-540-48816-3</identifier>
<identifier type="ISSN">0302-9743</identifier>
<identifier type="eISSN">1611-3349</identifier>
<identifier type="BookTitleID">142446</identifier>
<identifier type="BookID">978-3-540-48816-3</identifier>
<identifier type="BookChapterCount">26</identifier>
<identifier type="BookVolumeNumber">4281</identifier>
<identifier type="BookSequenceNumber">4281</identifier>
<identifier type="PartChapterCount">2</identifier>
<part><date>2006</date>
<detail type="part"><title>Tutorials: Extended Abstracts</title>
</detail>
<detail type="volume"><number>4281</number>
<caption>vol.</caption>
</detail>
<extent unit="pages"><start>366</start>
<end>370</end>
</extent>
</part>
<recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2006</recordOrigin>
</recordInfo>
</relatedItem>
<relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title>
</titleInfo>
<name type="personal"><namePart type="given">David</namePart>
<namePart type="family">Hutchison</namePart>
<affiliation>Lancaster University, UK</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Takeo</namePart>
<namePart type="family">Kanade</namePart>
<affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Josef</namePart>
<namePart type="family">Kittler</namePart>
<affiliation>University of Surrey, Guildford, UK</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Jon</namePart>
<namePart type="given">M.</namePart>
<namePart type="family">Kleinberg</namePart>
<affiliation>Cornell University, Ithaca, NY, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Friedemann</namePart>
<namePart type="family">Mattern</namePart>
<affiliation>ETH Zurich, Switzerland</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">John</namePart>
<namePart type="given">C.</namePart>
<namePart type="family">Mitchell</namePart>
<affiliation>Stanford University, CA, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Moni</namePart>
<namePart type="family">Naor</namePart>
<affiliation>Weizmann Institute of Science, Rehovot, Israel</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Oscar</namePart>
<namePart type="family">Nierstrasz</namePart>
<affiliation>University of Bern, Switzerland</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">C.</namePart>
<namePart type="family">Pandu Rangan</namePart>
<affiliation>Indian Institute of Technology, Madras, India</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Bernhard</namePart>
<namePart type="family">Steffen</namePart>
<affiliation>University of Dortmund, Germany</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Madhu</namePart>
<namePart type="family">Sudan</namePart>
<affiliation>Massachusetts Institute of Technology, MA, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Demetri</namePart>
<namePart type="family">Terzopoulos</namePart>
<affiliation>University of California, Los Angeles, CA, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Dough</namePart>
<namePart type="family">Tygar</namePart>
<affiliation>University of California, Berkeley, CA, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Moshe</namePart>
<namePart type="given">Y.</namePart>
<namePart type="family">Vardi</namePart>
<affiliation>Rice University, Houston, TX, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Gerhard</namePart>
<namePart type="family">Weikum</namePart>
<affiliation>Max-Planck Institute of Computer Science, Saarbruecken, Germany</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<originInfo><publisher>Springer</publisher>
<copyrightDate encoding="w3cdtf">2006</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 Berlin Heidelberg, 2006</recordOrigin>
</recordInfo>
</relatedItem>
<identifier type="istex">1249FAC26F49FBD522B1C62A11767C491F01D85D</identifier>
<identifier type="ark">ark:/67375/HCB-C9SH85Z6-K</identifier>
<identifier type="DOI">10.1007/11921240_26</identifier>
<identifier type="ChapterID">26</identifier>
<identifier type="ChapterID">Chap26</identifier>
<accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 2006</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 Berlin Heidelberg, 2006</recordOrigin>
</recordInfo>
</mods>
<json:item><extension>json</extension>
<original>false</original>
<mimetype>application/json</mimetype>
<uri>https://api.istex.fr/ark:/67375/HCB-C9SH85Z6-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 000408 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 000408 | 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:1249FAC26F49FBD522B1C62A11767C491F01D85D
   |texte=   Decision Procedures for the Formal Analysis of Software
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

Decision Procedures for the Formal Analysis of Software

Decision Procedures for the Formal Analysis of Software

Source :

Abstract

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri