Inferring invariants with quantifier alternations: taming the search space explosion

DOI10.1007/978-3-030-99524-9_18zbMATH Open1547.68433MaRDI QIDQ6535571

Jason R. Koenig, Oded Padon, Alex Aiken, Sharon Shoham

Publication date: 23 January 2024

zbMATH Keywords

quantifier alternationinvariant inferencePDR/IC3

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Title not available (Why is that?)
• SMT-based model checking for recursive programs
• Global guidance for local generalization in model checking
• Syntax-guided synthesis for lemma generation in hardware model checking
• Generalized Property Directed Reachability
• SAT-Based Model Checking without Unrolling
• Property-Directed Inference of Universal Invariants or Proving Their Absence
• Bounded Quantifier Instantiation for Checking Inductive Invariants
• Quantifiers on demand
• Verification of threshold-based distributed algorithms by decomposition to decidable logics
• Quantified invariants via syntax-guided synthesis
• Inferring inductive invariants from phase structures

This page was built for publication: Inferring invariants with quantifier alternations: taming the search space explosion

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