Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs

DOI10.1007/978-3-642-15769-1_8zbMath1306.68017OpenAlexW1523037784MaRDI QIDQ4930721

Alain Darte, Christophe Alias, Paul Feautrier, Laure Gonnord

Publication date: 1 October 2010

Published in: Static Analysis (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/inria-00523298

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Analyzing program termination and complexity automatically with \textsf{AProVE}, A combination framework for complexity, Constraint-based relational verification, Learning probabilistic termination proofs, Decision tree learning in CEGIS-based termination analysis, Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution, Complexity and resource bound analysis of imperative programs using difference constraints, Rely-guarantee termination and cost analyses of loops with concurrent interleavings, Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis, Type-based amortized resource analysis with integers and arrays, Proving Termination Through Conditional Termination, Analysis of Executable Software Models, More Precise Yet Widely Applicable Cost Analysis, Inferring expected runtimes of probabilistic integer programs using expected sizes, Unnamed Item, Lower Runtime Bounds for Integer Programs, Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free, Ranking Functions for Linear-Constraint Loops, A new order-theoretic characterisation of the polytime computable functions, Type-based analysis of logarithmic amortised complexity

Uses Software

• Aspic
• SPEED
• aiT