Does "Property Proving" feature in Simulink Design Verifier uses Theorem Proving or Model Checking in the background?

I am using Simulink Design Verifier to test the Stateflow model I developed as a part of my research. I wanted to know whether the "Property Proving" feature in Simulink Design Verifier (SLDV) uses Theorem Proving or Model Checking.

I tried looking for that in the MathWorks documentation but could not find an answer. It would be a great help if you could answer my question.

Answer 1

[MathWorks Support Team]

Please see the following points:

1) "Property Proving" in SLDV is based on two engines, namely Polyspace and Prover Plug-in.

a) The Polyspace engine uses Abstract Interpretation, which in essence computes relations between variables in the model. If the property is implied by those relations it is always true.

b) The approach of Prover Plug-in is Model Checking, in particular k-Induction, which reasons about the reachable state space of the model.

The two engines are complementary. Abstract Interpretation is good for range-like properties but is originally an approach to verify programs. Model Checking reasons about sequences of steps of transition systems, and is thus closer to how Simulink operates. SLDV uses Abstract Interpretation first and usually spends most of the analysis time in Model Checking.

2) Simulink Design Verifier is not based on theorem proving (if by theorem proving you mean proof assistant tools like Coq).

3) Simulink Design Verifier is an automated tool that does not require a user to interact with it.