Sciweavers

FMICS
2006
Springer
13 years 7 months ago
SAT-Based Verification of LTL Formulas
Abstract. Bounded model checking (BMC) based on satisfiability testing (SAT) has been introduced as a complementary technique to BDDbased symbolic model checking of LTL properties ...
Wenhui Zhang
FMICS
2006
Springer
13 years 7 months ago
Discovering Symmetries
Hassen Saïdi
FMICS
2006
Springer
13 years 7 months ago
Verified Design of an Automated Parking Garage
Parking garages that stow and retrieve cars automatically are becoming viable solutions for parking shortages. However, these are complex systems and a number of severe incidents i...
Aad Mathijssen, A. Johannes Pretorius
FMICS
2006
Springer
13 years 7 months ago
jmle: A Tool for Executing JML Specifications Via Constraint Programming
Formal specifications are more useful and easier to develop if they are executable. In this work, we describe a system for executing specifications written in the Java Modeling Lan...
Ben Krause, Tim Wahls
FMICS
2006
Springer
13 years 7 months ago
Model-Based Testing of a WAP Gateway: An Industrial Case-Study
Abstract. We present experiences from a case study where a model-based approach to black-box testing is applied to verify that a Wireless Application Protocol (WAP) gateway conform...
Anders Hessel, Paul Pettersson
FMICS
2006
Springer
13 years 7 months ago
"To Store or Not To Store" Reloaded: Reclaiming Memory on Demand
Behrmann et al. posed the question whether "To Store or Not To Store" [1] states during reachability analysis, in order to counter the effects of the well-known state spa...
Moritz Hammer, Michael Weber
FMICS
2006
Springer
13 years 7 months ago
Goanna - A Static Model Checker
Ansgar Fehnker, Ralf Huuck, Patrick Jayet, Michel ...
FMICS
2006
Springer
13 years 7 months ago
Can Saturation Be Parallelised?
Abstract. Symbolic state-space generators are notoriously hard to parallelise. However, the Saturation algorithm implemented in the SMART verification tool differs from other seque...
Jonathan Ezekiel, Gerald Lüttgen, Radu Simini...
FMICS
2006
Springer
13 years 7 months ago
Evaluating Quality of Service for Service Level Agreements
Abstract. Quantitative analysis of quality-of-service metrics is an important tool in early evaluation of service provision. This analysis depends on being able to estimate the ave...
Allan Clark, Stephen Gilmore
FMICS
2006
Springer
13 years 7 months ago
Automated Incremental Synthesis of Timed Automata
Abstract. In this paper, we concentrate on incremental synthesis of timed automata for automatic addition of different types of bounded response properties. Bounded response
Borzoo Bonakdarpour, Sandeep S. Kulkarni