Analyzing Program Termination and Complexity Automatically with AProVE
- Submitting institution
-
Birkbeck College
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 161
- Type
- D - Journal article
- DOI
-
10.1007/s10817-016-9388-y
- Title of journal
- Journal of Automated Reasoning
- Article number
- -
- First page
- 3-31
- Volume
- 58
- Issue
- 1
- ISSN
- 0168-7433
- Open access status
- Compliant
- Month of publication
- October
- Year of publication
- 2016
- URL
-
http://eprints.bbk.ac.uk/id/eprint/16551/
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
12
- Research group(s)
-
1 - Algorithms, Verification and Software
- Citation count
- 24
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- AProVE <http://aprove.informatik.rwth-aachen.de/> is a world-leading tool for automatic analysis of termination and worst-case time complexity bounds of programs and term rewrite systems. Won two Kurt Goedel medals at FLoC Olympic Games'2014. Was among the strongest tools at the International Termination and Complexity Competition <http://termination-portal.org/wiki/Termination_Competition> and the termination category of the International Competition on Software Verification <https://sv-comp.sosy-lab.org/>. Implementation platform for many publications <http://aprove.informatik.rwth-aachen.de/index.asp?subform=references.html>. AProVE's analysis outputs include formal proofs. Significant parts of these proofs can be verified independently by trusted proof checking tools based on formalisations in proof assistants (Isabelle, Coq). The earlier conference version IJCAR'14 has another 88+ GS citations.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -