scientific article; zbMATH DE number 7559486
From MaRDI portal
Publication:5089296
Cites work
- A scalable segmented decision tree abstract domain
- Affine relationships among variables of a program
- Automata, Languages and Programming
- Bounded quantifier instantiation for checking inductive invariants
- Complete semialgebraic invariant synthesis for the Kannan-Lipton orbit problem
- Constructive versions of Tarski's fixed point theorems
- Dafny: an automatic program verifier for functional correctness
- Decidability of inferring inductive invariants
- scientific article; zbMATH DE number 3714908 (Why is no real title available?)
- scientific article; zbMATH DE number 1222407 (Why is no real title available?)
- scientific article; zbMATH DE number 1759702 (Why is no real title available?)
- scientific article; zbMATH DE number 3302923 (Why is no real title available?)
- scientific article; zbMATH DE number 3349291 (Why is no real title available?)
- Inductive methods for proving properties of programs
- Inferring inductive invariants from phase structures
- Making abstract interpretations complete
- On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics
- On the decidability of the existence of polyhedral invariants in transition systems
- Polynomial Invariants for Affine Programs
- Synthesis of circular compositional program proofs via abduction
Cited in
(5)- Intensional Kleene and Rice theorems for abstract program semantics
- Inductive termination proofs with transition invariants and their relationship to the size-change abstraction
- Stratified guarded first-order transition systems
- A correctness and incorrectness program logic
- A Rice's theorem for abstract semantics
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5089296)
