Property-directed inference of universal invariants or proving their absence
From MaRDI portal
Publication:3177887
DOI10.1145/3022187zbMATH Open1426.68050OpenAlexW2603705845MaRDI QIDQ3177887FDOQ3177887
Authors: Nikolaj Bjørner, Shachar Itzhaky, Noam Rinetzky, Sharon Shoham, 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
Recommendations
- Property-directed inference of universal invariants or proving their absence
- Property-directed incremental invariant generation
- Property Directed Reachability for Proving Absence of Concurrent Modification Errors
- Goal-directed invariant synthesis for model checking modulo theories
- Property directed abstract interpretation
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)
Cited In (8)
- Property-directed incremental invariant generation
- Stratified guarded first-order transition systems
- Efficiently learning safety proofs from appearance as well as behaviours
- Synthesizing history and prophecy variables for symbolic model checking
- On invariant synthesis for parametric systems
- Non-well-founded deduction for induction and coinduction
- Goal-directed invariant synthesis for model checking modulo theories
- Inferring invariants with quantifier alternations: taming the search space explosion
This page was built for publication: Property-directed inference of universal invariants or proving their absence
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3177887)
