Decidability of inferring inductive invariants

DOI10.1145/2837614.2837640zbMath1347.68234OpenAlexW2296031223MaRDI QIDQ2828258

Sharon Shoham, Oded Padon, Mooly Sagiv, Aleksandr Karbyshev

Publication date: 24 October 2016

Published in: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

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

zbMATH Keywords

verificationwell-quasi-ordereffectively propositional logicinvariant inference

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25)

Related Items (4)

Stratified guarded first-order transition systems ⋮ What’s Decidable About Program Verification Modulo Axioms? ⋮ Unnamed Item ⋮ On invariant synthesis for parametric systems

This page was built for publication: Decidability of inferring inductive invariants