Many symbolic program analysis techniques use satisfiability modulo theory (SMT) solvers to verify properties of programs. SMT solvers can provide solutions quicker if they cache their results. GREEN, which is currently integrated into Symbolic Pathfinding (SPF), is a promising SMT memoization solution. The project entails (a) optimization of GREEN's satisfiability checking, (b) improving the model counting and (c) incorporating unit propagation into GREEN.

Student

Jan Taljaard

Mentors

  • Willem Visser
  • Neha Rungta
close

2017