99 citations · 174 across the 12 of their papers we have counts for
12 papers
Arithmetizing Shape Analysis
Sebastian Wolff, Ekanshdeep Gupta, Zafer Esen +3
Memory safety is an essential correctness property of software systems. For programs operating on linked heap-allocated data structures, the problem of proving memory safety boils…
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…
DyNetKAT: An Algebra of Dynamic Networks
Georgiana Caltais, Hossein Hojjat, Mohammad Mousavi +1
We introduce a formal language for specifying dynamic updates for Software Defined Networks. Our language builds upon Network Kleene Algebra with Tests (NetKAT) and adds constructs…
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…
Event-Driven Network Programming
Jedidiah McClurg, Hossein Hojjat, Nate Foster +1
Software-defined networking (SDN) programs must simultaneously describe static forwarding behavior and dynamic updates in response to events. Event-driven updates are critical to g…
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…
Efficient Synthesis of Network Updates
Jedidiah McClurg, Hossein Hojjat, Pavol Cerny +1
Software-defined networking (SDN) is revolutionizing the networking industry, but current SDN programming platforms do not provide automated mechanisms for updating global configur…
The Homeostasis Protocol: Avoiding Transaction Coordination Through Program Analysis
Sudip Roy, Lucja Kot, Gabriel Bender +5
Datastores today rely on distribution and replication to achieve improved performance and fault-tolerance. But correctness of many applications depends on strong consistency proper…
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…