[tooling] meeting notes 23 January 2025 #160
Conversation
some additions related to DO-178
| | Underfined Behaviour Absence | ASIL-D? | [verifast](https://github.com/verifast/verifast) - wip, [creusot](https://github.com/creusot-rs/creusot) - wip, works only for safe rust, [gillian-creusot](wip - not in a usable state, works for unsafe rust), [kani](https://model-checking.github.io/kani/) | | ||
| | Static Analysis Tools | (ask Oreste Bernardi), DAL-A, DAL-B, DAL-C | probably similar to Polyspace, an assesement about what the rust compiler covers is necessary. For DO-178 such tools support the "source code conformity" objective. | | ||
| | Formal Methods | ASIL-D | does this mean more than UB? | |
There was a problem hiding this comment.
I poked around internally.
For line 31, formal methods are more than UB detection. Formal methods is when the properties of the software are rigorously rather than heuristically verified.
Static analysis only means "without execution".
Some formal methods belong to static analysis (static strong typing), some are not (concolic execution).
With that being said, there is no inclusion between Static Analysis tools and Formal Methods. Some static analysis tools work by detecting "suspicious patterns" and do not provide any formal guarantee of the absence of the undesirable property when their patterns are not matched, therefore they cannot be described as “formal methods”, even if some sophisticated implementations of such of these analyzers may borrow tools from formal methods, such as SMT provers.
creusot does not mention undefined behavior at all. It focuses on proving functionnal correctness rather than the absence of UB. It does so by using formal methods, and doesn't run any code.
kani uses model checking and (as I understand it) does not require any execution. It therefore belongs to formal methods and static analysis.
verifast provides deductive verification like creusot while relying on a different approach internally (forward symbolic execution). It is formal methods and a form of static analysis.
I suggest the following edits:
- Move both
creusotandkanito the Static Analysis Tools and the Formal Methods rows - Move
verifastin the Formal Methods row - Delete the Undefined Behavior Absence row
This pull request adds the meeting notes for the meeting from 23 January 2025.
I did not write down the list of attendants (my fault), please feel free do add yourself if you were present. Thank you.