Showing cs.LOShow all
2 papers · 1 filter
cs.LO2026
Craig Interpolation in Program Verification
Philipp Rümmer
Craig interpolation is used in program verification for automating key tasks such as the inference of loop invariants and the computation of program abstractions. This chapter cove…
cs.LO2024
An Encoding for CLP Problems in SMT-LIB
Daneshvar Amrollahi, Hossein Hojjat, Philipp Rümmer
The input language for today's CHC solvers are commonly the standard SMT-LIB format, borrowed from SMT solvers, and the Prolog format that stems from Constraint-Logic Programming (…