Related papers: Flat and One-Variable Clauses: Complexity of Verif…
We produce a class of $\omega$-categorical structures with finite signature by applying a model-theoretic construction -- a refinement of the Hrushosvki-encoding -- to $\omega$-categorical structures in a possibly infinite signature. We…
We prove the #P-hardness of the counting problems associated with various satisfiability, graph and combinatorial problems, when restricted to planar instances. These problems include \begin{romannum} \item[{}] {\sc 3Sat, 1-3Sat, 1-Ex3Sat,…
Motivated by applications in automated verification of higher-order functional programs, we develop a notion of constrained Horn clauses in higher-order logic and a decision problem concerning their satisfiability. We show that, although…
On July 5, 2022, the National Institute of Standards and Technology announced four possible post-quantum cryptography standards, three of them are based on lattice theory and the other one is based on Hash function. It is well-known that…
For high-assurance software, source-level reasoning is insufficient: we need binary-level guarantees. Despite constrained Horn clause (CHC) solving being one of the most popular forms of automated verification, prior work has not evaluated…
Analysis of cryptographic protocols in a symbolic model is relative to a deduction system that models the possible actions of an attacker regarding an execution of this protocol. We present in this paper a transformation algorithm for such…
We formalize the simulation paradigm of cryptography in terms of category theory and show that protocols secure against abstract attacks form a symmetric monoidal category, thus giving an abstract model of composable security definitions in…
The functional properties of a program are often specified by providing a contract for each of its functions. A contract of a function consists of a pair of formulas, called a precondition and a postcondition, which, respectively, should…
A composite source, consisting of multiple subsources and a memoryless switch, outputs one symbol at a time from the subsource selected by the switch. If some data should be encoded more accurately than other data from an information…
Verifying programs that manipulate tree data structures often requires complex, ad-hoc proofs that are hard to generalize and automate. This paper introduces an automatic technique for analyzing such programs. Our approach combines automata…
Constraint Programming (CP) has proved an effective paradigm to model and solve difficult combinatorial satisfaction and optimisation problems from disparate domains. Many such problems arising from the commercial world are permeated by…
The unique solution of contractions is a proof technique for bisimilarity that overcomes certain syntactic constraints of Milner's "unique solution of equations" technique. The paper presents an overview of a rather comprehensive…
The proof of a program property can be reduced to the proof of satisfiability of a set of constrained Horn clauses (CHCs) which can be automatically generated from the program and the property. In this paper we have conducted a case study…
We propose a new formal criterion for secure compilation, providing strong security guarantees for components written in unsafe, low-level languages with C-style undefined behavior. Our criterion goes beyond recent proposals, which protect…
We determine the exact threshold of satisfiability for random instances of a particular NP-complete constraint satisfaction problem (CSP). This is the first random CSP model for which we have determined a precise linear satisfiability…
Several techniques and tools have been developed for verification of properties expressed as Horn clauses with constraints over a background theory (CHC). Current CHC verification tools implement intricate algorithms and are often limited…
In recent years they have been numerous works that aim to automate relational verification. Meanwhile, although Constrained Horn Clauses (CHCs) empower a wide range of verification techniques and tools, they lack the ability to express…
We define a problem of certifying computation integrity performed by some remote party we do not necessarily trust. We present a multi-party interactive protocol called SafeComp that solves this problem under specified constraints.…
In the universal blind quantum computation problem, a client wants to make use of a single quantum server to evaluate $C|0\rangle$ where $C$ is an arbitrary quantum circuit while keeping $C$ secret. The client's goal is to use as few…
We consider the satisfiability problem for the two-variable fragment of first-order logic over finite unranked trees. We work with signatures consisting of some unary predicates and the binary navigational predicates child, right sibling,…