Property-Directed Inference of Universal Invariants or Proving Their Absence

DOI10.1145/3022187zbMath1426.68050OpenAlexW2603705845MaRDI QIDQ3177887

Shachar Itzhaky, Nikolaj Bjørner, Sharon Shoham, Noam Rinetzky, Aleksandr Karbyshev

Publication date: 2 August 2018

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/3022187

zbMATH Keywords

EPRIC3property-directed reachabilityuniversal invariantsPDR

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Synthesizing history and prophecy variables for symbolic model checking ⋮ Stratified guarded first-order transition systems ⋮ Non-well-founded deduction for induction and coinduction ⋮ On invariant synthesis for parametric systems

This page was built for publication: Property-Directed Inference of Universal Invariants or Proving Their Absence