The formal methods area in HRL was a pioneer in developing and deploying an industrial application of model checking on hardware (RuleBase). Since then, formal verification of hardware has matured, and we now face the challenge of applying formal methods to new domains beyond hardware.
The Beyond Hardware project serves as an umbrella for seeking new opportunities for formal methods based on our assets RuleBase PE and ExpliSAT. As part of the project, we are examining:
- Model checking of critical control systems
- Verification of models
- Finding semantic differences between two versions of code to support incremental development
- Software test generation
To support this effort, we are also coordinating an EU project (PINCETTE) starting in July 2010.