Volume
OASIcs, Volume 47
15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)
-
Part of:
Series:
Open Access Series in Informatics (OASIcs)
Conference: Workshop on Worst-Case Execution Time Analysis (WCET)
Event
WCET 2015, July 7, 2015, Lund, SwedenEditor
Publication Details
- published at: 2015-07-06
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- ISBN: 978-3-939897-95-8
- DBLP: db/conf/wcet/wcet2015
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Volume
OASIcs, Volume 47, WCET'15, Complete Volume
Abstract
OASIcs, Volume 47, WCET'15, Complete Volume
Cite as
15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015). Open Access Series in Informatics (OASIcs), Volume 47, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@Proceedings{cazorla:OASIcs.WCET.2015,
title = {{OASIcs, Volume 47, WCET'15, Complete Volume}},
booktitle = {15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-95-8},
ISSN = {2190-6807},
year = {2015},
volume = {47},
editor = {Cazorla, Francisco J.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2015},
URN = {urn:nbn:de:0030-drops-52652},
doi = {10.4230/OASIcs.WCET.2015},
annote = {Keywords: Performance Analysis and Design Aids – Worst-case Analysis, Performance Analysis and Design Aids, Software/Program Verification, Testing and Debugging Special-Purpose and Application-Based Systems – Real-Time and Embedded Systems, Performance of Systems, Computers in other systems – Real time, Real t}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Workshop Organization
Abstract
Front Matter, Table of Contents, Preface, Workshop Organization
Cite as
15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015). Open Access Series in Informatics (OASIcs), Volume 47, pp. i-xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{cazorla:OASIcs.WCET.2015.i,
author = {Cazorla, Francisco J.},
title = {{Front Matter, Table of Contents, Preface, Workshop Organization}},
booktitle = {15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)},
pages = {i--xiv},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-95-8},
ISSN = {2190-6807},
year = {2015},
volume = {47},
editor = {Cazorla, Francisco J.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2015.i},
URN = {urn:nbn:de:0030-drops-52501},
doi = {10.4230/OASIcs.WCET.2015.i},
annote = {Keywords: Front Matter, Table of Contents, Preface, Workshop Organization}
}
Document
A Framework to Quantify the Overestimations of Static WCET Analysis
Abstract
To reduce complexity while computing an upper bound on the worst-case execution time, static WCET analysis performs over-approximations. This feeds the general feeling that static WCET estimations can be far above the real WCET. This feeling is strengthened when these estimations are compared to measured execution times: generally, it is very unlikely to capture the worstcase from observations, then the difference between the highest watermark and the proven WCET upper bound might be considerable. In this paper, we introduce a framework to quantify the possible overestimation on WCET upper bounds obtained by static analysis. The objective is to derive a lower bound on the WCET to complement the upper bound.
Cite as
Hugues Cassé, Haluk Ozaktas, and Christine Rochange. A Framework to Quantify the Overestimations of Static WCET Analysis. In 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015). Open Access Series in Informatics (OASIcs), Volume 47, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{casse_et_al:OASIcs.WCET.2015.1,
author = {Cass\'{e}, Hugues and Ozaktas, Haluk and Rochange, Christine},
title = {{A Framework to Quantify the Overestimations of Static WCET Analysis}},
booktitle = {15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)},
pages = {1--10},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-95-8},
ISSN = {2190-6807},
year = {2015},
volume = {47},
editor = {Cazorla, Francisco J.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2015.1},
URN = {urn:nbn:de:0030-drops-52517},
doi = {10.4230/OASIcs.WCET.2015.1},
annote = {Keywords: Static WCET analysis, uncertainty, overestimation, cache analysis}
}
Document
Software-enforced Interconnect Arbitration for COTS Multicores
Abstract
The advent of multicore processors complicates timing analysis owing to the need to account for the interference between cores accessing shared resources, which is not always easy to characterize in a safe and tight way. Solutions have been proposed that take two distinct but complementary directions: on the one hand, complex analysis techniques have been developed to provide safe and tight bounds to contention; on the other hand, sophisticated arbitration policies (hardware or software) have been proposed to limit or control inter-core interference. In this paper we propose a software-based TDMA-like arbitration of accesses to a shared interconnect (e.g. a bus) that prevents inter-core interference. A more flexible arbitration scheme is also proposed to reserve more bandwidth to selected cores while still avoiding contention. A proof-of-concept implementation on an AURIX TC277TU processor shows that our approach can apply to COTS processors, thus not relying on dedicated hardware arbiters, while introducing little overhead.
Cite as
Marco Ziccardi, Alessandro Cornaglia, Enrico Mezzetti, and Tullio Vardanega. Software-enforced Interconnect Arbitration for COTS Multicores. In 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015). Open Access Series in Informatics (OASIcs), Volume 47, pp. 11-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{ziccardi_et_al:OASIcs.WCET.2015.11,
author = {Ziccardi, Marco and Cornaglia, Alessandro and Mezzetti, Enrico and Vardanega, Tullio},
title = {{Software-enforced Interconnect Arbitration for COTS Multicores}},
booktitle = {15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)},
pages = {11--20},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-95-8},
ISSN = {2190-6807},
year = {2015},
volume = {47},
editor = {Cazorla, Francisco J.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2015.11},
URN = {urn:nbn:de:0030-drops-52526},
doi = {10.4230/OASIcs.WCET.2015.11},
annote = {Keywords: Multicore, Resource Arbitration, Interference, Mixed-Criticality}
}
Document
Timing Analysis of Event-Driven Programs with Directed Testing
Abstract
Accurately estimating the worst-case execution time (WCET) of real-time event-driven software is crucial. For example, NASA's study of unintended acceleration in Toyota vehicles highlights poor support in timing analysis for event-driven code, which could put human life in danger. WCET occurs during the longest possible execution path in a program. Static analysis produces safe but overestimated measurements. Dynamic analysis, on other hand, measures actual execution times of code under a test suite. Its performance depends on the branch coverage, which itself is sensitive to scheduling of events. Thus dynamic analysis often underestimates the WCET. We present a new dynamic approach called event-driven directed testing. Our approach combines aspects of prior random-testing techniques devised for event-driven code with the directed testing method applied to sequential code. The aim is to come up with complex event sequences and choices of parameters for individual events that might result in execution times closer to the true WCET. Our experiments show that, compared to random testing, genetic algorithms, and traditional directed testing, we achieve significantly better branch coverage and longer WCET.
Cite as
Mahdi Eslamimehr and Hesam Samimi. Timing Analysis of Event-Driven Programs with Directed Testing. In 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015). Open Access Series in Informatics (OASIcs), Volume 47, pp. 21-31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{eslamimehr_et_al:OASIcs.WCET.2015.21,
author = {Eslamimehr, Mahdi and Samimi, Hesam},
title = {{Timing Analysis of Event-Driven Programs with Directed Testing}},
booktitle = {15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)},
pages = {21--31},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-95-8},
ISSN = {2190-6807},
year = {2015},
volume = {47},
editor = {Cazorla, Francisco J.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2015.21},
URN = {urn:nbn:de:0030-drops-52535},
doi = {10.4230/OASIcs.WCET.2015.21},
annote = {Keywords: worst-case execution time, timing analysis, event-driven, directed testing}
}
Document
GenE: A Benchmark Generator for WCET Analysis
Abstract
The fact that many benchmarks for evaluating worst-case execution time (WCET) analysis tools are based on real-world applications greatly increases the value of their results. However, at the same time, the complexity of these programs makes it difficult, sometimes even impossible, to obtain all corresponding flow facts (i.e., loop bounds, infeasible paths, and input values triggering the WCET), which are essential for a comprehensive evaluation. In this paper, we address this problem by presenting GenE, a benchmark generator that in addition to source code also provides the flow facts of the benchmarks created. To generate a new benchmark, the tool combines code patterns that are commonly found in real-time applications and are challenging for WCET analyzers. By keeping track of how patterns are put together, GenE is able to determine the flow facts of the resulting benchmark based on the known flow facts of the patterns used. Using this information, it is straightforward to synthesize the accurate WCET, which can then serve as a baseline for the evaluation of WCET analyzers.
Cite as
Peter Wägemann, Tobias Distler, Timo Hönig, Volkmar Sieh, and Wolfgang Schröder-Preikschat. GenE: A Benchmark Generator for WCET Analysis. In 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015). Open Access Series in Informatics (OASIcs), Volume 47, pp. 33-43, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{wagemann_et_al:OASIcs.WCET.2015.33,
author = {W\"{a}gemann, Peter and Distler, Tobias and H\"{o}nig, Timo and Sieh, Volkmar and Schr\"{o}der-Preikschat, Wolfgang},
title = {{GenE: A Benchmark Generator for WCET Analysis}},
booktitle = {15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)},
pages = {33--43},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-95-8},
ISSN = {2190-6807},
year = {2015},
volume = {47},
editor = {Cazorla, Francisco J.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2015.33},
URN = {urn:nbn:de:0030-drops-52545},
doi = {10.4230/OASIcs.WCET.2015.33},
annote = {Keywords: WCET, benchmark generation, flow facts, WCET Tool Challenge}
}
Document
Precise Continuous Non-Intrusive Measurement-Based Execution Time Estimation
Abstract
Precise estimation of the Worst-Case Execution Time (WCET) of embedded software is a necessary precondition in safety critical systems. Static methods for WCET analysis rely on precise models of the target processor’s micro-architecture. Measurement-based methods, in contrast, rely on exhaustive measurements performed on the real hardware. The rise of the multicore processors often renders staticWCET analysis infeasible, either due to the computational complexity or due the lack of necessary documentation. Current approaches for (hybrid) measurement-based WCET estimation process the trace data offline and thus need to store large amounts of data. In this contribution, we present a novel approach that performs continuous online aggregation of timing measurements. This enables long observation periods and increases the possibility to catch rare circumstances. Moreover, we incorporate the execution contexts of basic blocks. We can therefore account for typical cache behaviour, without being overly pessimistic.
Cite as
Boris Dreyer, Christian Hochberger, Simon Wegener, and Alexander Weiss. Precise Continuous Non-Intrusive Measurement-Based Execution Time Estimation. In 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015). Open Access Series in Informatics (OASIcs), Volume 47, pp. 45-54, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{dreyer_et_al:OASIcs.WCET.2015.45,
author = {Dreyer, Boris and Hochberger, Christian and Wegener, Simon and Weiss, Alexander},
title = {{Precise Continuous Non-Intrusive Measurement-Based Execution Time Estimation}},
booktitle = {15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)},
pages = {45--54},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-95-8},
ISSN = {2190-6807},
year = {2015},
volume = {47},
editor = {Cazorla, Francisco J.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2015.45},
URN = {urn:nbn:de:0030-drops-52555},
doi = {10.4230/OASIcs.WCET.2015.45},
annote = {Keywords: Hybrid Worst-Case Execution Time (WCET) Estimation for Multicore Processors, Real-time Systems}
}
Document
Context-sensitive Parametric WCET Analysis
Abstract
In this paper, we propose aWCET analysis that focuses on two aspects. First, it supports contextsensitive hardware and software timing effects, meaning that it is sensitive to the execution history of the program and thus can account for effects like cache persistence, triangular loop, etc. Second, it supports the introduction of parameters in both the software model (e.g. parametric loop bounds) and the hardware model (e.g. number of cache misses). WCET computation by static analysis is traditionally handled by the Implicit Path Enumeration Technique (IPET), using an Integer Linear Program (ILP) that is difficult to resolve parametrically. We suggest an alternative tree-based approach. We define a context-sensitive CFG format to express these effects, and we provide an efficient method to process it, giving a parametric WCET formula. Experimental results show that this new method is significantly faster and more accurate than existing parametric approaches.
Cite as
Clément Ballabriga, Julien Forget, and Giuseppe Lipari. Context-sensitive Parametric WCET Analysis. In 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015). Open Access Series in Informatics (OASIcs), Volume 47, pp. 55-64, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{ballabriga_et_al:OASIcs.WCET.2015.55,
author = {Ballabriga, Cl\'{e}ment and Forget, Julien and Lipari, Giuseppe},
title = {{Context-sensitive Parametric WCET Analysis}},
booktitle = {15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)},
pages = {55--64},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-95-8},
ISSN = {2190-6807},
year = {2015},
volume = {47},
editor = {Cazorla, Francisco J.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2015.55},
URN = {urn:nbn:de:0030-drops-52569},
doi = {10.4230/OASIcs.WCET.2015.55},
annote = {Keywords: Parametric, WCET, Real-time, Static analysis}
}
Document
WCET and Mixed-Criticality: What does Confidence in WCET Estimations Depend Upon?
Abstract
Mixed-criticality systems integrate components of different criticality. Different criticality levels require different levels of confidence in the correct behavior of a component. One aspect of correctness is timing. Confidence in worst-case execution time (WCET) estimates depends on the process by which they have been obtained. A somewhat naive view is that static WCET analyses determines safe bounds in which we can have absolute confidence, while measurement-based approaches are inherently unreliable. In this paper, we refine this view by exploring sources of doubt in the correctness of both static and measurement-based WCET analysis.
Cite as
Sebastian Altmeyer, Björn Lisper, Claire Maiza, Jan Reineke, and Christine Rochange. WCET and Mixed-Criticality: What does Confidence in WCET Estimations Depend Upon?. In 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015). Open Access Series in Informatics (OASIcs), Volume 47, pp. 65-74, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{altmeyer_et_al:OASIcs.WCET.2015.65,
author = {Altmeyer, Sebastian and Lisper, Bj\"{o}rn and Maiza, Claire and Reineke, Jan and Rochange, Christine},
title = {{WCET and Mixed-Criticality: What does Confidence in WCET Estimations Depend Upon?}},
booktitle = {15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)},
pages = {65--74},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-95-8},
ISSN = {2190-6807},
year = {2015},
volume = {47},
editor = {Cazorla, Francisco J.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2015.65},
URN = {urn:nbn:de:0030-drops-52574},
doi = {10.4230/OASIcs.WCET.2015.65},
annote = {Keywords: mixed criticality, WCET analysis, confidence in WCET estimates}
}
Document
Bare-Metal Execution of Hard Real-Time Tasks Within a General-Purpose Operating System
Abstract
Integrating high performance and real-time demands on multi-processor systems is a challenging task. We present our concept of isolating processes from a general-purpose operating system without deeply invading modifications. This allows executing code on dedicated CPUs with minimum latency and jitter like bare-metal on micro-controllers. The unbounded execution of mixed critical processes on the same system induces performance interference in real-time tasks. We present the implementation of isolated partitions on multi-processor x86 systems running Linux and describe challenges restoring operating system stability. This work also presents our experience with Non-Uniform Memory Access architectures that allow to partition the system in a way that the impact to memory and I/O transfers of other partitions is minimized.
Cite as
Georg Wassen and Stefan Lankes. Bare-Metal Execution of Hard Real-Time Tasks Within a General-Purpose Operating System. In 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015). Open Access Series in Informatics (OASIcs), Volume 47, pp. 75-84, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{wassen_et_al:OASIcs.WCET.2015.75,
author = {Wassen, Georg and Lankes, Stefan},
title = {{Bare-Metal Execution of Hard Real-Time Tasks Within a General-Purpose Operating System}},
booktitle = {15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)},
pages = {75--84},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-95-8},
ISSN = {2190-6807},
year = {2015},
volume = {47},
editor = {Cazorla, Francisco J.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2015.75},
URN = {urn:nbn:de:0030-drops-52584},
doi = {10.4230/OASIcs.WCET.2015.75},
annote = {Keywords: Hard Real-Time System, High-Performance Computing, Non-uniform Memory Access, Bare-Metal Execution}
}
Document
Analysing Switch-Case Code with Abstract Execution
Abstract
Constructing the control-flow graph (CFG) of machine code is made difficult by dynamic transfers of control (DTC), where the address of the next instruction is computed at run-time. Switchcase statements make compilers generate a large variety of machine-code forms with DTC. Two analysis approaches are commonly used: pattern-matching methods identify predefined instruction patterns to extract the target addresses, while analytical methods try to compute the set of target addresses using a general value-analysis. We tested the abstract execution method of the SWEET tool as a value analysis for switch-case code. SWEET is here used as a plugin to the Bound-T tool: thus our work can also be seen as an experiment in modular tool design, where a general value-analysis tool is used to aid the CFG construction in a WCET analysis tool. We find that the abstract-execution analysis works at least as well as the switch-case analyses in Bound-T itself, which are mostly based on pattern-matching. However, there are still some weaknesses: the abstract domains available in SWEET are not well suited to representing sets of DTC target addresses, which are small but sparse and irregular. Also, in some cases the abstract-execution analysis fails because the used domain is not relational, that is, does not model arithmetic relationships between the values of different variables. Future work will be directed towards the design of abstract domains eliminating these weaknesses.
Cite as
Niklas Holsti, Jan Gustafsson, Linus Källberg, and Björn Lisper. Analysing Switch-Case Code with Abstract Execution. In 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015). Open Access Series in Informatics (OASIcs), Volume 47, pp. 85-94, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{holsti_et_al:OASIcs.WCET.2015.85,
author = {Holsti, Niklas and Gustafsson, Jan and K\"{a}llberg, Linus and Lisper, Bj\"{o}rn},
title = {{Analysing Switch-Case Code with Abstract Execution}},
booktitle = {15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)},
pages = {85--94},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-95-8},
ISSN = {2190-6807},
year = {2015},
volume = {47},
editor = {Cazorla, Francisco J.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2015.85},
URN = {urn:nbn:de:0030-drops-52598},
doi = {10.4230/OASIcs.WCET.2015.85},
annote = {Keywords: ynamic control flow, indexed branch, machine-code analysis, WCET analysis}
}
Document
Using SMT Solving for the Lookup of Infeasible Paths in Binary Programs
Abstract
Worst-Case Execution Time (WCET) is a key component to check temporal constraints of realtime systems. WCET by static analysis provides a safe upper bound. While hardware modelling is now efficient, loss of precision stems mainly in the inclusion of infeasible execution paths in the WCET calculation. This paper proposes a new method to detect such paths based on static analysis of machine code and the feasibility test of conditions using Satisfiability Modulo Theory (SMT) solvers. The experimentation shows promising results although the expected precision was slightly lowered due to clamping operations needed to cope with complexity explosion. An important point is that the implementation has been performed in the OTAWA framework and is independent of any instruction set thanks to its semantic instructions.
Cite as
Jordy Ruiz and Hugues Cassé. Using SMT Solving for the Lookup of Infeasible Paths in Binary Programs. In 15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015). Open Access Series in Informatics (OASIcs), Volume 47, pp. 95-104, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
Copy BibTex To Clipboard
@InProceedings{ruiz_et_al:OASIcs.WCET.2015.95,
author = {Ruiz, Jordy and Cass\'{e}, Hugues},
title = {{Using SMT Solving for the Lookup of Infeasible Paths in Binary Programs}},
booktitle = {15th International Workshop on Worst-Case Execution Time Analysis (WCET 2015)},
pages = {95--104},
series = {Open Access Series in Informatics (OASIcs)},
ISBN = {978-3-939897-95-8},
ISSN = {2190-6807},
year = {2015},
volume = {47},
editor = {Cazorla, Francisco J.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2015.95},
URN = {urn:nbn:de:0030-drops-52604},
doi = {10.4230/OASIcs.WCET.2015.95},
annote = {Keywords: WCET, infeasible paths, SMT, machine code}
}