Project

General

Profile

Feature #3407

Use Z3 for non-determinism check

Added by Anonymous over 2 years ago. Updated over 1 year ago.

Status:
New
Priority:
Normal
Assignee:
-
Category:
-
Target version:
Start date:
05/15/2018
Due date:
% Done:

0%

Estimated time:

Description

Use Z3 for non-determinism check.

After redesign of formal verification in AF3, non-determinism check ended up being implemented using NuSMV.

Consider implementing it using Z3.

History

#1 Updated by Anonymous over 2 years ago

  • Assignee changed from Anonymous to Anonymous

Any comments?

#2 Updated by Anonymous over 2 years ago

  • Assignee changed from Anonymous to Anonymous

I think the only case where this could make sense is for BIG models and only if the current implementation is slow for such cases (SMT is probably way faster than a model checker but this will be only observable in huge models).

#3 Updated by Johannes Eder over 1 year ago

  • Target version changed from AF3 2.14 RC1 (Feature Freeze) to Backlog

Also available in: Atom PDF