Collaborative inference of combined invariants

DOI10.29007/KV72MaRDI QIDQ7025214zbMATH OpenFDO

Authors Yurii Kostyukov, Dmitriĭ Aleksandrovich Mordvinov, Grigory Fedyukovich

Publication date 19 February 2025

Full work available at URL https://doi.org/10.29007/KV72

zbMATH Keywords

algebraic data typescegarcollaborative inferenceconstrained Horn clausesinductive invariants

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites work

• A survey on product operators in abstract interpretation
• Composing dataflow analyses and transformations
• Equational formulae with membership constraints
• HoIce: an ICE-based non-linear Horn clause solver
• Horn clause solvers for program verification
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• IC3 -- flipping the E in ICE
• Invariant Synthesis for Combined Theories
• SMT-based model checking for recursive programs
• TIP: tons of inductive problems
• Transition power abstractions for deep counterexample detection

This page was built for publication: Collaborative inference of combined invariants

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