Wiki » History » Revision 8
Revision 7 (Karine Even Mendoza, 13/05/2016 18:08) → Revision 8/27 (Karine Even Mendoza, 13/05/2016 20:24)
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
> - 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
d. Incremental SMT for funfrog (use)
e. Unbounded MC
=====