Word-Level Model Checking

Description

In SMT bit-vectors and thus word-level reasoningis common and widely used in industry. However, it took until2019 that the hardware model checking competition started to useword-level benchmarks. Reasoning on the word-level opens upmany possibilities for simplification and more powerful reasoning.In SMT we do see advantages due to operating on the word-level, even though, ultimately, bit-blasting and thus transformingthe word-level problem into SAT is still the dominant and mostimportant technique. For word-level model checking the situationis different. As the hardware model checking competition in 2019has shown bit-level solvers are far superior (after bit-blasting themodel through an SMT solver though). On the other hand word-level model checking shines for problems with memory modeledwith arrays. In this tutorial we revisit the problem of wordlevel model checking, also from a theoretical perspective, give anoverview on classical and more recent approaches for word-levelmodel checking and then discuss challenges and future work.The tutorial covered material from the following papers

Period	21 Sept 2020
Event title	19th Intl. Conf. on Formal Methods in Computer-Aided Design (FMCAD'20)
Event type	Other
Location	AustriaShow on map