99 citations · 174 across the 12 of their papers we have counts for
7 papers · 1 filter
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 (…
OptiRica: Towards an Efficient Optimizing Horn Solver
Hossein Hojjat, Philipp Rümmer
This paper describes an ongoing effort to develop an optimizing version of the Eldarica Horn solver. The work starts from the observation that many kinds of optimization problems,…
Proceedings 8th Workshop on Horn Clauses for Verification and Synthesis
Hossein Hojjat, Bishoksan Kafle
This volume contains the post-proceedings of the 8th Workshop on Horn Clauses for Verification and Synthesis (HCVS), which took place virtually due to Covid-19 pandemic as an affil…
Deciding and Interpolating Algebraic Data Types by Reduction (Technical Report)
Hossein Hojjat, Philipp Rümmer
Recursive algebraic data types (term algebras, ADTs) are one of the most well-studied theories in logic, and find application in contexts including functional programming, modellin…
Horn Clauses for Communicating Timed Systems
Hossein Hojjat, Philipp Rümmer, Pavle Subotic +1
Languages based on the theory of timed automata are a well established approach for modelling and analysing real-time systems, with many applications both in industrial and academi…
The Relationship between Craig Interpolation and Recursion-Free Horn Clauses
Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
Despite decades of research, there are still a number of concepts commonly found in software programs that are considered challenging for verification: among others, such concepts…
Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report)
Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
One of the main challenges in software verification is efficient and precise compositional analysis of programs with procedures and loops. Interpolation methods remain one of the m…