Lower-bound synthesis using loop specialization and Max-SMT

DOI10.1007/978-3-030-81688-9_40zbMATH Open1493.68098OpenAlexW3183759032MaRDI QIDQ832313FDOQ832313

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

Publication date: 25 March 2022

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

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

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)

Cites Work

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

Cited In (2)

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

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)