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

DOI10.1016/j.jsc.2016.07.023zbMath1356.68041OpenAlexW2504411393WikidataQ55670515 ScholiaQ55670515MaRDI QIDQ507359

Laura Kovács, Jakob Zwirchmayr, Jens Knoop

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)

Uses Software

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

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item