Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
PLDI
2010
ACM
10 years 4 months ago
Parameterized Verification of Transactional Memories
We describe an automatic verification method to check whether transactional memories ensure strict serializability--a key property assumed of the transactional interface. Our main...
Michael Emmi, Rupak Majumdar, Roman Manevich
ICDCSW
2000
IEEE
10 years 4 months ago
Compositional Verification of a Third Generation Mobile Communication Protocol
Model-checking has turned out to be an efficient and relatively easy-to-use technique in the verification of formally described programs. However, there is one major drawback in u...
Sari Leppänen, Matti Luukkainen
FMICS
2009
Springer
10 years 5 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
FM
2001
Springer
118views Formal Methods» more  FM 2001»
10 years 5 months ago
Avoiding State Explosion for Distributed Systems with Timestamps
This paper describes a reduction technique which is very useful against the state explosion problem which occurs when model checking many distributed systems. Timestamps are often ...
Fabrice Derepas, Paul Gastin, David Plainfoss&eacu...
GLVLSI
2002
IEEE
95views VLSI» more  GLVLSI 2002»
10 years 6 months ago
Term ordering problem on MDG
As an efficient representation of Extended Finite State Machines, Multiway Decision Graphs (MDG) are suitable for automatic hardware verification of Register Transfer Level (RTL) ...
Yi Feng, Eduard Cerny
SPIN
2005
Springer
10 years 6 months ago
Model Checking Machine Code with the GNU Debugger
Embedded software verification is an important verification problem that requires the ability to reason about the timed semantics of concurrent behaviors at a low level of atomic...
Eric Mercer, Michael Jones
EUROMICRO
2007
IEEE
10 years 7 months ago
Partial Verification of Software Components: Heuristics for Environment Construction
Code model checking of software components suffers from the well-known problem of state explosion when applied to highly parallel components, despite the fact that a single compon...
Pavel Parizek, Frantisek Plasil
books