-
Knowledge compilation for online decision-making : application to the control...
Controlling autonomous systems requires to make decisions depending on current observations and objectives. This involves some tasks that must be executed online--with... -
State equality detection for implementation-level model-checking of distribut...
International audience -
Genetic Network Analyzer: A Tool for the Qualitative Modeling and Simulation ...
International audience -
Abstraction-based Malware Analysis Using Rewriting and Model Checking
International audience -
SystemC waiting-state automata
International audience -
Timed SystemC waiting-state automata
International audience -
Context Aware Model Exploration with OBP tool to Improve Model-Checking
International audience -
Diagnostic of discrete event systems using timed automata in MATLAB SIMULINK
International audience -
Concurrency Makes Simple Theories Hard
International audience -
Counting CTL
The original publication is available at www.springerlink.com. -
Counting LTL
The original publication is available at ieeexplore.ieee.org. -
Interrupt Timed Automata: verification and expressiveness
International audience -
McScM: A General Framework for the Verification of Communicating Machines
International audience -
Time Properties Verification Framework for UML-MARTE Safety Critical Real-Tim...
Time properties are key requirements for the reliability of Safety Critical Real-Time Systems (RTS). UML and MARTE are standardized modelling languages widely accepted... -
Equational Abstraction Refinement for Certified Tree Regular Model Checking
Tree Regular Model Checking (TRMC) is the name of a family of techniques for analyzing in nite-state systems in which states are represented by trees and sets of... -
An overview of CADP 2001
CADP is a toolbox for specifying and verifying asynchronous finite-state systems described using process algebraic languages. It offers a wide range of... -
Exp.Open 2.0: A Flexible Tool Integrating Partial Order, Compositional, and O...
It is desirable to integrate formal verification techniques applicable to different languages. We present EXP.OPEN 2.0, a new tool of the CADP verification toolbox... -
Behavioural Models for Hierarchical Components
We describe a method for the specification and verification of the dynamic behaviour of component systems. Building applications using a component framework allows the... -
Combining symbolic execution and model checking to reduce dynamic program ana...
By using symbolic execution techniques in the framework of the Java PathFinder model checker, we show that some Java program statements are unable to change the... -
Formalisation and verification of the Chilean electronic invoice system
We present a case study describing the formal specification and verification of the Chilean electronic invoice system, which has been defined by the Chilean taxes...
