-
Vérification des systèmes multi-agents comportementalistes par le moyen des s...
Multi-agent systems (MASs) can be used to model phenomena that can be decomposed into several interacting agents which exist within an environment. In particular, they... -
Formal Fact-Oriented model transformations for Cooperative Information System...
ISBN 978-3-642-29957-5 Selected extended paper from ICEIS'2011 -
Verification and composition of security protocols with applications to elect...
This thesis is about the formal verification and composition of security protocols, motivated by applications to electronic voting protocols. Chapters 3 to 5 concern... -
Latency-Insensitive Design and Central Repetitive Scheduling
The theory of latency-insensitive design (LID) was recently invented to cope with the time closure problem in otherwise synchronous circuits and programs. The idea is... -
Verification of Control Properties in the Polyhedral Model
We propose a combination of heuristic methods to prove properties of control signals for regular systems defined by means of affine recurrence equations (AREs). We... -
Model-oriented appraoch for verification and performance evaluation of servic...
Web services are widely used by organizations to share their knowledge over the network and facilitate business-to-business collaboration. The emergence of Web... -
Foundations and practice of security : 4th Canada-France MITACS workshop, FPS...
International audience -
Integrating Formal Verification Techniques into Software Development Process ...
In past years, formal verification techniques and tools were widely developed and used by the research community. However, the use of formal verification at industrial... -
Interactive Abstractions: Proving Safety Properties by Integrating Static Ana...
We present a new approach for proving safety properties of reactive systems, based on tight interaction between static analysis, theorem proving and abstraction... -
Circuit Generation for Verification of ESTEREL Programs
We propose in this paper a method that takes external Boolean variables into account for the verification of ESTEREL programs. The intermediate code that we use is a... -
Formal Verification of Netlog Protocols
International audience -
Towards Timed Requirement Verification for Service Choreographies
International audience -
On the Validation of Robotics Control Systems Part I: High Level Specificatio...
This report presents an extensive work on the specification and the formal verification of complex applications in advanced robotics systems. In a first part, the need... -
Large Integrating formal verification methods of quantitative real-time prope...
In this paper we describe our experience with a development environment for robot controllers, which provides the user with formal verification functionalities. We... -
Black-Box And White-Box Early Power Intent Simulation and Verification: Two N...
International audience -
Reachability Analysis of Hybrid Systems using Support Functions
In model based design, one constructs a mathematical model of the system and uses it to design the system so that it exhibits the desired properties. For safety... -
Compositional design of isochronous systems
International audience
