Syntax-guided synthesis for lemma generation in hardware model checking

DOI10.1007/978-3-030-67067-2_15zbMath1472.68096OpenAlexW3120833016MaRDI QIDQ2234081

Sharad Malik, Aarti Gupta, Hongce Zhang

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)

Related Items (1)

Level-up -- from bits to words

Cites Work

• Unnamed Item
• Unnamed Item
• Guiding Craig interpolation with domain-specific abstractions
• SMT-based model checking for recursive programs
• Synthesizing environment invariants for modular hardware verification
• Learning inductive invariants by sampling from frequency distributions
• Global guidance for local generalization in model checking
• Code2Inv: a deep learning framework for program verification
• SMT-based scenario verification for hybrid systems
• SAT-Based Model Checking without Unrolling
• Counterexample-guided abstraction refinement for symbolic model checking
• Effectively Propositional Interpolants
• Property Directed Polyhedral Abstraction
• Computer Science Logic
• The MathSAT5 SMT Solver
• Computer Aided Verification
• Decomposing Farkas Interpolants
• Overfitting in synthesis: theory and practice

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