STTT
2008
13 years 7 months ago
2008
We present ProB, a validation toolset for the B method. ProB's automated animation facilities allow users to gain confidence in their specifications. ProB also contains a mode...
MJ
2006
13 years 7 months ago
2006
In this paper, we describe a hybrid tool for hardware formal verification that links the HOL (higher-order logic) theorem prover and (multiway decision graphs) model checker. Our ...
JSS
2006
13 years 7 months ago
2006
Model checking is a powerful automated technique mainly used for the verification of properties of reactive systems. In practice, model checkers are limited due to the state explos...
ENTCS
2006
13 years 7 months ago
2006
This paper presents VyrdMC, a runtime verification tool we are building for concurrent software components. The correctness criterion checked by VyrdMC is refinement: Each executi...
ENTCS
2008
13 years 7 months ago
2008
The broad availability of multi-core chips on standard desktop PCs provides strong motivation for the development of new algorithms for logic model checkers that can take advantag...
DC
2010
13 years 7 months ago
2010
Model checking software transactional memories (STMs) is difficult because of the unbounded number, length, and delay of concurrent transactions and the unbounded size of the memo...
FMICS
2010
Springer
13 years 8 months ago
2010
Springer
Embedded networks for chip-to-chip networks are emerging as communication infrastructure in mobile devices. We present three novel embedded network protocols: a sliding window prot...
FORTE
2001
13 years 8 months ago
2001
The modal logic FULL is designed to capture strong bisimulation over early symbolic transition systems (STSs) for full LOTOS. It provides a compact way of expressing and verifying ...
FORTE
2004
13 years 8 months ago
2004
In this paper, we present an approach for modeling an existing web application using communicating finite automata model based on the userdefined properties to be validated. We ela...
ISSRE
2007
IEEE
13 years 9 months ago
2007
IEEE
Model-checkers are powerful tools that can find individual traces through models to satisfy desired properties. These traces provide solutions to a number of problems. Instead of...