Sciweavers

Share
TACAS
2004
Springer
107views Algorithms» more  TACAS 2004»
10 years 5 months ago
Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata
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...
Pavel Krcál, Wang Yi
TACAS
2004
Springer
139views Algorithms» more  TACAS 2004»
10 years 5 months ago
Error Explanation with Distance Metrics
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 ...
Alex Groce
TACAS
2004
Springer
94views Algorithms» more  TACAS 2004»
10 years 5 months ago
Numeric Domains with Summarized Dimensions
We introduce a systematic approach to designing summarizing abstract numeric domains from existing numeric domains. Summarizing domains use summary dimensions to represent potentia...
Denis Gopan, Frank DiMaio, Nurit Dor, Thomas W. Re...
TACAS
2004
Springer
135views Algorithms» more  TACAS 2004»
10 years 5 months ago
Liveness with Incomprehensible Ranking
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...
Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck
TACAS
2004
Springer
62views Algorithms» more  TACAS 2004»
10 years 5 months ago
Lower and Upper Bounds in Zone Based Abstractions of Timed Automata
Gerd Behrmann, Patricia Bouyer, Kim Guldstrand Lar...
TACAS
2004
Springer
90views Algorithms» more  TACAS 2004»
10 years 5 months ago
FASTer Acceleration of Counter Automata in Practice
Sébastien Bardin, Alain Finkel, Jér&...
TACAS
2004
Springer
111views Algorithms» more  TACAS 2004»
10 years 5 months ago
Automatic Creation of Environment Models via Training
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...
Thomas Ball, Vladimir Levin, Fei Xie
TACAS
2004
Springer
108views Algorithms» more  TACAS 2004»
10 years 5 months ago
Model Checking Discounted Temporal Properties
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...
Luca de Alfaro, Marco Faella, Thomas A. Henzinger,...
TACAS
2004
Springer
94views Algorithms» more  TACAS 2004»
10 years 5 months ago
A Tool for Checking ANSI-C Programs
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...
Edmund M. Clarke, Daniel Kroening, Flavio Lerda
books