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

DOI10.1016/J.JSC.2016.07.023zbMATH Open1356.68041DBLPjournals/jsc/KnoopKZ17OpenAlexW2504411393WikidataQ55670515 ScholiaQ55670515MaRDI QIDQ507359FDOQ507359

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

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

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)

Cites Work

• The algorithm design manual
• Title not available (Why is that?)
• Title not available (Why is that?)
• Scalable and precise refinement of cache timing analysis via path-sensitive verification
• Refinement of worst-case execution time bounds by graph pruning
• Quantitative abstraction refinement

Cited In (16)

• Calculating WCET estimates from timed traces
• Symbolic worst case execution times
• Correct Hardware Design and Verification Methods
• Title not available (Why is that?)
• Scalable and precise refinement of cache timing analysis via path-sensitive verification
• Refinement of worst-case execution time bounds by graph pruning
• Title not available (Why is that?)
• Certifying execution time
• Computer Aided Verification
• Criticality: static profiling for real-time programs
• 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

Uses Software

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

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)