scientific article; zbMATH DE number 7559486

DOI10.4230/LIPIcs.CONCUR.2020.30MaRDI QIDQ5089296

Francesco Ranzato

Publication date: 18 July 2022

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

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

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)

Related Items (1)

Intensional Kleene and Rice theorems for abstract program semantics

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Affine relationships among variables of a program
• Constructive versions of Tarski's fixed point theorems
• Complete semialgebraic invariant synthesis for the Kannan-Lipton orbit problem
• On the decidability of the existence of polyhedral invariants in transition systems
• Decidability of inferring inductive invariants
• Dafny: An Automatic Program Verifier for Functional Correctness
• A Scalable Segmented Decision Tree Abstract Domain
• Inductive methods for proving properties of programs
• On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics
• Polynomial Invariants for Affine Programs
• Synthesis of Circular Compositional Program Proofs via Abduction
• Making abstract interpretations complete
• Automata, Languages and Programming
• Inferring inductive invariants from phase structures

This page was built for publication: