Generalized Property Directed Reachability
From MaRDI portal
Publication:2843329
DOI10.1007/978-3-642-31612-8_13zbMath1273.68229OpenAlexW81626549MaRDI QIDQ2843329
Kryštof Hoder, Nikolaj Bjørner
Publication date: 12 August 2013
Published in: Theory and Applications of Satisfiability Testing – SAT 2012 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-31612-8_13
Related Items
Improving Generalization in Software IC3, Infinite-state invariant checking with IC3 and predicate abstraction, Interpolation and model checking for nonlinear arithmetic, Guiding Craig interpolation with domain-specific abstractions, SAT-Based Model Checking, Automating regression verification of pointer programs by predicate abstraction, Leveraging Horn clause solving for compositional verification of PLC software, When Is a Formula a Loop Invariant?, Horn Clause Solvers for Program Verification, Analysis and Transformation of Constrained Horn Clauses for Program Verification, Unnamed Item, Property Directed Reachability for Proving Absence of Concurrent Modification Errors, A unifying view on SMT-based software verification, Relational program reasoning using compiler IR, Unnamed Item, Efficient strategies for CEGAR-based model checking, Unnamed Item, Unnamed Item, SMT-based verification of data-aware processes: a model-theoretic approach, Learning inductive invariants by sampling from frequency distributions, Parametrized invariance for infinite state processes, Unbounded procedure summaries from bounded environments, Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF, Tree dimension in verification of constrained Horn clauses, SMT-based model checking for recursive programs, From invariant checking to invariant inference using randomized search, Higher-order quantifier elimination, counter simulations and fault-tolerant systems, ICE-based refinement type discovery for higher-order functional programs, On recursion-free Horn clauses and Craig interpolation, Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes), Model completeness, covers and superposition, Removing algebraic data types from constrained Horn clauses using difference predicates
Uses Software
