Sciweavers

TACAS
2004
Springer
132views Algorithms» more  TACAS 2004»
13 years 10 months ago
Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study
Numerical analysis based on uniformisation and statistical techniques based on sampling and simulation are two distinct approaches for transient analysis of stochastic systems. We ...
Håkan L. S. Younes, Marta Z. Kwiatkowska, Ge...
TACAS
2004
Springer
114views Algorithms» more  TACAS 2004»
13 years 10 months ago
Symbolically Computing Most-Precise Abstract Operations for Shape Analysis
Greta Yorsh, Thomas W. Reps, Shmuel Sagiv
TACAS
2004
Springer
97views Algorithms» more  TACAS 2004»
13 years 10 months ago
Resource-Optimal Scheduling Using Priced Timed Automata
Jacob Illum Rasmussen, Kim Guldstrand Larsen, K. S...
TACAS
2004
Springer
114views Algorithms» more  TACAS 2004»
13 years 10 months ago
CoPS - Checker of Persistent Security
Carla Piazza, Enrico Pivato, Sabina Rossi
TACAS
2004
Springer
108views Algorithms» more  TACAS 2004»
13 years 10 months ago
The Succinct Solver Suite
Abstract. The Succinct Solver Suite offers two analysis engines for solving data and control flow problems expressed in clausal form in a large fragment of first order logic. Th...
Flemming Nielson, Hanne Riis Nielson, Hongyan Sun,...
TACAS
2004
Springer
127views Algorithms» more  TACAS 2004»
13 years 10 months ago
MetaGame: An Animation Tool for Model-Checking Games
Abstract. Failing model checking runs should be accompanied by appropriate error diagnosis information that allows the user to identify the cause of the problem. For branching time...
Markus Müller-Olm, Haiseung Yoo
TACAS
2004
Springer
110views Algorithms» more  TACAS 2004»
13 years 10 months ago
An Interpolating Theorem Prover
We present a method of deriving Craig interpolants from proofs in the quantifier-free theory of linear inequality and uninterpreted function symbols, and an interpolating theorem...
Kenneth L. McMillan
TACAS
2004
Springer
122views Algorithms» more  TACAS 2004»
13 years 10 months ago
A Scalable Incomplete Test for the Boundedness of UML RT Models
Abstract. We describe a scalable incomplete boundedness test for the communication buffers in UML RT models. UML RT is a variant of the UML modeling language, tailored to describin...
Stefan Leue, Richard Mayr, Wei Wei