scientific article; zbMATH DE number 7559486

DOI10.4230/LIPICS.CONCUR.2020.30MaRDI QIDQ5089296FDOQ5089296

Authors: Francesco Ranzato 

Publication date: 18 July 2022

Full work available at URL: https://arxiv.org/abs/2004.03170

Title of this publication is not available (Why is that?)

zbMATH Keywords

abstract interpretationprogram verificationinductive invariant

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• Dafny: an automatic program verifier for functional correctness
• Constructive versions of Tarski's fixed point theorems
• Title not available (Why is that?)
• Affine relationships among variables of a program
• Title not available (Why is that?)
• Synthesis of Circular Compositional Program Proofs via Abduction
• Making abstract interpretations complete
• Title not available (Why is that?)
• Title not available (Why is that?)
• On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics
• Inductive methods for proving properties of programs
• On the decidability of the existence of polyhedral invariants in transition systems
• Polynomial Invariants for Affine Programs
• Title not available (Why is that?)
• Automata, Languages and Programming
• A scalable segmented decision tree abstract domain
• Decidability of inferring inductive invariants
• Title not available (Why is that?)
• Complete semialgebraic invariant synthesis for the Kannan-Lipton orbit problem
• Inferring inductive invariants from phase structures

Cited In (2)

• Intensional Kleene and Rice theorems for abstract program semantics
• Inductive termination proofs with transition invariants and their relationship to the size-change abstraction

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)