Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution

DOI10.1016/J.JSC.2016.07.023MaRDI QIDQ507359zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Jens Knoop, Laura Kovács, Jakob Zwirchmayr

Publication date 6 February 2017

Published in Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:3-3335

zbMATH Keywords

symbolic computationstatic symbolic executionworst-case execution time (WCET) analysis

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Correct Hardware Design and Verification Methods
• Symbolic worst case execution times
• Chronos: A timing analyzer for embedded software
• Refinement of worst-case execution time bounds by graph pruning
• Calculating WCET estimates from timed traces

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1324833 (Why is no real title available?)
• Quantitative abstraction refinement
• Refinement of worst-case execution time bounds by graph pruning
• Scalable and precise refinement of cache timing analysis via path-sensitive verification
• The algorithm design manual

Cited in

(16)

• Calculating WCET estimates from timed traces
• Symbolic worst case execution times
• Correct Hardware Design and Verification Methods
• scientific article; zbMATH DE number 2011465 (Why is no real title available?)
• Scalable and precise refinement of cache timing analysis via path-sensitive verification
• Refinement of worst-case execution time bounds by graph pruning
• scientific article; zbMATH DE number 1760152 (Why is no real title available?)
• Certifying execution time
• Criticality: static profiling for real-time programs
• Computer Aided Verification
• Chronos: A timing analyzer for embedded software
• Realistic Worst-Case Execution Time Analysis in the Context of Pervasive System Verification
• On the modular integration of abstract semantics for WCET analysis
• Symbolic WCET analysis of programs containing input-dependent branches
• Calculation of symbolic running times in embedded real-time systems.
• Bounding the execution time of software in realtime systems

Describes a project that uses

Uses Software

• STP
• OTAWA
• Smacc
• r-TuBound
• Stony Brook
• KLEE
• LLVM
• lp_solve
• Boolector

This page was built for publication: Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution

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