Affine Disjunctive Invariant Generation with Farkas' Lemma
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2023
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866929597268885504 |
|---|---|
| author | Ke, Jingyu Fu, Hongfei Liu, Hongming Sun, Zhouyue Chen, Liqian Li, Guoqiang |
| author_facet | Ke, Jingyu Fu, Hongfei Liu, Hongming Sun, Zhouyue Chen, Liqian Li, Guoqiang |
| contents | In the verification of loop programs, disjunctive invariants are essential to capture complex loop dynamics such as phase and mode changes. In this work, we develop a novel approach for the automated generation of affine disjunctive invariants for affine while loops via Farkas' Lemma, a fundamental theorem on linear inequalities. Our main contributions are two-fold. First, we combine Farkas' Lemma with a succinct control flow transformation to derive disjunctive invariants from the conditional branches in the loop. Second, we propose an invariant propagation technique that minimizes the invariant computation effort by propagating previously solved invariants to yet unsolved locations as much as possible. Furthermore, we resolve the infeasibility checking in the application of Farkas' Lemma which has not been addressed previously, and extend our approach to nested loops via loop summary. Experimental evaluation over more than 100 affine while loops (mostly from SV-COMP 2023) demonstrates that our approach is promising to generate tight linear invariants over affine programs. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2307_13318 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Affine Disjunctive Invariant Generation with Farkas' Lemma Ke, Jingyu Fu, Hongfei Liu, Hongming Sun, Zhouyue Chen, Liqian Li, Guoqiang Logic in Computer Science In the verification of loop programs, disjunctive invariants are essential to capture complex loop dynamics such as phase and mode changes. In this work, we develop a novel approach for the automated generation of affine disjunctive invariants for affine while loops via Farkas' Lemma, a fundamental theorem on linear inequalities. Our main contributions are two-fold. First, we combine Farkas' Lemma with a succinct control flow transformation to derive disjunctive invariants from the conditional branches in the loop. Second, we propose an invariant propagation technique that minimizes the invariant computation effort by propagating previously solved invariants to yet unsolved locations as much as possible. Furthermore, we resolve the infeasibility checking in the application of Farkas' Lemma which has not been addressed previously, and extend our approach to nested loops via loop summary. Experimental evaluation over more than 100 affine while loops (mostly from SV-COMP 2023) demonstrates that our approach is promising to generate tight linear invariants over affine programs. |
| title | Affine Disjunctive Invariant Generation with Farkas' Lemma |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2307.13318 |