Credible Autocoding and Verification of Embedded Software (CrAVES)

Critical control software is becoming increasingly complex and certification standards increasingly high. In this 
context, it becomes necessary to drive certification costs down while improving safety assurance. We 
provide a development framework, which draws from control  theory concepts and formal analysis to offer a 
credible, automated control software generation tool. This endeavor, at the intersection of control theory 
and computer science, aims at bringing together the 2 communities and facilitating their interaction. Indeed 
it is believed domain specific knowledge can prove itself invaluable in the certification and analysis of 
generated software.

The challenges are numerous:

  • Providing controller designers with easy ways of including stability and performance proofs to their 
  • controller diagrams.
  • Coming up with a semantic to express stability and performance properties at the level of the code and 
  • potentially at intermediate levels of representation of the controller.
  • Developing a compiler able to translate these proofs and properties along with the actual controller.
  • Study the effect of various model transformations on the validity of the proof (e.g. from an abstraction standpoint):
      • Discretization
      • Floating-point arithmetic
      • Machine-level constructs (pointers)
  • Replaying the proofs down at the level of the code in an automatic fashion.
  • As the model gets closer to implementation, handle artifacts of concretization such as array bound checks and pointer de-referencing.



Eric Feron's picture
Eric Feron
Decision and Control Laboratory
Georgia Institute of Technology


Jack Riderhof
Dynamics and Control Systems Laboratory
Georgia Tech



Wang, T., A. E. Ashari, R. J. Jobredeaux, and E. M. Feron, "Credible autocoding of fault detection observers", American Control Conference (ACC), 2014, June, 2014. PDF icon acc2014.Wang_.Ashari.Jobredeaux.Feron_.printed.pdf (412.19 KB)
Wang, T., R. J. Jobredeaux, M. Pantel, P-L. Garoche, E. M. Feron, and D. Henrion, "Credible Autocoding of Convex Optimization Algorithms", CoRR, vol. abs/1403.1861, 2014. PDF icon corr2014.wang_.et_.al_.pdf (634.67 KB)


Herencia-Zapana, H., R. J. Jobredeaux, S. Owre, P-L. Garoche, E. M. Feron, G. Perez, and P. Ascariz, "PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL", NASA Formal Methods, 2012. PDF icon nfm2012.Zapana.Jobredeaux.Feron_.etal_.submitted.pdf (350.66 KB)


Jobredeaux, R. J., T. Wang, and E. M. Feron, "Autocoding control software with proofs I: Annotation translation", Digital Avionics Systems Conference (DASC), 2011 IEEE/AIAA 30th, oct., 2011. PDF icon 06096122.pdf (294.45 KB)

Dynamics and Control Systems Lab


Robotic Mobility Group


Aerospace Robotics and Embedded Systems Laboratory

About us

We are three research groups from Georgia Tech, the Massachusetts Institute of Technology, and the University of Southern California, collaborating to perform basic research on high-speed autonomous driving.  We are most interested in researching biologically-inspired methods in the realms of both perception and control.


This work was supported by the Army Research Office under MURI Award W911NF-11-1-0046.