Retrograde Program Analysis: A Practical Tutorial
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2010
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866912660950351872 |
|---|---|
| author | Perisic, Aleksandar |
| author_facet | Perisic, Aleksandar |
| contents | Retrograde analysis reads programs from the end to the beginning: treat statements as constraints on prior states, propagate sets of states backward, and compare the reachable inputs with the intended specification. This tutorial condenses a longer exposition to a focused guide with definitions, worked examples (toy branches, sorting networks, binary search), loop treatment via fixpoints, and a range-algebra appendix that standardizes array splits and midpoints. The aim is practical: short proofs, concrete invariants, and drop-in code and property tests |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_1006_2534 |
| institution | arXiv |
| publishDate | 2010 |
| record_format | arxiv |
| spellingShingle | Retrograde Program Analysis: A Practical Tutorial Perisic, Aleksandar Software Engineering Retrograde analysis reads programs from the end to the beginning: treat statements as constraints on prior states, propagate sets of states backward, and compare the reachable inputs with the intended specification. This tutorial condenses a longer exposition to a focused guide with definitions, worked examples (toy branches, sorting networks, binary search), loop treatment via fixpoints, and a range-algebra appendix that standardizes array splits and midpoints. The aim is practical: short proofs, concrete invariants, and drop-in code and property tests |
| title | Retrograde Program Analysis: A Practical Tutorial |
| topic | Software Engineering |
| url | https://arxiv.org/abs/1006.2534 |