Re: [eclipse-pmc] [CQ 11173] The Omega Project version 2.1 for modeling.

["Daniel Megert" <daniel_megert@xxxxxxxxxx>]

Hi

This is the wrong PMC. You need to send
this to the Modelling PMC (modeling-pmc@xxxxxxxxxxx).

Dani



From:      
 "-- Boutheina"
<boutheina.bannour@xxxxxxxxx>
To:      
 eclipse-pmc@xxxxxxxxxxx
Cc:      
 arnault.lapitre@xxxxxx
Date:      
 11.05.2016 09:08
Subject:    
   [eclipse-pmc]
[CQ 11173] The Omega Project version 2.1 for        modeling.efm
discussion
Sent by:    
   eclipse-pmc-bounces@xxxxxxxxxxx

---

Hi

Please find below our justification on the use of Omega solver, required
by the IP team. Cheers.

// In a nutshell, Omega is used only by one Formal Analysis Module (FAM)
in
efm-symbex which is optional: the symbolic execution kernel is completely
independent, FAM modules are as plug-ins for the efm-symbex. In fact no
other
FAM modules is concerned. Users can activate (a) FAM module(s) upon need.
Note
that FAM modules can make use of existing tools such as constraint solvers
Omega, CVC4, Z3, Yices… We have tried to our best to choose the solvers
that
are EPL compliant (e.g. we suppressed Yices and kept Z3 whose license changed
recently). Now if using Omega in this module causes a license issues, we
can
remove the dependency to Omega and keep the module functioning with other
solvers.

Inline responses:

1.      how this code is used by the project:
The FAM module “behavior redundancy detection” may use solvers functions
to
compare two behaviors equivalence. Using Omega in this module is optional
(as
using any other solver). We can remove the dependency to Omega (the include
omega.h in C++…).

2.      what parts of the project depend on this: 
The formal analysis module “behavior redundancy detection”

3.      what all doesn't function without it:
The formal analysis module “behavior redundancy detection” is concerned,
the
other FAM modules and the symbolic execution kernel are not. 


BlackBerry®
_______________________________________________
eclipse-pmc mailing list
eclipse-pmc@xxxxxxxxxxx
To change your delivery options, retrieve your password, or unsubscribe
from this list, visit
https://dev.eclipse.org/mailman/listinfo/eclipse-pmc