Sciweavers

FMICS
2009
Springer
13 years 8 months ago
Platform-Specific Restrictions on Concurrency in Model Checking of Java Programs
The main limitation of software model checking is that, due to state explosion, it does not scale to real-world multi-threaded programs. One of the reasons is that current software...
Pavel Parizek, Tomás Kalibera
FMICS
2009
Springer
13 years 8 months ago
On a Uniform Framework for the Definition of Stochastic Process Languages
In this paper we show how Rate Transition Systems (RTSs) can be used as a unifying framework for the definition of the semantics of stochastic process algebras. RTSs facilitate the...
Rocco De Nicola, Diego Latella, Michele Loreti, Mi...
FMICS
2009
Springer
13 years 8 months ago
A Certified Implementation on Top of the Java Virtual Machine
Abstract. Safe is a first-order functional language with unusual memory management features: memory can be both explicitly and implicitly deallocated at some specific points in the...
Javier de Dios, Ricardo Peña-Marí
FMICS
2009
Springer
13 years 11 months ago
Model-Based Testing of Electronic Passports
Wojciech Mostowski, Erik Poll, Julien Schmaltz, Ja...
FMICS
2009
Springer
13 years 11 months ago
Preemption Abstraction
Erik Schierboom, Alejandro Tamalet, Hendrik Tews, ...
FMICS
2009
Springer
13 years 11 months ago
Dynamic State Space Partitioning for External Memory Model Checking
We describe a dynamic partitioning scheme usable by model checking techniques that divide the state space into partitions, such as most external memory and distributed model checki...
Sami Evangelista, Lars Michael Kristensen
FMICS
2009
Springer
13 years 11 months ago
Formal Analysis of Non-determinism in Verilog Cell Library Simulation Models
Cell libraries often contain a simulation model in a system design language, such as Verilog. These languages usually involve nondeterminism, which in turn, poses a challenge to th...
Matthias Raffelsieper, Mohammad Reza Mousavi, Jan-...
FMICS
2009
Springer
13 years 11 months ago
Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software
Most modern safety-critical control programs, such as those embedded in fly-by-wire control systems, perform a lot of floating-point computations. The well-known pitfalls of IEEE...
David Delmas, Eric Goubault, Sylvie Putot, Jean So...
FMICS
2009
Springer
13 years 11 months ago
Visualising Event-B Models with B-Motion Studio
Lukas Ladenberger, Jens Bendisposto, Michael Leusc...
FMICS
2009
Springer
13 years 11 months ago
A Rigorous Methodology for Composing Services
on Abstraction: a Lightweight Approach to Modelling Concurrency. Javier de Dios and Ricardo Peña Certified Implementation on top of the Java Virtual Machine 19:00 Social dinner + ...
Kenneth J. Turner, Koon Leai Larry Tan