salle A. Turing CE4
7 December 2015 - 14h00
Verifying a Real-Time Language with Constraints
by Anicet Bart from École des Mines de Nantes / LINA
Abstract: Formal verification of real time programs, where variables can be assigned different values at every single time, is difficult due to the analyses of loops with time lags. In this talk, we consider a problem arising from verification of real- time languages: checking of the range of stream variables. We present a constraint model for this problem, and an algorithm, combining constraint propagation and an ad hoc-solving method, for solving it. We apply our method to the FAUST language, a language for processing audio streams.
