We present a new property driven pruning algorithm in dynamic model checking to efficiently detect race conditions in multithreaded programs. The main idea is to use a lockset base...
Abstract. NetQi is a freely available model-checker designed to analyze network incidents such as intrusion. This tool is an implementation of the anticipation game framework, a va...
The evaluation of successor or predecessor state spaces through time progress is a central component in the model-checking algorithm of dense-time automata. The definition of the t...
Goanna is an industrial-strength static analysis tool used in academia and industry alike to find bugs in C/C++ programs. Unlike existing approaches Goanna uses the off-the-shelf N...
Abstract. Non-freely generated data types are widely used in case studies carried out in the theorem prover KIV. The most common examples are stores, sets and arrays. We present an...
We show how fault injection together with recent advances in stochastic model checking can be combined to form a crucial ingredient for improving quantitative safety analysis. Base...
UPPAAL PORT is a new tool for component-based design and analysis of embedded systems. It operates on the hierarchically structured continuous time component modeling language Save...
We present a compositional method for the verification of component-based systems described in a subset of the BIP language encompassing multi-party interaction without data transf...
Saddek Bensalem, Marius Bozga, Joseph Sifakis, Tha...