Simplification and Generalization in CIRC

Cite This

Files in this item

Files Size Format View

There are no files associated with this item.

GORIAC, Eugen-Ioan, Georgiana CALTAIS, Dorel LUCANU, 2009. Simplification and Generalization in CIRC. 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC) 2009. Timisoara, Romania, Sep 26, 2009 - Sep 29, 2009. In: 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing 2009. New York, NY:IEEE, pp. 85-92. ISBN 978-1-4244-5910-0. Available under: doi: 10.1109/SYNASC.2009.54

@inproceedings{Goriac2009-09Simpl-46028, title={Simplification and Generalization in CIRC}, year={2009}, doi={10.1109/SYNASC.2009.54}, isbn={978-1-4244-5910-0}, address={New York, NY}, publisher={IEEE}, booktitle={11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing 2009}, pages={85--92}, author={Goriac, Eugen-Ioan and Caltais, Georgiana and Lucanu, Dorel} }

<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/46028"> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dcterms:title>Simplification and Generalization in CIRC</dcterms:title> <dc:creator>Caltais, Georgiana</dc:creator> <dc:creator>Goriac, Eugen-Ioan</dc:creator> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/46028"/> <dc:contributor>Goriac, Eugen-Ioan</dc:contributor> <dcterms:abstract xml:lang="eng">CIRC is an automated theorem prover based on the circular coinduction principle. The tool is used for the verification of programs, behavioral equivalence checking, and proving properties over infinite data structures. In this paper we present two extensions of CIRC that handle the case when the prover indicates an infinite execution for a certain goal. The first extension involves goal simplification rules and a procedure for checking that the new execution is indeed a proof, while the second one refers to finding and proving a generalization of the goal. Each of the extensions is presented based on a case study: Binary Process Algebra (BPA) for checking the proof correctness and Streams for using generalization.</dcterms:abstract> <dc:language>eng</dc:language> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dc:creator>Lucanu, Dorel</dc:creator> <dcterms:issued>2009-09</dcterms:issued> <dc:contributor>Caltais, Georgiana</dc:contributor> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2019-06-18T09:51:43Z</dc:date> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2019-06-18T09:51:43Z</dcterms:available> <dc:contributor>Lucanu, Dorel</dc:contributor> </rdf:Description> </rdf:RDF>

This item appears in the following Collection(s)

Search KOPS


Browse

My Account