Project

General

Profile

Actions

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)

Updated by Antti Hyvärinen over 8 years ago · 1 revisions