Publikation:

Automated Proving of the Behavioral Attributes

Vorschaubild

Dateien

Zu diesem Dokument gibt es keine Dateien.

Datum

2009

Autor:innen

Grigoras, Gheorghe
Lucanu, Dorel
Goriac, Eugen-Ioan

Herausgeber:innen

Kontakt

ISSN der Zeitschrift

Electronic ISSN

ISBN

Bibliografische Daten

Verlag

Schriftenreihe

Auflagebezeichnung

URI (zitierfähiger Link)
DOI (zitierfähiger Link)
https://doi.org/10.1109/BCI.2009.40
ArXiv-ID

Internationale Patentnummer

Angaben zur Forschungsförderung

Projekt

Open Access-Veröffentlichung

Sammlungen

Informatik und Informationswissenschaft: Publikationen
Core Facility der Universität Konstanz

Gesperrt bis

Titel in einer weiteren Sprache

Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published

Erschienen in

Fourth Balkan Conference in Informatics 2009. New York, NY: IEEE, 2009, pp. 33-38. ISBN 978-0-7695-3783-2. Available under: doi: 10.1109/BCI.2009.40

Zusammenfassung

Behavioral equivalence is indistinguishably under experiments: two elements are behavioral equivalent iff each experiment returns the same value for the two elements. Behavioral equivalence can be proved by coinduction. CIRC is a theorem prover which implements circular coinduction, an efficient coinductive technique. Equational attributes refer properties like associativity, commutativity, unity, etc. If these attributes are behaviorally satisfied, then we refer them as behavioral attributes. Two problems regarding these properties are important: expressing the commutativity as a rewrite rule leads to non-termination and their use as attributes requires a careful handling in the proving process. In this paper we present how these attributes are automatically checked in CIRC and we prove that this extension is sound.

Zusammenfassung in einer weiteren Sprache

Fachgebiet (DDC)
004 Informatik

Schlagwörter

Konferenz

Fourth Balkan Conference in Informatics 2009, 17. Sept. 2009 - 19. Sept. 2009, Thessaloniki, Greece
Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

ISO 690GRIGORAS, Gheorghe, Dorel LUCANU, Georgiana CALTAIS, Eugen-Ioan GORIAC, 2009. Automated Proving of the Behavioral Attributes. Fourth Balkan Conference in Informatics 2009. Thessaloniki, Greece, 17. Sept. 2009 - 19. Sept. 2009. In: Fourth Balkan Conference in Informatics 2009. New York, NY: IEEE, 2009, pp. 33-38. ISBN 978-0-7695-3783-2. Available under: doi: 10.1109/BCI.2009.40
BibTex
@inproceedings{Grigoras2009-09Autom-46032,
  year={2009},
  doi={10.1109/BCI.2009.40},
  title={Automated Proving of the Behavioral Attributes},
  isbn={978-0-7695-3783-2},
  publisher={IEEE},
  address={New York, NY},
  booktitle={Fourth Balkan Conference in Informatics 2009},
  pages={33--38},
  author={Grigoras, Gheorghe and Lucanu, Dorel and Caltais, Georgiana and Goriac, Eugen-Ioan}
}
RDF
<rdf:RDF
    xmlns:dcterms="http://purl.org/dc/terms/"
    xmlns:dc="http://purl.org/dc/elements/1.1/"
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:bibo="http://purl.org/ontology/bibo/"
    xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#"
    xmlns:foaf="http://xmlns.com/foaf/0.1/"
    xmlns:void="http://rdfs.org/ns/void#"
    xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > 
  <rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/46032">
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:contributor>Goriac, Eugen-Ioan</dc:contributor>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dcterms:abstract xml:lang="eng">Behavioral equivalence is indistinguishably under experiments: two elements are behavioral equivalent iff each experiment returns the same value for the two elements. Behavioral equivalence can be proved by coinduction. CIRC is a theorem prover which implements circular coinduction, an efficient coinductive technique. Equational attributes refer properties like associativity, commutativity, unity, etc. If these attributes are behaviorally satisfied, then we refer them as behavioral attributes. Two problems regarding these properties are important: expressing the commutativity as a rewrite rule leads to non-termination and their use as attributes requires a careful handling in the proving process. In this paper we present how these attributes are automatically checked in CIRC and we prove that this extension is sound.</dcterms:abstract>
    <dc:contributor>Grigoras, Gheorghe</dc:contributor>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2019-06-18T11:31:02Z</dcterms:available>
    <dc:language>eng</dc:language>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:creator>Lucanu, Dorel</dc:creator>
    <dc:contributor>Caltais, Georgiana</dc:contributor>
    <dcterms:issued>2009-09</dcterms:issued>
    <dc:creator>Caltais, Georgiana</dc:creator>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2019-06-18T11:31:02Z</dc:date>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/46032"/>
    <dc:contributor>Lucanu, Dorel</dc:contributor>
    <dc:creator>Goriac, Eugen-Ioan</dc:creator>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:creator>Grigoras, Gheorghe</dc:creator>
    <dcterms:title>Automated Proving of the Behavioral Attributes</dcterms:title>
  </rdf:Description>
</rdf:RDF>

Interner Vermerk

xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter

Kontakt
URL der Originalveröffentl.

Prüfdatum der URL

Prüfungsdatum der Dissertation

Finanzierungsart

Kommentar zur Publikation

Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Nein
Begutachtet
Diese Publikation teilen