Third VORACE workshop

20-22 September 2016
Toulouse

Scope

The workshop is organized within the scope of the VORACE project. Topics include optimization, systems control and formal methods in computer science.

Date and venue

The workshop takes place on Tuesday 20, Wednesday 21 and Thursday 22 September 2016 in room F501 (salle du conseil) at ENSEEIHT, 2 Rue Charles Camichel, 31000 Toulouse, an engineering school located in the historical city center of Toulouse (nearest metro station: François Verdier). Room F501 is located in building F. To access this building, please register at the entrance lodge of ENSEEIHT, showing up a national identification card or a passport.

Invited speakers

  • Behçet Açıkmeşe, University of Washington, Seattle, USA
  • Assalé Adjé, University of Perpignan, France
  • Guillaume Davy, ONERA Toulouse, France
  • Eric Feron, Georgia Institute of Technology, Atlanta, USA
  • John Hauser, University of Colorado at Boulder, USA
  • Mioara Joldeş, LAAS-CNRS Toulouse, France
  • Mihai Putinar, University of California at Santa Barbara, USA
  • Pierre Roux, ONERA Toulouse, France
  • Lieven Vandenberghe, University of California at Los Angeles, USA

    Participants

  • Pierre Apkarian, ONERA Toulouse, FR
  • Serban Belinschi, IMT-CNRS Univ. Toulouse, FR
  • Laura Dal Col, LAAS-CNRS Univ. Toulouse, FR
  • Simon Duverger, ONERA Toulouse, FR
  • Pierre-Loïc Garoche, ONERA Toulouse, FR
  • Didier Henrion, LAAS-CNRS Univ. Toulouse, FR
  • Jean-Baptiste Hiriart-Urruty, Univ. Paul Sabatier Toulouse, FR
  • Roxana Hess, LAAS-CNRS Univ. Toulouse, FR
  • Cédric Josz, LAAS-CNRS Univ. Toulouse, FR
  • Jean Bernard Lasserre, LAAS-CNRS Univ. Toulouse, FR
  • Erik Martin-Dorel, IRIT-UPS Univ. Toulouse, FR
  • Marc Pantel, IRIT-ENSEEIHT Univ. Toulouse, FR
  • Philippe Queinnec, IRIT-ENSEEIHT Univ. Toulouse, FR
  • Aneel Tanwani, LAAS-CNRS Univ. Toulouse, FR
  • Xavier Thirioux, IRIT-ENSEEIHT Univ. Toulouse, FR
  • Victor Vinnikov, Ben Gurion Univ. Negev, Be'er Sheva, IL
  • Tim Wang, United Technologies Research Center, Hartford, USA
  • Tillmann Weisser, LAAS-CNRS Univ. Toulouse, FR

    Schedule

    Tuesday, September 20, 2016

  • 14:00-15:00 - Lieven Vandenberghe - Sparse matrix theory and semidefinite optimization

    Sparsity in the coefficients of a semidefinite program has important implications for the structure (sparsity and rank) of the solutions of the problem. The talk will focus on applications of classical results in sparse matrix theory, and, in particular, the fact that, for chordal sparsity patterns, zero-fill Cholesky factorizations, maximum-determinant and minimum-rank positive semidefinite completions, and minimum-dimension Euclidean distance matrix completions are simple to characterize and easy to compute. These properties are very useful in theoretical analysis and algorithm development for semidefinite optimization. Data structures and techniques familiar from the sparse matrix literature, such as elimination trees, supernodal elimination trees, and multifrontal algorithms, will play a central role in the derivation of the key results and algorithms.

  • 15:00-16:00 - Pierre Roux - Validating Numerical Semidefinite Programming Solvers for Polynomial Invariants

    Semidefinite programming (SDP) solvers are increasingly used as primitives in many program verification tasks to synthesize and verify polynomial invariants for a variety of systems including programs, hybrid systems and stochastic models. On one hand, they provide a tractable alternative to reasoning about semi-algebraic constraints. However, the results are often unreliable due to ``numerical issues'' that include a large number of reasons such as floating-point errors, ill-conditioned problems, failure of strict feasibility, and more generally, the specifics of the algorithms used to solve SDPs. These issues influence whether the final numerical results are trustworthy or not. In this paper, we briefly survey the emerging use of SDP solvers in the static analysis community. We report on the perils of using SDP solvers for common invariant synthesis tasks, characterizing the common failures that can lead to unreliable answers. Next, we demonstrate existing tools for guaranteed semidefinite programming that often prove inadequate to our needs. Finally, we present a solution for verified semidefinite programming that can be used to check the reliability of the solution output by the solver and a padding procedure that can check the presence of a feasible nearby solution to the one output by the solver. We report on some successful preliminary experiments involving our padding procedure.

  • 16:30-17:30 - Guillaume Davy - Software verification of an interior point method algorithm

    The efficiency of modern optimization methods, coupled with increasing computational resources, has led to the possibility of real-time optimization algorithms acting in safety critical roles. There is a considerable body of mathematical proofs on on-line optimization programs which can be leveraged to assist in the development and verification of their implementation. To demonstrate this we wrote a C implementation of a primal algorithm solving a small linear problem. We annotated this small example with proof elements in a specific language call ACSL. Using this language enable a software call Frama-C to guarantee that the C code is satisfying all the property stated as annotation such as termination or correctness.

    Wednesday, September 21, 2016

  • 10:00-11:00 - Behçet Açıkmeşe - Convex Optimization Approach to Synthesis of Controlled Markov Chains with Autonomous Vehicle Applications

    This talk will focus on using theory of controlled Markov chains to synthesize higher-level control laws for autonomous systems, particularly multi-agent autonomous systems, e.g., swarms. The proposed approach specifies the time evolution of the probability density distribution of the vehicles by using a Markov chain, which guides the vehicles to a desired steady-state distribution, while satisfying the prescribed ergodicity, motion, and safety constraints. We present convex optimization methods for both offline and online Markov chain synthesis. We extend these results to Markov Decision Processes (MDPs), and present results on safety constrained MDP policy synthesis. We also incorporate additional observations for instantaneous transitions in MDPs, to extend the convex MDP synthesis results to vehicles with ON/OFF observation modes.

  • 11:00-12:00 - John Hauser - On the Formation Rejoin Problem

    We consider the problem of a maneuvering vehicle performing a rejoin to close formation with another maneuvering vehicle. The dynamics of relative position and velocity is shown to be governed by a linear time varying dynamics. Using rotationally invariant potential functions to exploit the symmetry present in the dynamics, we are able to construct Lyapunov functions that, along with their time derivative, are independent of time allowing us to conclude, in the case of linear feedback, exponential stability of the time varying closed loop system. The situation with nonlinear feedback is somewhat more delicate, requiring the use of Matrosov's theorem to prove uniform global asymptotic stability. Performance of the approach is illustrated by rejoining to an aggressively maneuvering flight leader using a saturating control law.

  • 14:00-15:00 - Mihai Putinar - Positivity Certificates

    I will review some known positivity certificates for real polynomials or more general function algebras. Then I will discuss some challenging questions involving positive polynomials: The BMV conjecture and its recent solution by Stahl, Crouzeix bound for the numerical range of functions of matrices and some geometrical aspects of Cauchy-Riemann manifolds.

  • 15:00-16:00 - Mioara Joldeş - Validated numerics for robust space mission design

    In this talk we present an overview of several symbolic-numeric algorithms and software tools developed for applications in optimal control and robust space mission design. We aim at providing computer-aided proofs of numerical values, with validated and reasonably tight error bounds, without sacrificing efficiency. We focus on two applications. Firstly, due to the large amount of debris, we consider the computation of collision probabilities between space objects in low Earth orbits. Secondly, we consider the spacecraft rendezvous problem: under certain assumptions, we are interested in designing a fuel-optimal maneuvers plan, which takes one active spacecraft, originally moving on an initial orbit, to the final reference orbit of a passive target spacecraft e.g., International Space Station. In these applications, we particularly make use of properties of D-finite functions (solutions of linear differential equations with polynomial coefficients) and analytic or validated bounds on truncation errors for power or Chebyshev series. This talk is based on joint works with D. Arzelier, F. Bréhard, N. Brisebarre, J.-B. Lasserre, C. Louembet, A. Rondepierre, B. Salvy, R. Serra.

    Thursday, September 22, 2016

  • 10:00-11:00 9:00-10:00 - Eric Feron - Command and control software for safety critical cyber-physical systems: Carrying the burden of proof

    From 1930 to 1960, command and control systems were implemented electro-mechanically and evidence of proper behavior were written by hand.

    From 1960 to 2000, command and control systems were implemented on a computer and evidence of proper behavior, though sometimes computed with the help of a computer, were still written by hand.

    From 2000 onwards, command and control systems are still implemented on a computer. This talk argues that evidence of proper behavior is necessary and should now be written by a computer. To support this view, the case of classical control systems will be considered first, followed by convex optimization algorithms that can be used for advanced vehicle guidance. The development of a dedicated and formal, computer-ready meta-language supporting the expression of proofs of proper behavior of these systems will be discussed in conjunction with existing general mathematical reasoning languages. Practical examples will be discussed to root this research topic into real-life systems and concerns.

  • 11:00-12:00 10:30-11:30 - Assalé Adjé - Quadratic templates revisited

    A combination of a policy iterations algorithm and quadratic templates was proposed in 2010 to represent reachable values set of linear systems as an intersection of ellipsoids. However, this combination suffered from the fact that the quadratic templates had to be provided by the user. Then in 2014, an automatic generation of quadratic templates from quadratic Lyapunov functions was proposed. In this talk, we present a new automatic construction of quadratic templates. Each template is associated to a coordinate of the state-variable and minimizes a quadratic optimization problem. This new construction coupled with the policy iterations algorithm leads to a tighter representation of the reachable values set.