Programs for small embedded devices are economically important and are more amenable to formal analysis than large software artifacts for general purpose computing. Nevertheless, concurrent programs for small embedded processors create difficult correctness problems related to timing and liveness properties. Unfortunately, automated formal verification using explicit model checking for embedded software using existing algorithms requires prohibativly large amounts of computational resources (even more unfortunately, symbolic model checking techniques for embedded software seem even less useful for this problem due to the asynchrony inherent to embedded software). The verificationand validation lab at BYU is researching algorithms to improve embedded software capability by designing new algorithms for explicit model checking of this software that efficiently find errors and proves correctness.

The design of new algorithms for explicit model checking of embedded software is based on recasting the embedded software verification problem as a parallel graph exploration problem. This is the same approach to explicit model checking which resulted in the now-famous double depth first search algorithm. We chose this approach because embedded software transition graphs have a unique topology that we can leverage to create more efficient search algorithms. New parallel algorithms for embedded software verification can exploit the unique graph structure of embedded software while optimizing for, rather than coping with (as with parallel double DFS), a parallel computational platform.