mercredi 13 Septembre, 9h-12h en salle Métivier
Matinée d'exposés à l'occasion de la soutenance de Ayman Aljarbouh
Verification des systèmes cyber-physiques
[Annulé] Models, Over-approximations and Robustness
Eugenio Moggi, DIBRIS, Univ. di Genova
Hybrid systems, and related formalisms, have been successfully used to model Cyber-Physical Systems. However, mathematical models are always a simplification of the system they are meant to describe, and one must aware of this mismatch, when using these models to analyze a system. In safety analysis it is acceptable to use over-approximations of the system behavior, indeed they are the bread and butter of counterexample guided abstraction refinement (CEGAR). We propose a notion of system behavior robust wrt arbitrary small over-approximations, and argue that it is particularly appropriate for safety analysis
9:45-10:30 SMT Solving for Real Algebra
Erika Abraham, RWTH Aachen University
Satisfiability checking is a relatively young research area, aiming at the development of algorithms and tools for checking the satisfiability of existentially quantified logical formulas. For propositional logic, in the late '90s impressive progress was made towards practically applicable solutions, resulting in powerful SAT solvers. Driven by this success, a new line of research started to enrich propositional SAT solving with solver modules for different theories. Nowadays, sophisticated SAT-modulo-theories (SMT) solvers are available also for algebraic problems, partly based on decision procedures rooted in symbolic computation. In this talk we give a brief introduction to SMT solving, discuss relations to symbolic computation, and illustrate the potentials and obstacles for embedding symbolic computation techniques in SMT solvers on the example of the cylindrical algebraic decomposition.
10:45-11:30 Guaranteed simulation of nonlinear continuous-time dynamical systems using interval methods
Luc Jaulin, Lab-STICC, UBO, Brest
We consider dynamical systems that can be expressed by nonlinear differential equations. The system may be uncertain and all uncertainties are assumed to be bounded. We are interested in simulating the system and computing an envelop containing all feasible trajectories in order to guarantee that no forbidden events will occur. In this presentation, I will propose two approaches, both based on interval analysis and constraint propagation. The first approach is Lagrangian and is based on the notion of ‘tubes' which are intervals o trajectories. Interval Lagrangian methods discretize the time space and can be efficient in high dimensions, but are very conservative. The second approach is Eulerian, and is based on the notion of 'mazes' which are intervals of paths. Interval Eulerian methods discretize the state space. They are accurate and can deal with small dimensional systems. They can for instance detect limit cycles and can deal efficiently with zeno behaviors. Finally, I will show how these two approaches can be combined. Some test-cases will be presented in order to illustrate the efficiency of the approaches.
Exposés des semaines suivantes
jeudi 21 Septembre, 14h en salle Aurigny
Deian Stefan (UCSD)
Practical multi-core information flow control
Large-scale private user data theft has become a common occurrence. A huge factor in these privacy breaches we hear so much about is that developers specify and enforce data security policies by strewing checks throughout their application code. Overlooking even a single check can lead to vulnerabilities. In this talk, I will describe a new approach to protecting sensitive data even when application code is buggy or malicious. The key ideas behind our approach are to separate the security and privacy concerns of an application from its functionality, and to use language-level information flow control (IFC) to enforce policies throughout the code. This talk will cover our recent work on LIO, a language-level IFC system, and its use in Hails, a server-side web framework that makes it easy to specify policies in a declarative way. I will particularly focus on the key challenges of designing an IFC system that can run on multiple cores without leaking information, and can simultaneously leverage formal semantics to rule out large classes of design error.
jeudi 12 Octobre, 14h en salle Minquiers (B025)
Why Liveness for Timed Automata Is Hard, and What We Can Do About It
The liveness problem for timed automata asks if a given automaton has a run passing infinitely often through an accepting state. We show that unless P=NP, the liveness problem is more difficult than the reachability problem; more precisely, we exhibit a family of automata for which solving the reachability problem with the standard algorithm is in P but solving the liveness problem is NP-hard. This leads us to revisit the algorithmics for the liveness problem. We propose a notion of a witness for the fact that a timed automaton violates a liveness property. We give an algorithm for computing such a witness and compare it with the existing solutions.
jeudi 26 Octobre, 14h en salle Aurigny