Syntax-guided synthesis for lemma generation in hardware model checking

DOI10.1007/978-3-030-67067-2_15MaRDI QIDQ2234081zbMATH OpenOpenAlexFDO

Authors Hongce Zhang, Aarti Gupta, Sharad Malik

Publication date 18 October 2021

Full work available at URL https://doi.org/10.1007/978-3-030-67067-2_15

zbMATH Keywords

hardware model checkinglemma generationbit-vector theoryCHC solversyntax-guided synthesis (SyGuS)

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical problems of computer architecture (68M07)

Recommendations

• Counterexample-guided quantifier instantiation for synthesis in SMT
• Counterexample-Guided Model Synthesis
• Word level bitwidth reduction for unbounded hardware model checking
• Refutation-based synthesis in SMT
• SAT-Based Synthesis Methods for Safety Specs

Cites work

• scientific article; zbMATH DE number 1701764 (Why is no real title available?)
• scientific article; zbMATH DE number 7088727 (Why is no real title available?)
• Code2Inv: a deep learning framework for program verification
• Computer Science Logic
• Counterexample-guided abstraction refinement for symbolic model checking
• Decomposing Farkas Interpolants
• Effectively propositional interpolants
• Global guidance for local generalization in model checking
• Guiding Craig interpolation with domain-specific abstractions
• Interpolation and SAT-based model checking.
• Learning inductive invariants by sampling from frequency distributions
• Overfitting in synthesis: theory and practice
• Property directed polyhedral abstraction
• SAT-Based Model Checking without Unrolling
• SMT-based model checking for recursive programs
• SMT-based scenario verification for hybrid systems
• Synthesizing environment invariants for modular hardware verification
• The MathSAT5 SMT solver

Cited in

(4)

• Syntax-guided synthesis with quantitative syntactic objectives
• Level-up -- from bits to words
• Inferring invariants with quantifier alternations: taming the search space explosion
• Searching for i-good lemmas to accelerate safety model checking

This page was built for publication: Syntax-guided synthesis for lemma generation in hardware model checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2234081)