In order to apply formal methods in practice, the practitioner has to comprehend a vast amount of research literature and realistically evaluate practical merits of different appr...
This paper presents an experience report on the specification and the validation of a real case study in the context of the industrial CRISTAL project. The case study concerns a pl...
Samuel Colin, Arnaud Lanoix, Olga Kouchnarenko, Je...
Lustre is a formal synchronous declarative language widely used for modeling and specifying safety-critical applications in the elds of avionics, transportation or energy productio...
Virginia Papailiopoulou, Laya Madani, Lydie du Bou...
There has been relatively little work on the implementability of timing requirements. We have previously provided definitions of fundamental timing operators that explicitly consid...
Abstract. In this paper we propose a certification technique for noninterference of Java programs based on rewriting logic, a very general logical and semantic framework efficientl...
Different approaches have been developed to mitigate the state space explosion of model checking techniques. Among them, symbolic verification techniques use efficient representati...
Given the intractability of exhaustively verifying software, the use of runtime-verification, to verify single execution paths at runtime, is becoming popular. Although the use of ...
Christian Colombo, Gordon J. Pace, Gerardo Schneid...