search

seahorn / seahorn

SeaHorn Verification Framework
http://seahorn.github.io/
Other
441 stars 131 forks source link

Supporting real domain #102

Closed ezudheen closed 6 years ago

ezudheen commented 7 years ago

I would like to know whether Seahorn support verification of programs in the real domain. I understand that Z3 can verify the VCs in the real domain. I would like to know how we can modify the VC generation to support real domain.

caballa commented 6 years ago

Are you interested in reals or floating points (FP)? We have a private branch that allows SeaHorn to do BMC on floating points. It has not been tested but we could make it public. Invariant generation on FP is something very interesting but we have not tried yet.

ezudheen commented 6 years ago

It will be very helpful for me if the implementation of reals or floating points (FP) made public. Actually, I am trying to verify Simulink models (discrete controller + continuous plant). My idea is to generate Verification conditions (real domain) in smt2 format.

caballa commented 6 years ago

If you care about Simulink you should check out this project https://github.com/coco-team/cocoSim

cocoSim verifies Simulink code by translating to Horn clauses and it uses Spacer among other solvers. I'm not sure SeaHorn can be helpful here since SeaHorn is for analysis of C/C++ programs.

ezudheen commented 6 years ago

We are converting Simulink models into C programs (Simulink automatically do it for the controller part) and verifying the program. I will look into this project and check its suitability for our approach.