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
c. Benchmarks (ALL)
d. Incremental SMT for funfrog (use) (G,K,S)
e. Unbounded MC (G,K,S)



=====