Lower-bound synthesis using loop specialization and Max-SMT

DOI10.1007/978-3-030-81688-9_40MaRDI QIDQ832313zbMATH OpenOpenAlexFDO

Authors Elvira Albert, Samir Genaim, Enrique Martin-Martin, Alicia Merayo, Albert Rubio

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-81688-9_40

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Lower runtime bounds for integer programs
• On the inference of resource usage upper and lower bounds
• Symbolic Loop Bound Computation for WCET Analysis
• CONCUR 2005 – Concurrency Theory
• Synthesis with asymptotic resource bounds

Cites work

• scientific article; zbMATH DE number 4089320 (Why is no real title available?)
• A New Algorithm for Identifying Loops in Decompilation
• A calculus for modular loop acceleration
• Automated termination analysis of Java bytecode by term rewriting
• Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis
• Automatic Static Cost Analysis for Parallel Programs
• Complexity and resource bound analysis of imperative programs using difference constraints
• Computer Aided Verification
• Lower runtime bounds for integer programs
• Mechanical program analysis
• On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems
• On the inference of resource usage upper and lower bounds

Cited in

(2)

• Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)
• Lower runtime bounds for integer programs

Describes a project that uses

Uses Software

• z3
• LoAT

This page was built for publication: Lower-bound synthesis using loop specialization and Max-SMT

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832313)