Lifting CDCL to template-based abstract domains for program verification

The success of Conflict Driven Clause Learning (CDCL) for Boolean satisfiability has inspired adoption in other domains. We present a novel lifting of CDCL to program analysis called Abstract Conflict Driven Learning for Programs (ACDLP). ACDLP alternates between model search, which performs over-ap...

Полное описание

Библиографические подробности
Главные авторы: Mukherjee, R, Schrammel, P, Haller, L, Kroening, D, Melham, T
Формат: Conference item
Опубликовано: Springer, Cham 2017