Program Analysis Tools

The goal is to compute symbolic post-image for controller programs in ROS for synthesizing assumptions on the interfacing variables/ROS messages.

The idea is to reuse existing program analysis tools for C++ or Python. At the best case, we only need to analyze the callback functions for ROS subscribers and the loop for periodically publishing messages using ROS publishers.


  • Software Analysis Workbench by Galois Inc.
  • SPARTA by Facebook
  • IKOS by NASA
  • CBMC


  • CrossHair

Some Features to Look for

  • How to instrument or annotate to only analyze part of a ROS package. The fewer instrumentation needed the better.
  • How to add pre/post conditions or approximations for complicate/uninterpreted functions such as trigonometry functions or ellipsoids
  • Floating point numbers or real numbers
  • Support matrix and linear algebra?

Simulated Autonomous Systems for Case Studies


  • Lane keeping (vision, dynamics)
  • Crop row following (vision)
  • Vision-based fixed-wing aircraft landing (vision, dynamics)
  • UTM (dynamics, coordination)
  • ARIAC smart manufacturing (dynamics, coordination)



  • Drone racing (vision, dynamics)
  • Vision-based drone formation (vision, dynamics, coordination)