VERIMAG (Room 206, 2nd floor)
28 October 2016 - 10h00
Verification: Theory and Practice
by J. Esparza, A. Bouajjani, and D. Nickovic from TU Munich, IRIF, Austrian IT
Abstract:
10:00 Javier Esparza, Technical University of Munich, Germany
Limit-Deterministic Automata for Probabilistic Model Checking
Limit-deterministic Büchi automata can replace deterministic Rabin automata in probabilistic model checking algorithms, and can be significantly smaller. We present a direct construction from an LTL formula to a limit-deterministic Büchi automaton. Our translation is compositional and has a clear logical structure. Moreover, due to its special structure, the resulting automaton can be used not only for qualitative, but also for quantitative verification of Markov Decision Processes, using the same model checking algorithm as for deterministic automata. This allows one to reuse existing efficient implementations of this algorithm without any modification. Our construction yields much smaller automata for formulas with deep nesting of modal operators and performs at least as well as the existing approaches on general formulas.
This is a joint work with Stefan Jaax, Jan Kretinsky, and Salomon Sickert.
---------------------------
10:40 Ahmed Bouajjani, IRIF, Univ. Paris Diderot
Linearizability Checking: Reductions to State Reachability
We address the issue of verifying the correctness of libraries of concurrent data structures. We consider the problem of checking whether given implementation is linearisable w.r.t. a sequential abstract specification of the data structure. We overview complexity and decidability results concerning this problem in general, and show cases where efficient reductions of this problem to state reachability problems are possible.
This is a joint work with Michael Emmi, Constantin Enea, and Jad Hamza.
-----------------------------
11:20 Dejan Nickovic, Austrian Institute of Technology
Monitoring Analog and Mixed-Signal Designs Emulated on FPGA
To avoid the simulation bottleneck in verification and testing of analog and mixed-signal (AMS) circuits, designers use an emulation-based approach: the designed system model is replaced with an early prototype implemented on FPGA which allows significantly longer tests. However, verification techniques used with the emulation-based approach involve many manual, thus error prone and time consuming tasks.
We propose to improve the verification techniques for this approach by combining design emulation with assertion-based runtime verification using Signal Temporal Logic (STL) as a specification language, because of its rigorous formal semantics and support for describing complex timing relations between analog and digital signals. Originally, STL monitors distinguish between good and the bad behaviors but this binary classification may not be sufficiently informative for analog signals. We therefore implement a quantitative extension of STL monitors that measure the robustness degree of an assertion with respect to a behavior and indicate how far is the behavior from satisfying or violating the requirement. We illustrate our monitors on case studies from the automotive application domain.
This is joint work with Ezio Bartocci, Radu Grosu, Stefan Jaksic and Thang Nguyen.
On the occasion of the thesis defense of Thomas Ferrere
