Verifying multi-threaded software with impact

Lazy abstraction with interpolants, also known as the Impact algorithm, is en vogue as a state-of-the-art software model-checking technique for sequential programs. However, a direct extension of the Impact algorithm to concurrent programs is bound to be inefficient as it has to explore all thread i...

Mô tả đầy đủ

Chi tiết về thư mục
Những tác giả chính: Wachter, B, Kroening, D, Ouaknine, J
Định dạng: Conference item
Được phát hành: IEEE 2013