Automated Proving of the Behavioral Attributes

Cite This

Files in this item

Files Size Format View

There are no files associated with this item.

GRIGORAS, Gheorghe, Dorel LUCANU, Georgiana CALTAIS, Eugen-Ioan GORIAC, 2009. Automated Proving of the Behavioral Attributes. Fourth Balkan Conference in Informatics 2009. Thessaloniki, Greece, Sep 17, 2009 - Sep 19, 2009. In: Fourth Balkan Conference in Informatics 2009. New York, NY:IEEE, pp. 33-38. ISBN 978-0-7695-3783-2. Available under: doi: 10.1109/BCI.2009.40

@inproceedings{Grigoras2009-09Autom-46032, title={Automated Proving of the Behavioral Attributes}, year={2009}, doi={10.1109/BCI.2009.40}, isbn={978-0-7695-3783-2}, address={New York, NY}, publisher={IEEE}, 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 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/rdf/resource/123456789/46032"> <dc:contributor>Lucanu, Dorel</dc:contributor> <dc:creator>Lucanu, Dorel</dc:creator> <dc:creator>Caltais, Georgiana</dc:creator> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <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> <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/46032"/> <dc:language>eng</dc:language> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dc:contributor>Caltais, Georgiana</dc:contributor> <dc:creator>Goriac, Eugen-Ioan</dc:creator> <dc:creator>Grigoras, Gheorghe</dc:creator> <dcterms:issued>2009-09</dcterms:issued> <dc:contributor>Grigoras, Gheorghe</dc:contributor> <dcterms:title>Automated Proving of the Behavioral Attributes</dcterms:title> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2019-06-18T11:31:02Z</dcterms:available> <dc:contributor>Goriac, Eugen-Ioan</dc:contributor> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2019-06-18T11:31:02Z</dc:date> </rdf:Description> </rdf:RDF>

This item appears in the following Collection(s)

Search KOPS


Browse

My Account