Research Papers

Fribourg Laurent and Romain Soulat. Stable Limit Cycles for Sampled Switched Systems

We show that, for a controlled switched system with contractive modes and a known stabilization zone R, for each starting point x0 in R, there is a stable limit cycle C to which the trajectory issued from any point of R converges, and that C intersects with R. The interest of this result is illustrated on the boost DC-DC converter example.

Susmit Jha and Sanjit A. Seshia. From Verification to Synthesis of Fixedpoint Implementation of Numerical Software Routines

In this paper, we present an automated technique swati: Synthesizing Wordlengths Automatically Using Testing and Induction, which uses a combination of Nelder-Mead optimization based testing, and induction from examples to automatically synthesize optimal fixedpoint implementation of numerical routines. The design of numerical software is commonly done using floating-point arithmetic in design-environments such as Matlab. However, these designs are often implemented using fixed-point arithmetic for speed and efficiency reasons especially in embedded systems. The fixed-point implementation reduces implementation cost, provides better performance, and reduces power consumption. The conversion from floating-point designs to fixed-point code is subject to two opposing constraints: (i) the word-width of fixed-point types must be minimized, and (ii) the outputs of the fixed-point program must be accurate. In this paper, we propose a new solution to this problem. Our technique takes the floating-point program, specified accuracy and an implementation cost model and provides the fixed-point program with specified accuracy and optimal implementation cost. We demonstrate the effectiveness of our approach on a set of examples from the domain of automated control, robotics and digital signal processing.

Pierre Roux and Pierre-Loic Garoche. A Polynomial Template Abstract Domain based on Bernstein Polynomials

The analysis of reactive systems such as the command control of aircrafts requires the ability to analyze nonlinear systems and synthesize nonlinear invariants. However, in the static analysis state of the art, few analyses are applicable or effective when applied to those systems. We present a template abstract domain that relies on Bernstein polynomials to bound the reachable states of polynomial reactive systems with polynomial invariants.

Extended Abstract

Xiaoqing Jin, Alexandre Donzé and Gianfranco Ciardo. Mining Weighted Requirements from Closed-Loop Control Models

Specification defects have been a nightmare for engineers. We propose a new weighted requirement mining framework to address this problem. We define weighted and parametric weighted signal temporal logic (STL) as the underlying formalism to improve the expressiveness. This also improves convergence of the mining process. We provide some primitive results to show the benefit of the new framework.