Lower-bound synthesis using loop specialization and Max-SMT

DOI10.1007/978-3-030-81688-9_40zbMath1493.68098OpenAlexW3183759032MaRDI QIDQ832313

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

Publication date: 25 March 2022

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

Mathematics Subject Classification ID

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

Related Items (1)

Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)

Uses Software

• z3
• LoAT

Cites Work

• Unnamed Item
• On automation of \(\mathsf{CTL}^*\) verification for infinite-state systems
• 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
• Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis
• A New Algorithm for Identifying Loops in Decompilation
• Mechanical program analysis
• A Calculus for Modular Loop Acceleration
• Automated Termination Analysis of Java Bytecode by Term Rewriting
• Computer Aided Verification

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