Giesl, J;
Brockschmidt, M;
Emmes, F;
Frohn, F;
Fuhs, C;
Otto, C;
Plücker, M;
... Thiemann, R; + view all
(2014)
Proving Termination of Programs Automatically with AProVE.
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. 184 - 191).
Springer International Publishing
![[thumbnail of IJCAR14-aprove-tool.pdf]](https://discovery.ucl.ac.uk/style/images/fileicons/application_pdf.png) Preview |
PDF
IJCAR14-aprove-tool.pdf Available under License : See the attached licence file. Download (441kB) |
Abstract
AProVE is a system for automatic termination and complexity proofs of Java, C, Haskell, Prolog, and term rewrite systems (TRSs). To analyze programs in high-level languages, AProVE automatically converts them to TRSs. Then, a wide range of techniques is employed to prove termination and to infer complexity bounds for the resulting TRSs. The generated proofs can be exported to check their correctness using automatic certifiers. For use in software construction, we present an AProVE plug-in for the popular Eclipse software development environment.
| Type: | Proceedings paper |
|---|---|
| Title: | Proving Termination of Programs Automatically with AProVE |
| 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_13 |
| Publisher version: | http://dx.doi.org/10.1007/978-3-319-08587-6_13 |
| 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_13 |
| 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/1455009 |
Archive Staff Only
 |
View Item |
