Sound up-to techniques and complete abstract domains

DOI10.1145/3209108.3209169MaRDI QIDQ5145290zbMATH OpenOpenAlexFDO

Authors Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi, Dusko Pavlovic

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)

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

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)

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.

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

Cited in

(9)

• Combining semilattices and semimodules
• Up-to techniques for behavioural metrics via fibrations
• Up-to techniques for behavioural metrics via fibrations
• Systems of fixpoint equations: abstraction, games, up-to techniques and local algorithms
• scientific article; zbMATH DE number 7559481 (Why is no real title available?)
• Strong induction is an up-to technique
• Convexity via Weak Distributive Laws
• Exploiting adjoints in property directed reachability analysis
• Language inclusion algorithms as complete abstract interpretations

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)