Repair and Generation of Formal Models Using Synthesis
Writing a formal model is a complicated and time-consuming task.
Synthesis
Interactive Model Repair by Synthesis
When using B or Event-B for formal specifications, model checking is often used to detect errors such as invariant violations, deadlocks or refinement errors.