Synchronizing constrained Horn clauses

DOI10.29007/GR5CMaRDI QIDQ4645746zbMATH OpenOpenAlexFDO

Authors Dmitriĭ Aleksandrovich Mordvinov, Grigory Fedyukovich

Publication date 10 January 2019

Published in EPiC Series in Computing (Search for Journal in Brave)

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

zbMATH Keywords

constrained Horn clausesinductive invariantlinearizationrelational verificationunbounded model checking

Mathematics Subject Classification ID

Logic in computer science (03B70) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Solving Horn clauses on inductive data types without induction
• Automating induction for solving Horn clauses
• Solving non-linear Horn clauses using a linear Horn clause solver
• Inferring simple solutions to recursion-free Horn clauses via sampling
• Probabilistic Horn clause verification

Cited in

(12)

• Learning inductive invariants by sampling from frequency distributions
• On a generalization of Horn constraint systems
• Solving constrained Horn clauses using dependence-disjoint expansions
• Tree dimension in verification of constrained Horn clauses
• scientific article; zbMATH DE number 7444023 (Why is no real title available?)
• scientific article; zbMATH DE number 7453193 (Why is no real title available?)
• Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
• Fold/unfold transformations for fixpoint logic
• scientific article; zbMATH DE number 7589540 (Why is no real title available?)
• Analysis and Transformation of Constrained Horn Clauses for Program Verification
• Solving constrained Horn clauses over algebraic data types
• Lockstep composition for unbalanced loops

This page was built for publication: Synchronizing constrained Horn clauses

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