Proving safety with trace automata and bounded model checking

Loop under-approximation enriches C programs with additional branches that represent the effect of a (limited) range of loop iterations. While this technique can speed up bug detection significantly, it introduces redundant execution traces which may complicate the verification of the program. This...

Бүрэн тодорхойлолт

Номзүйн дэлгэрэнгүй
Үндсэн зохиолчид: Kroening, D, Lewis, M, Weissenbacher, G
Бусад зохиолчид: Bjørner, N
Формат: Conference item
Хэвлэсэн: Springer 2015