Symbolic Loop Bound Computation for WCET Analysis

DOI10.1007/978-3-642-29709-0_20MaRDI QIDQ3457981zbMATH OpenOpenAlexFDO

Authors Jens Knoop, Laura Kovács, Jakob Zwirchmayr

Publication date 7 December 2015

Published in Perspectives of Systems Informatics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-29709-0_20

Mathematics Subject Classification ID

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

Recommendations

• Computing exact loop bounds for bounded program verification
• Efficient loop navigation for symbolic execution
• Symbolic WCET analysis of programs containing input-dependent branches
• Symbolic termination analysis of solvable loops
• Loop invariant symbolic execution for parallel programs
• Control flow refinement and symbolic computation of average case bound
• ABC: algebraic bound computation for loops

Cited in

(7)

• Lower-bound synthesis using loop specialization and Max-SMT
• ABC: algebraic bound computation for loops
• Probabilistic output analysis by program manipulation
• Regular path clauses and their application in solving loops
• Symbolic WCET analysis of programs containing input-dependent branches
• Control flow refinement and symbolic computation of average case bound
• Computing exact loop bounds for bounded program verification

This page was built for publication: Symbolic Loop Bound Computation for WCET Analysis

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