TACAS
2004
Springer
14 years 5 months ago
2004
Springer
Abstract. We study schedulability problems of timed systems with nonuniformly recurring computation tasks. Assume a set of real time tasks whose best and worst execution times, and...
TACAS
2004
Springer
14 years 5 months ago
2004
Springer
Abstract In the event that a system does not satisfy a specification, a model checker will typically automatically produce a counterexample trace that shows a particular instance ...
TACAS
2004
Springer
14 years 5 months ago
2004
Springer
We introduce a systematic approach to designing summarizing abstract numeric domains from existing numeric domains. Summarizing domains use summary dimensions to represent potentia...
TACAS
2004
Springer
14 years 5 months ago
2004
Springer
Abstract. The methods of Invisible Invariants and Invisible Ranking were developed originally in order to verify temporal properties of parameterized systems in a fully automatic m...
TACAS
2004
Springer
14 years 5 months ago
2004
Springer
TACAS
2004
Springer
14 years 5 months ago
2004
Springer
TACAS
2004
Springer
14 years 5 months ago
2004
Springer
Abstract. Model checking suffers not only from the state-space explosion problem, but also from the environment modeling problem: how can one create an accurate enough model of the...
TACAS
2004
Springer
14 years 5 months ago
2004
Springer
Temporal logic is two-valued: formulas are interpreted as either true or false. When applied to the analysis of stochastic systems, or systems with imprecise formal models, tempor...
TACAS
2004
Springer
14 years 5 months ago
2004
Springer
Abstract. We present a tool for the formal verification of ANSI-C programs using Bounded Model Checking (BMC). The emphasis is on usability: the tool supports almost all ANSI-C la...