Second VORACE workshop

11-12 June 2015


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 Thursay 11 and Friday 12 June 2015 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

  • Behcet Acikmese, University of Texas at Austin, USA
  • Andrzej Banaczuk, United Technologies Research Center, Hartford, USA
  • Benoît Bayon, Price Induction, Anglet, FR
  • Menouer Boubekeur, United Technologies Research Center, Cork, IE
  • Eric Feron, Georgia Institute of Technology, Atlanta, USA
  • Khalil Ghorbal, Carnegie Mellon University, Pittsburgh, USA
  • John Hauser, University of Colorado at Boulder, USA
  • Romain Jobredeaux, Georgia Institute of Technology, Atlanta, USA
  • Sriram Sankaranarayanan, University of Colorado at Boulder, USA
  • Timothy Wang, Georgia Institute of Technology, Atlanta, USA


  • Assalé Adjé, IRIT Toulouse, FR
  • Philippe Beaufreton, Safran Electronics Sagem, Massy, FR
  • Olivier Cots, IRIT-ENSEEIHT Univ. Toulouse, FR
  • Pierre-Loic Garoche, ONERA Toulouse, FR
  • Didier Henrion, LAAS-CNRS Univ. Toulouse, FR
  • Florian Many, DGA Toulouse, FR
  • Marc Pantel, IRIT-ENSEEIHT Univ. Toulouse, FR
  • Pierre Roux, ONERA Toulouse, FR
  • Romain Serra, LAAS-CNRS Univ. Toulouse, FR
  • Xavier Thirioux, IRIT-ENSEEIHT Univ. Toulouse, FR


    Thursday, June 11, 2015

  • 10:00-11:00 - A. Banaszuk and M. Boudekeur - Controls, Autonomy, and Intelligent Systems Research at United Technologies Research Center
  • 11:00-12:00 - K. Ghorbal - Formal Verification and Automated Generation of Invariant Sets for Dynamical Systems
  • 14:00-15:00 - B. Bayon - Optimisation and control of aircraft turbofan engines
  • 15:00-16:00 - S. Sankaranarayanan - Template Domains with a Twist

    Friday, June 12, 2015

  • 10:00-11:00 - J. Hauser - Receding Horizon Control of Nonlinear Systems
  • 11:00-12:00 - R. Jobredeaux and T. Wang - Floating-point considerations in control systems and linear programming
  • 14:00-15:00 - B. Acikmese - Convex optimization applications in autonomous systems
  • 15:00-16:00 - E. Feron - Dealing with computation uncertainty in convex optimization

    Talk abstracts


    Speaker: Behcet Ackimese, University Texas at Austin, USA

    Title: Convex optimization applications in autonomous systems


    This presentation will summarize some useful applications of convex optimization in autonomous systems. First we will present updates on our convex optimization based realtime trajectory optimization algorithms, which include a summary of technical results and recent flight testing. Then the presentation will introduce some results on Markov Decision Processes (MDPs) and their applications in autonomous vehicles. The results will include designing randomized policies for finite horizon MDPs and sequentially observed MDPs with safety constraints. Applications of these methods in multi-vehicle autonomous systems will also be discussed.


    Speakers: Dr. Andrzej Banaszuk and Dr. Menouer Boubekeur, United Technologies Research Center, USA and IE

    Title: Controls, Autonomy, and Intelligent Systems Research at United Technologies Research Center


    We will present a broad overview of UTRC.s research initiatives in the software intensive areas of Controls, Autonomy, and Intelligent Systems that were created to conceive, develop and mature a broad range of intelligent systems and capabilities to enhance and support the diverse array of businesses that comprise the United Technologies Corporation in aerospace and building systems. The research, conducted by a diverse team of researchers in robotics, control, applied mathematics, and computer science (in partnership with several leading universities in US and EU) includes:

  • Real-time path planning algorithms for dynamic collision avoidance in an obstacle-rich environment using probabilistic roadmaps and model-predictive control.
  • Navigation with imperfect and intermittent sensors in GPS degraded environments.
  • Collaborative motion planning for multiple aerial and ground robots, trading off mission objectives while satisfying logical/spatial/temporal constraints.
  • Intelligent system design methodology including architectures for autonomy, human-machine systems, and formal verification.
  • Integrated tool-chain for model-based design of Cyber Physical Systems.
  • Cyber security and resiliency for industrial controls applied to smart grids.
  • Intelligent control and diagnostics for energy efficient buildings. We will conclude with research challenge problems of interest to UTRC and discuss collaboration opportunities at the intersection of formal methods, advanced controls, and autonomy.

    Speakers Bio: Dr. Andrzej Banaszuk is a Program Leader of Sikorsky Program Office at United Technologies Research Center. Since joining UTRC in 1997, he has conducted research in analysis, design, and control of dynamical systems applied to jet engines, rotorcraft, electric power networks, and buildings. Since 2000 he has led collaborative multi-university research teams in the area of flow control, control of combustion instabilities, robust design of large uncertain dynamic networks, and autonomy. He is an author of 44 journal papers, 71 conference papers, and 9 patents. From 1999 to 2002, he was an Associate Editor of IEEE Transactions of Controls Systems Technology. He was appointed to serve on the Board of Governors of IEEE Control Systems Society in 2004. For his work on active and passive control of flow instabilities in jet engines he received IEEE Controls Systems Technology Award in 2007. He became an IEEE Fellow in 2011. He was elected to the Connecticut Academy of Science and Engineering in 2015. He holds Ph.D. in EE from Warsaw University of Technology and Ph.D. in Mathematics from Georgia Institute of Technology.

    Dr. Menouer Boubekeur leads the Business Development activities at UTRC Ireland. Since joining UTRC-I in late 2010, he led a number of research projects in areas related to cyber physical systems modeling and analysis. He has co-authored over 40 publications in international journals and conferences in the areas of formal verification, embedded/real-time systems, security and building automation systems. He is a member of the IEEE, has chaired and served as a technical member of the program committees of international conferences, and is a regular reviewer for international journal and conferences. He holds Ph.D. in computer science and an MSc degree in critical systems from the University of Joseph Fourier (Grenoble).


    Speaker: Benoît Bayon, Price Induction, FR

    Title: Optimisation and control of aircraft turbofan engines


    Price Induction is a small company located in the Basque Country, close to the French Aerospace pool. It is designing the smallest turbofan, the DGEN 380. Due to several innovative concepts, simple but uncommon approaches were developed to control this engine. The size and flexibility of this engine makes it the perfect tool to calibrate algorithms, and to do proofs of concepts. It is also used in several famous institutions as a research tool for control and acoustics.

    Price Induction is also involved in several long term research projects on turbine engines.

    This presentation will include the following items.

  • Presentation of the speaker and achievements in embedded optimization in industry.
  • Presentation of the DGEN 380.
  • Presentation of jet engine control, and possible benefits of efficient and robust control algorithms.
  • The DGEN380 as a proof of concept, with a short presentation of a work in progress with the Georgia Tech Team.

    Speaker Bio: Benoit Bayon finished his PhD Thesis on robust estimation in 2012, before joining a technology transfer Institute in Energy industry. After 2 years working on wind energy and Electrical vehicles, he joined Price Induction, as a control system engineer. His duty involves control and turbofan engine modeling.


    Speaker: Eric Feron, Georgia Institute of Technology, USA

    Title: Dealing with computation uncertainty in convex optimization


    I will describe what I believe is a possible way to go forward and robustify the computations involved in convex optimization, when it is to be used in real time. The idea is to rewrite the problem of robust computation of Newton directions as an algebraic problem similar to those encountered in robust control and determine the regions of the feasible space over which robustness margins are sufficiently large to guarantee that computations will not encounter numerical issues.


    Speaker: Khalil Ghorbal, Carnegie Mellon University, USA

    Title: Formal Verification and Automated Generation of Invariant Sets for Dynamical Systems


    We focus on dynamical systems described by ordinary differential equations with polynomial right-hand side. We investigate two questions of interest for those systems: (i) decision procedures for the invariance of semi-algebraic sets---a set described by finite disjunctions of conjunctions of polynomial equalities and inequalities---for a given dynamical system, and (ii) the automated generation of invariant algebraic and semi-algebraic sets. We enumerate and theoretically compare previously reported methods as well the most recent ones. We also empirically assess the practical running performance of such methods on a generic set of benchmarks. Finally, we show how invariant sets could be used for the formal verification of dynamical and hybrid systems as well as controller synthesis. The advantages and limitations of such methods will be clearly established thought out the talk.


    Speaker: Romain Jobredeaux and Timothy Wang, Georgia Institute of Technology, USA

    Title: Floating-point considerations in control systems and linear programming


    Sound verification of functional properties at the level of the code require to take floating-point errors into account: these implementation artifacts arise from the discrepancy between the mathematical model of controllers and optimization algorithms, which are usually studied assuming exact computations in the real field, and their implementation on finite-memory, finite-space machines, which must use approximations. We present our latest findings in the analysis of controllers and linear programming solvers, regarding their continued and guaranteed performance under floating-point computations.


    Speaker: John Hauser, University of Colorado at Boulder, USA

    Title: Receding Horizon Control of Nonlinear Systems


    Effective control of highly nonlinear systems can be accomplished using online optimization where one repeatedly solves a nonlinear optimal control problem on a receding horizon and implements the first portion of the control strategy. Stable behavior of the resulting closed loop system will be obtained provided that the incremental and terminal cost functions have been carefully chosen to be compatible with the system dynamics and an appropriate horizon length has been chosen. In this talk, we will discuss the interplay of cost and dynamics for solvability of the optimal control problem and its impact on stability. After ensuring (local) stability by choice of the cost functional, we also discuss the use of barrier functionals for ensuring the satisfaction of constraints. Key ideas will be illustrated on systems including aircraft and motorcycles.


    Speaker: Sriram Sankaranarayanan, University of Colorado at Boulder, USA

    Title: Template Domains with a Twist


    Template domains are a versatile representation of sets for proving reachability properties of discrete programs, continuous-time dynamical systems and their combination as hybrid systems. In the past decade, the connections between template domain program analysis and optimization techniques have yielded novel approaches such as policy and strategy iteration. However, the entire approach depends intimately on template selection by the user - a process that is specific to the system being analyzed, wherein much remains to be understood.

    In this talk, we present ongoing approach that sidesteps the problem of template selection by allowing the analysis algorithm to modify an initial choice of the template, during the process of the analysis. Our approach first uses a well-known formalization of numerical program analysis as a bilinear feasibility problem, and shows how modifications to templates can be performed as the analysis progresses. Finally, we examine the performance of our approach on some numerical examples to illustrate some of its promising aspects, as well as pitfalls that are being addressed by our ongoing work.

    Joint work with Amin Ben Sassi (University of Colorado, Boulder)