SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

Applied Formal Logic: Searching in Strings

by Yannick Moy in Dev Projects, Formal Verification – June 29, 2017

A friend pointed me to recent posts by Tommy M. McGuire, in which he describes how Frama-C can be used to functionally prove a brute force version of string search, and to find a previously unknown bug in a faster version of string search called quick search. Frama-C and SPARK share similar history, techniques and goals. So it was tempting to redo the same proofs on equivalent code in SPARK, and completing them with a functional proof of the fixed version of quick search. This is what I'll present in this post.