2014 | OriginalPaper | Buchkapitel
Proving Termination of Programs Automatically with AProVE
verfasst von : Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, René Thiemann
Erschienen in: Automated Reasoning
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.