Classical verification often uses abstraction when dealing with data. On the other hand, dynamic XML-based applications have become pervasive, for instance with the ever growing im...
Blaise Genest, Anca Muscholl, Olivier Serre, Marc ...
We present a tool for parallel shared-memory enumerative LTL model-checking and reachability analysis. The tool is based on distributed-memory algorithms reimplemented specifically...
In this paper, a uniform approach for synthesizing monitors checking correctness properties specified in linear-time logics at runtime is provided. Therefore, a generic three-value...
e Abstraction Arie Gurfinkel1 , Ou Wei2 , and Marsha Chechik2 1 Software Engineering Institute, Carnegie Mellon University 2 Department of Computer Science, University of Toronto A...
Multi-valued Model Checking is an extension of classical, two-valued model checking with multi-valued logic. Multi-valuedness has been proved useful in expressing additional inform...
Model checking has proven to be a useful analysis technique not only for concurrent systems, but also for the genetic regulatory networks (Grns) that govern the functioning of livi...
Radu Mateescu, Pedro T. Monteiro, Estelle Dumas, H...
We identify a new class of decidable hybrid automata: namely, parallel compositions of semi-algebraic o-minimal automata. The class we consider is fundamental to hierarchical model...
Alberto Casagrande, Pietro Corvaja, Carla Piazza, ...
Electronic inter-organizational relationships are governed by contracts regulating their interaction. It is necessary to run-time monitor the contracts, as to guarantee their fulfi...