Skype Meeting 17/05/2016

Skype Meeting 03/05/2016¶

Why we need combination of theories, multipication of non-constants

Short Code example:
t1 = x*y;
x' = x;
y'= y;
t2 = x'*y';
assert(t1 != t2);

Solution: t1 = f(x, y)

=====

Work Plan - Meeting 9-11/05/2016¶

Mile-Stones¶

I. Propositional logic MC for FunFrog + OpenSMT2
Tasks (1) - (3)

II. Theories MC for FunFrog + OpenSMT2/Other
Tasks (1) - (3)

III. Theory aware MC for FunFrog + OpenSMT2
Tasks (1) - (4) and (5.5)

IV. Incremental SMT for FunFrog
Tasks (1) - (4)

V. Unbounded MC (loops)
Tasks (1) - (4)

Tasks for OpenSMT2¶

1. Library + Headers (A,L)
2. Interface (ALL)
3. Interpolation (L,S)
4. Incrementality - Push/Pop (M,A)
5. Parallelizaion and clause sharing between theories (M,A)
   5.5 Theory combinations (L,A)
   5.6 Full define - fun for OpenSMT2, with parameteres (?)
6. Quantifiers (G,A,M)

Tasks for Funfrog¶

a. Encoding SSA --> theory (L,K,S)

- Convert SSA --> PTRef (propositional logic)
- Convert Itp --> funfrog (propositional logic)
- Convert SSA --> PTRef (theories)
- Convert Itp --> funfrog (exprt theory)

b. New CBMC - updare the repository (G,K)
c. Benchmarks (ALL)
d. Incremental SMT for funfrog (use) (G,K,S)
e. Unbounded MC (G,K,S)

=====