Analyzing program termination and complexity automatically with \textsf{AProVE}

From MaRDI portal
Revision as of 10:04, 6 March 2024 by Import240305080351 (talk | contribs) (Created automatically from import240305080351)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

Publication:2362493

DOI10.1007/S10817-016-9388-YzbMath1409.68255OpenAlexW2533836568MaRDI QIDQ2362493

Stephanie Swiderski, René Thiemann, Carsten Fuhs, Jürgen Giesl, Jera Hensel, Florian Frohn, Marc Brockschmidt, Fabian Emmes, Carsten Otto, Cornelius Aschermann, Martin Plücker, Thomas Ströder, Peter Schneider-Kamp

Publication date: 10 July 2017

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-016-9388-y




Related Items (27)

ATLAS: automated amortised complexity analysis of self-adjusting data structuresPorous invariantsLoop detection by logically constrained term rewritingTermination and complexity analysis for programs with bitvector arithmetic by symbolic executionLower bounds for runtime complexity of term rewritingAnalyzing Innermost Runtime Complexity Through Tuple InterpretationsSemantically-guided goal-sensitive reasoning: decision procedures and the Koala proverAnalysing parallel complexity of term rewritingUnnamed ItemAutomated termination analysis of polynomial probabilistic programsProving Termination Through Conditional TerminationA Perron-Frobenius theorem for deciding matrix growthAn automated approach to the Collatz conjectureUnnamed ItemNon-termination in Term Rewriting and Logic ProgrammingFrom LCF to Isabelle/HOLExtended Nested Dual System Groups, RevisitedConstant runtime complexity of term rewriting is semi-decidableExplaining safety failures in NetKATApplications and extensions of context-sensitive rewritingInferring expected runtimes of probabilistic integer programs using expected sizesAProVEDerivational complexity and context-sensitive RewritingConditions for confluence of innermost terminating term rewriting systemsTuple interpretations for termination of term rewritingType-based analysis of logarithmic amortised complexityRuntime complexity analysis of logically constrained rewriting


Uses Software



Cites Work




This page was built for publication: Analyzing program termination and complexity automatically with \textsf{AProVE}