Dataset - CKAN

Qualitative and Quantitative Methods for Detection of Hidden Information

Information systems have become ubiquitous and are used to handle each day more and more data. This data is increasingly confidential: strategic military or financial...

HTML

A formal study of Free Software distributions

Over the last two decades, free and open source software has grown considerably. Distributions that started out with a few hundred packages now contain tens of...

HTML

Security policies modeling by using formal methods

Access control allows one to specify a part of the security Policy of an IS (information system). An AC (access control) policy defines which conditions must old for...

HTML

Certification of a Tool Chain for Deductive Program Verification

This thesis belongs to the domain of software verification. The goalof verifying software is to ensure that an implementation, a program,satisfies the requirements,...

HTML

A Formal Framework for specifying and Analyzing Liabilities Using Log as Digi...

Despite the effort made to define methods for the design of high quality software, experience shows that failures of IT systems due to software errors remain very...

HTML

Formal approaches for performability analysis of communicating systems : an a...

We are interested in analyzing the performability requirements of mobile communication systems by using model checking techniques. We model these systems using a...

HTML

Modélisation algébrique du dîner des philosophes

International audience

HTML

Apport d'un prototype spécifié en Z dans le redéveloppement d'un outil de test

http://tsi.revuesonline.com/article.jsp?articleId=17760

HTML

ScaleSem : model checking and semantic web

The increasing development of networks and especially the Internet has greatly expanded the gap between heterogeneous information systems. In a review of studies of...

HTML

Proofs by refinement of programs with pointers

The purpose of this thesis is to specify and prove programs with pointers, such as C programs, using refinement techniques. The proposed approach allows a compromise...

HTML

Static analysis with dioids and polynomial ideals

Static analysis aims to verify that programs behave correctly i.e. satisfy safety properties. However, generating properties verified by a program is a difficult...

HTML

From imperative programs to equational logic for correctness verification

Omnipresence of computer systems in modern technological applications makes the question of their reliability essential. In this thesis, we investigate equational...

HTML

Safe Allocation with Aeronautical systems : Modelisation, Verification and Ge...

This thesis aimed at providing a method to model, verify, and generate allocations of embedded systems functions on avionics resources. This method is based on the use...

HTML

A Simulation Framework for the Validation of Event-B Specifications

This thesis aims at the specification, verification and validation of safety-critical systems with formal methods, in particular, with Event-B. We assessed the...