Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Mon 18 Jan 2021 18:15 - 18:30 at VMCAI - Model Checking Chair(s): James R. Wilcox

In this work we propose to use Syntax-Guided Synthesis (SyGuS) for lemma generation in a word-level IC3/PDR framework for bit-vector problems. Hardware model checking is moving from bit-level to word-level problems, and it is expected that model checkers can benefit when such high-level information is available. However, for bit-vectors, it is challenging to find a good word-level interpolation strategy for lemma generation, which hinders the use of word-level IC3/PDR algorithms.

Our SyGuS-based procedure, SyGuS-APDR, is tightly integrated with an existing word-level IC3/PDR framework APDR. It includes a predefined grammar template and term production rules for generating candidate lemmas, and does not rely on any extra human inputs. Our experiments on benchmarks from the hardware model checking competition show that SyGuS-APDR can outperform state-of-the-art Constrained Horn Clause (CHC) solvers, including those that implement bit-level IC3/PDR. We also show that SyGuS-APDR and these CHC solvers can solve many instances not solved by other leading hardware model checkers that are not CHC-based. As a by-product of our work, we provide a translator Btor2CHC that enables use of CHC solvers for general hardware model checking problems, and contribute representative bit-vector benchmarks to the CHC-solver community.

Mon 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:00 - 18:30: Model CheckingVMCAI at VMCAI
Chair(s): James R. WilcoxUniversity of Washington
18:00 - 18:15
Unbounded Procedure Summaries from Bounded Environments
Lauren PickPrinceton University, Grigory FedyukovichFlorida State University, Aarti GuptaPrinceton University
Media Attached
18:15 - 18:30
Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking
Hongce ZhangPrinceton University, Aarti GuptaPrinceton University, Sharad MalikPrinceton University
Media Attached