2009 Research Summary

A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance

View Current Project Information

Sanjit A. Seshia, Wenchao Li and Orna Kupferman

Microelectronics Advanced Research Corporation and Gigascale Systems Research Center

To achieve certifiable error resilience, we need a good quality formal specification. Our current work addresses this problem from both theoretical and practical standpoints. On the theoretical side, we show that fault tolerance and specification coverage are dual problems. In addition, we have developed a theory of mutations for reasoning specification coverage in the context of fault tolerance. On the practical side, we exploit this duality and the aggressiveness order amongst mutations to iteratively strengthen specifications. We demonstrated our technique with formal verification of a Wormwhole Virtual Channel Router in Verilog as well as a subset of the VIS benchmarks. Results indicate that we are able characterize specification coverage precisely with respect to mutations, and automatically improve specifications in the case of low coverage.

[1]

O. Kupferman, W. Li, and S. A. Seshia, On the Duality between Vacuity and Coverage, UC Berkeley EECS Department Technical Report, March 31, 2008.

[2]

O. Kupferman, W. Li, and S. A. Seshia, "A Theory of Mutations with Applications to Vacuity, Coverage, and Fault Tolerance," Formal Methods in Computer Aided Design, November 2008 (to appear).