arXiv.itsnick.co

an independent field guide to 23 million papers from arXiv & OpenAlex — not affiliated with arXiv.org

Computer Science · Computational Theory and Mathematics

SAT-based Model Checking: Interpolation, IC3, and Beyond

Orna Grümberg, Shoham Sharon, Vizel Yakir

· NATO science for peace and security series. D, Information and communication security

See on the map

Abstract

SAT-based model checking is currently one of the most successful approaches to checking very large systems. In its early days, SAT-based (bounded) model checking was mainly used for bug hunting. The introduction of interpolation and IC3\PDR enable efficient complete algorithms that can provide full verification as well.

More like this