Publikation:

Simplification and Generalization in CIRC

Vorschaubild

Dateien

Zu diesem Dokument gibt es keine Dateien.

Datum

2009

Autor:innen

Goriac, Eugen-Ioan
Lucanu, Dorel

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/SYNASC.2009.54
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

11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing 2009. New York, NY: IEEE, 2009, pp. 85-92. ISBN 978-1-4244-5910-0. Available under: doi: 10.1109/SYNASC.2009.54

Zusammenfassung

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.

Zusammenfassung in einer weiteren Sprache

Fachgebiet (DDC)
004 Informatik

Schlagwörter

Konferenz

11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC) 2009, 26. Sept. 2009 - 29. Sept. 2009, Timisoara, Romania
Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

ISO 690GORIAC, 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, 26. Sept. 2009 - 29. Sept. 2009. In: 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing 2009. New York, NY: IEEE, 2009, pp. 85-92. ISBN 978-1-4244-5910-0. Available under: doi: 10.1109/SYNASC.2009.54
BibTex
@inproceedings{Goriac2009-09Simpl-46028,
  year={2009},
  doi={10.1109/SYNASC.2009.54},
  title={Simplification and Generalization in CIRC},
  isbn={978-1-4244-5910-0},
  publisher={IEEE},
  address={New York, NY},
  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: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/46028">
    <dc:creator>Lucanu, Dorel</dc:creator>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2019-06-18T09:51:43Z</dcterms:available>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2019-06-18T09:51:43Z</dc:date>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/46028"/>
    <dc:creator>Goriac, Eugen-Ioan</dc:creator>
    <dc:contributor>Lucanu, Dorel</dc:contributor>
    <dc:language>eng</dc:language>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dcterms:issued>2009-09</dcterms:issued>
    <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>
    <dcterms:title>Simplification and Generalization in CIRC</dcterms:title>
    <dc:creator>Caltais, Georgiana</dc:creator>
    <dc:contributor>Caltais, Georgiana</dc:contributor>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
  </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