Decomposing Farkas Interpolants

DOI10.1007/978-3-030-17462-0_1MaRDI QIDQ6091330zbMATH OpenOpenAlexFDO

Authors Martin Blicha, Antti E. J. Hyvärinen, Jan Kofroň, Natasha Sharygina

Publication date 24 November 2023

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-17462-0_1

zbMATH Keywords

Craig interpolationlinear arithmeticmodel checkingsatisfiability modulo theory

Mathematics Subject Classification ID

Logic in computer science (03B70) Interpolation, preservation, definability (03C40) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Computer Science Logic
• Constraint solving for interpolation
• Constraint Solving for Interpolation
• Improving interpolants for linear arithmetic
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(6)

• Farkas-based tree interpolation
• Syntax-guided synthesis for lemma generation in hardware model checking
• scientific article; zbMATH DE number 7453201 (Why is no real title available?)
• Interpolative Decomposition Butterfly Factorization
• Transition power abstractions for deep counterexample detection
• Global guidance for local generalization in model checking

This page was built for publication: Decomposing Farkas Interpolants

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