Mostrar el registro sencillo del ítem

dc.contributor.authorBagnara, Roberto
dc.contributor.authorRodríguez Carbonell, Enric
dc.contributor.authorZaffanella, Enea
dc.contributor.otherUniversitat Politècnica de Catalunya. Departament de Llenguatges i Sistemes Informàtics
dc.date.accessioned2016-03-11T09:35:06Z
dc.date.available2016-03-11T09:35:06Z
dc.date.issued2005-04
dc.identifier.citationBagnara, R., Rodríguez, E., Zaffanella, E. "Generation of basic semi-algebraic invariants using convex polyhedra". 2005.
dc.identifier.urihttp://hdl.handle.net/2117/84194
dc.description.abstractA technique for generating invariant polynomial inequalities of bounded degree is presented using the abstract interpretation framework. It is based on overapproximating basic semi-algebraic sets, i.e., sets defined by conjunctions of polynomial inequalities, by means of convex polyhedra. While improving on the existing methods for generating invariant polynomial equalities, since polynomial inequalities are allowed in the guards of the transition system, the approach does not suffer from the prohibitive complexity of methods based on quantifier-elimination. The application of our implementation to benchmark programs shows that the method produces non-trivial invariants in reasonable time. In some cases the generated invariants are essential to verify safety properties that cannot be proved with just classical linear invariants.
dc.format.extent20 p.
dc.language.isoeng
dc.relation.ispartofseriesLSI-05-14-R
dc.subjectÀrees temàtiques de la UPC::Informàtica::Informàtica teòrica
dc.subject.otherPolynomial inequalities
dc.subject.otherConvex polyhedra
dc.titleGeneration of basic semi-algebraic invariants using convex polyhedra
dc.typeExternal research report
dc.rights.accessOpen Access
drac.iddocument1876931
dc.description.versionPostprint (published version)
upcommons.citation.authorBagnara, R.; Rodríguez, E.; Zaffanella, E.
upcommons.citation.publishedtrue


Ficheros en el ítem

Thumbnail

Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro sencillo del ítem

Todos los derechos reservados.Esta obra está protegida por los derechos de propiedad intelectual e industrial. Sin perjuicio de las exenciones legales existentes, queda prohibida su reproducción, distribución, comunicación pública o transformación sin la autorización del titular de los derechos