[Discourse.ros.org] [ROS Projects] Formal verification of ROS nodes using Imandra reasoning engine

classic Classic list List threaded Threaded
1 message Options
Reply | Threaded
Open this post in threaded view
|

[Discourse.ros.org] [ROS Projects] Formal verification of ROS nodes using Imandra reasoning engine

Tully Foote via ros-users


Hello! We at [Aesthetic Integration](https://www.imandra.ai/) are developing tools and techniques for formal verification of distributed systems. For our ROS-related project, we are working on OCaml client for ROS and we are creating tools and wrappers that allow one to formally reason about ROS node models. With our [Imandra](https://www.imandra.ai/) reasoning engine you can formally verify statements about models written in OCaml, and the same model can be compiled and executed as a ROS node.

Check our medium post:[https://medium.com/imandra/imandra-interface-to-robot-os-part-i-9f3888c5c3a1](https://medium.com/imandra/imandra-interface-to-robot-os-part-i-9f3888c5c3a1) where we are describing our approach to the creation of a simple model of a ROS node.





---
[Visit Topic](https://discourse.ros.org/t/formal-verification-of-ros-nodes-using-imandra-reasoning-engine/5655/1) or reply to this email to respond.


If you do not want to receive messages from ros-users please use the unsubscribe link below. If you use the one above, you will stop all of ros-users from receiving updates.
______________________________________________________________________________
ros-users mailing list
[hidden email]
http://lists.ros.org/mailman/listinfo/ros-users
Unsubscribe: <http://lists.ros.org/mailman//options/ros-users>