hifrog

h1. 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)

=====

h1. Work Plan - Meeting 9-11/05/2016

h2. 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)

h3. Tasks for OpenSMT2

#   Library + Headers (A,L)

#   Interface (ALL)

#   Interpolation (L,S)

#   Incrementality - Push/Pop (M,A)

#   Parallelizaion and clause sharing between theories (M,A)

5.5 Theory combinations (L,A)

5.6 Full define - fun for OpenSMT2, with parameteres (?)

#   Quantifiers (G,A,M)

h3. 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)

=====