Showing cs.LOShow all
2 papers · 1 filter
cs.LO2025
Theta as a Horn Solver
Levente Bajczi, Milán Mondok, Vince Molnár
Theta is a verification framework that has participated in the CHC-COMP competition since 2023. While its core approach -- based on transforming constrained Horn clauses (CHCs) int…
cs.LO2024
Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification
Márk Somorjai, Mihály Dobos-Kovács, Zsófia Ãdám +2
Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. Most existing solvers use a diverse set of specialized technique…