4 papers
CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses
Mihály Dobos-Kovács, Levente Bajczi, András Vörös
Constrained Horn Clauses (CHCs) are widely adopted as intermediate representations for a variety of verification tasks, including safety checking, invariant synthesis, and interpro…
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…
Enhancing MBSE Education with Version Control and Automated Feedback
Levente Bajczi, Dániel Szekeres, Daniel Siegl +1
This paper presents an innovative approach to conducting a Model-Based Systems Engineering (MBSE) course, engaging over 80 participants annually. The course is structured around co…
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…