Ströder, T;
Giesl, J;
Brockschmidt, M;
Frohn, F;
Fuhs, C;
Hensel, J;
Schneider-Kamp, P;
(2014)
Proving Termination and Memory Safety for Programs with Pointer Arithmetic.
In: Demri, S and Kapur, D and Weidenbach, C, (eds.)
Automated Reasoning: 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings.
(pp. 208 - 223).
Springer International Publishing
![[thumbnail of IJCAR14-llvm-pointer.pdf]](https://discovery.ucl.ac.uk/style/images/fileicons/application_pdf.png) Preview |
PDF
IJCAR14-llvm-pointer.pdf Available under License : See the attached licence file. Download (470kB) |
Abstract
Proving termination automatically for programs with explicit pointer arithmetic is still an open problem. To close this gap, we introduce a novel abstract domain that can track allocated memory in detail. We use it to automatically construct a symbolic execution graph that represents all possible runs of the program and that can be used to prove memory safety. This graph is then transformed into an integer transition system, whose termination can be proved by standard techniques. We implemented this approach in the automated termination prover AProVE and demonstrate its capability of analyzing C programs with pointer arithmetic that existing tools cannot handle.
| Type: | Proceedings paper |
|---|---|
| Title: | Proving Termination and Memory Safety for Programs with Pointer Arithmetic |
| Event: | 7th International Joint Conference, IJCAR 2014 |
| ISBN-13: | 978-3-319-08586-9 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-319-08587-6_15 |
| Publisher version: | http://dx.doi.org/10.1007/978-3-319-08587-6_15 |
| Language: | English |
| Additional information: | This is the authors' accepted version of this published conference paper. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-08587-6_15 |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/1455008 |
Loading...
Loading...Loading...Loading...Archive Staff Only
 |
View Item |
