Wiki » History » Revision 7
Revision 6 (Karine Even Mendoza, 13/05/2016 18:08) → Revision 7/27 (Karine Even Mendoza, 13/05/2016 18:08)
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 b. New CBMC - updare the repository c. Benchmarks d. Incremental SMT for funfrog (use) e. Unbounded MC =====