<div class="csl-bib-body">
<div class="csl-entry">Ait El Manssour, R., Kenison, G. J., Shirmohammadi, M., & Varonka, A. (2024, September 19). <i>Simple Linear Loops: Algebraic Invariants and Synthesis</i> [Presentation]. 18th International Conference on Reachability Problems (RP 2024), Wien, Austria. https://doi.org/10.1007/978-3-031-72621-7</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/210457
-
dc.description.abstract
Many challenges of fully automated verification of recursive programs are rooted in the hardness of generating appropriate invariants (relations among variables that hold throughout program execution). This work focuses on algebraic invariants of simple linear loops (branch-free loop programs with a single linear update). Whilst this model is elementary, even the most natural verification problems (such as termination and reachability) are arguably difficult in this setting, see Ouaknine and Worrell, https://doi.org/10.1145/2766189.2766191. As a crucial step to understanding possible relations among variables of a simple linear loop, we present a polynomial-space algorithm to compute a representation of the strongest algebraic invariant of a given loop. This set comprises all invariant polynomial equalities. We further discuss the complexity of verifying whether a given algebraic relation, that is, a collection of polynomial equalities in loop variables, is a loop invariant. Finally, we turn to synthesising simple linear loops from desired relations. Specifically, we ask whether there exists a simple linear loop that possesses a given algebraic invariant. Notably, this problem is as hard as Hilbert's Tenth Problem and thus undecidable over the integers, while decidability is open over the rationals. To this end, we explore the complexity landscape for bit-bounded loop synthesis, where the bound on the number of bits used to describe the loop is an input parameter. We show that this problem admits a polynomial-space algorithm.
The material in this presentation is based on the work undertaken in https://arxiv.org/abs/2407.09154.
en
dc.description.sponsorship
European Commission
-
dc.description.sponsorship
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
-
dc.language.iso
en
-
dc.subject
algebraic invariant
en
dc.subject
program synthesis
en
dc.subject
loop invariant
en
dc.subject
Zariski closure
en
dc.subject
polynomial space
en
dc.subject
algebraic reasoning
en
dc.title
Simple Linear Loops: Algebraic Invariants and Synthesis
en
dc.type
Presentation
en
dc.type
Vortrag
de
dc.relation.grantno
ERC Consolidator Grant 2020
-
dc.relation.grantno
ICT19-018
-
dc.type.category
Presentation
-
tuw.project.title
Automated Reasoning with Theories and Induction for Software Technologies
-
tuw.project.title
LogiCs-Stipendien
-
tuw.project.title
Distribution Recovery for Invariant Generation of Probabilistic Programs
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
tuw.publication.orgunit
E056-13 - Fachbereich LogiCS
-
tuw.publisher.doi
10.1007/978-3-031-72621-7
-
tuw.author.orcid
0000-0001-6228-9071
-
tuw.author.orcid
0000-0002-7661-7061
-
tuw.author.orcid
0000-0002-7779-2339
-
tuw.author.orcid
0000-0001-5758-0657
-
tuw.event.name
18th International Conference on Reachability Problems (RP 2024)
en
dc.description.sponsorshipexternal
UKRI Frontier Research Grant
-
dc.relation.grantnoexternal
EP/X033813/1
-
tuw.event.startdate
25-09-2024
-
tuw.event.enddate
27-09-2024
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Wien
-
tuw.event.country
AT
-
tuw.event.institution
TU Wien, Paris Lodron University of Salzburg, Wolfgang Pauli Institute
-
tuw.event.presenter
Varonka, Anton
-
tuw.event.track
Single Track
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
80
-
wb.sciencebranch.value
20
-
item.openairecristype
http://purl.org/coar/resource_type/R60J-J5BD
-
item.cerifentitytype
Publications
-
item.languageiso639-1
en
-
item.fulltext
no Fulltext
-
item.openairetype
conference presentation
-
item.grantfulltext
none
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.orcid
0000-0001-6228-9071
-
crisitem.author.orcid
0000-0002-7661-7061
-
crisitem.author.orcid
0000-0002-7779-2339
-
crisitem.author.orcid
0000-0001-5758-0657
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.project.funder
European Commission
-
crisitem.project.funder
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
