一部のロボットコントローラーが、一連の述語で定義する障害状態に到達しないことを証明することに興味があります。それを実現するためのオープンソースソフトウェアツールがあることを私は知っています。たとえば、BLAST（Berkeley Lazy Abstraction Software Verification Tool）について聞いたことがありますが、他に、より簡単に使用できる、および/または特定のアプリケーションを対象としたものを知っていますか？
プロジェクトの1つでBLASTまたは別のそのようなツールを使用したことがありますか。また、そのようなツールを展開するために必要な労力よりもメリットが大きいと思いますか。
Frama-Cが役立つかもしれません。
Frama-C開発者ではない人による評価については、これら2つの記事を参照してください。安全性が重要なコード（DO-178BレベルAなど）を開発しているエンジニアの中には、投資する価値のある最も弱い前提条件手法に基づく正式な注釈と分析を見つけた人もいますが、従来のテストは非常に費用がかかります。この最後のリンクは、Frama-Cがやがて交換する予定のクローズドソースアナライザーであるCaveatに関するものです。
あなたの質問は、おそらくFrama-CのAoraïプラグインに感謝するかもしれないように聞こえます。
これがあなたのケースでいつもうまく費やされているかどうかは、おそらくあなたがこれらのテクニックについて学ぶことを喜びか雑用かを考えるかどうかの問題です。