A Calculus for Modular Loop Acceleration

DOI10.1007/978-3-030-45190-5_4OpenAlexW3023362447MaRDI QIDQ5039502

Florian Frohn

Publication date: 13 October 2022

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2001.01516

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (3)

Lower-bound synthesis using loop specialization and Max-SMT ⋮ Backward symbolic execution with loop folding ⋮ Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)

Uses Software

• FLATA
• z3
• PURRS
• Princess
• StarExec
• Eldarica
• TPDB
• FAST
• LoAT

Cites Work

• Under-approximating loops in C programs for fast counterexample detection
• On iterating linear transformations over recognizable sets of integers
• Termination of polynomial loops
• PTIME computation of transitive closures of octagonal relations
• Lower Runtime Bounds for Integer Programs
• Proving non-termination
• Fast Acceleration of Ultimately Periodic Relations
• Combining Widening and Acceleration in Linear Relation Analysis
• Iterating Octagons
• Accelerating Interpolants
• Underapproximation of Procedure Summaries for Integer Programs
• On Termination of Integer Linear Loops
• Abstract acceleration of general linear loops
• Automated Technology for Verification and Analysis
• Deciding Conditional Termination

This page was built for publication: A Calculus for Modular Loop Acceleration