How to Debug a Property Proving Counterexample

Property proving with Simulink Design Verifier™ is a static analysis technique that uses formal methods to prove whether a given property will always be valid. This technique can help you formally verify that specific requirements implemented in your design will always be met. If a property is invalidated, a counterexample will be automatically generated for debugging. Learn how to perform property proving with Simulink Design Verifier and see how to debug an automatically generated counterexample with the Model Slicer tool from Simulink Check™.