ABSTRACT. Hybrid automata are mathematical model designed to describe systems characterized by mixed discrete-continuous behaviours.

Standard semantics defined over hybrid automata implicitly assume perfect knowledge of the observed systems and infinite precision measurements. In the biological context these assumptions are unrealistic and often lead to unfaithful models.

From these observations, we introduce a family of more flexible semantics, the ε-semantics, able to handle noise, partial information, and finite precision.

In this presentation we study the relationship between ε-semantics and standard semantics over first order formulae used to construct logic-based hybrid automata. Under this framework, we present a decidability result concerning the reachability problem. Finally, we consider some biological models and show the qualitative benefits brought by the ε-semantics application.

ABSTRACT. We are developing a new approach for debugging and verifying floating-point implementations of nonlinear functions. Our method combines testing, numerical analysis, and delta-complete SMT solving using dReal. We generate point inputs to obtain preliminary coverage, and then generalize them to an automatically chosen neighborhood based on static analysis. In this way we often obtain full coverage of bounded intervals of interest in reasonable amount of time. Applying the techniques on the current version of the Embedded GNU C library, we have found serious bugs in the implementations of elementary functions, as well as intervals where their correctness is verified.

ABSTRACT. Interval computations are a means to guarantee a possible range of a numerical result computed with finite precision numbers. With a parallel implementation, the non-determinism of the execution order, which hinders the reproducibility of numerical result from one run to the other, may also affect the correctness of an interval algorithm. In addition, implementations of interval algorithms depend on the respect of the rounding mode by the software stack: from the compiler to the thread manager. The talk illustrates these pitfalls with the parallel implementation of interval matrix multiplications.

ABSTRACT. Verification and validation (V&V) for industrial control designs can be a difficult and expensive process. Simulation-guided approaches offer a practical means of performing V&V for industrial applications. One such technology uses simulation traces to discover Lyapunov functions or barrier certificates. This technique has proved promising; however, there are challenges related to the numerical computations involved. For example, the technique translates data obtained from simulation traces into a large collection of linear constraints, but not all of these constraints are necessarily useful for solving the problem. Strategies for selecting an appropriate subset of these constraints are required. In this talk, we present an overview of the simulation-guided analysis approach and discuss these numerical challenges.