Sound up-to techniques and complete abstract domains

DOI10.1145/3209108.3209169zbMATH Open1497.68107arXiv1804.10507OpenAlexW2964318636MaRDI QIDQ5145290FDOQ5145290

Roberto Giacobazzi, Dusko Pavlovic, Filippo Bonchi, Pierre Ganty

Publication date: 20 January 2021

Published in: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Abstract: Abstract interpretation is a method to automatically find invariants of programs or pieces of code whose semantics is given via least fixed-points. Up-to techniques have been introduced as enhancements of coinduction, an abstract principle to prove properties expressed via greatest fixed-points. While abstract interpretation is always sound by definition, the soundness of up-to techniques needs some ingenuity to be proven. For completeness, the setting is switched: up-to techniques are always complete, while abstract domains are not. In this work we show that, under reasonable assumptions, there is an evident connection between sound up-to techniques and complete abstract domains.

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

Recommendations

• Making abstract interpretations complete
• Complete Lattices and Up-To Techniques
• scientific article; zbMATH DE number 1759702
• A certified denotational abstract interpreter
• On the power of abstract interpretation

zbMATH Keywords

abstract interpretationcoinduction up-tocomplete abstract domainscross-fertilizationsound up-to techniques

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cited In (8)

• Combining semilattices and semimodules
• Up-to techniques for behavioural metrics via fibrations
• Systems of fixpoint equations: abstraction, games, up-to techniques and local algorithms
• Title not available (Why is that?)
• Convexity via Weak Distributive Laws
• Exploiting adjoints in property directed reachability analysis
• Language inclusion algorithms as complete abstract interpretations
• Up-To Techniques for Behavioural Metrics via Fibrations

This page was built for publication: Sound up-to techniques and complete abstract domains

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145290)