Synchronizing Constrained Horn Clauses

DOI10.29007/gr5czbMath1403.68243OpenAlexW2741328615MaRDI QIDQ4645746

Grigory Fedyukovich, Dmitriĭ Aleksandrovich Mordvinov

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

linearizationrelational verificationconstrained Horn clausesinductive invariantunbounded model checking

Mathematics Subject Classification ID

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

Related Items (9)

Verifying Catamorphism-Based Contracts using Constrained Horn Clauses ⋮ Analysis and Transformation of Constrained Horn Clauses for Program Verification ⋮ Unnamed Item ⋮ Solving constrained Horn clauses over algebraic data types ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Learning inductive invariants by sampling from frequency distributions ⋮ Tree dimension in verification of constrained Horn clauses ⋮ Fold/Unfold Transformations for Fixpoint Logic

This page was built for publication: Synchronizing Constrained Horn Clauses