Quantifiers on demand

DOI10.1007/978-3-030-01090-4_15zbMath1517.68239arXiv2106.00664OpenAlexW2893533736MaRDI QIDQ6109591

Yakir Vizel, Arie Gurfinkel, Sharon Shoham

Publication date: 28 July 2023

Published in: Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2106.00664

Mathematics Subject Classification ID

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

Related Items (11)

Verifying Array Manipulating Programs with Full-Program Induction ⋮ RustHorn: CHC-Based Verification for Rust Programs ⋮ Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays ⋮ \textsc{Diffy}: inductive reasoning of array programs using difference invariants ⋮ Data abstraction: a general framework to handle program verification of data structures ⋮ Lemmaless induction in trace logic ⋮ Efficient modular SMT-based model checking of pointer programs ⋮ Synthesizing history and prophecy variables for symbolic model checking ⋮ Interpolation and amalgamation for arrays with MaxDiff ⋮ Counterexample-guided prophecy for model checking modulo the theory of arrays ⋮ On invariant synthesis for parametric systems

This page was built for publication: Quantifiers on demand