Related papers: Proof System for Plan Verification under 0-Approxi…
The PCP Theorem is one of the most stunning results in computational complexity theory, a culmination of a series of results regarding proof checking it exposes some deep structure of computational problems. As a surprising side-effect, it…
We present a comprehensive programme analysing the decomposition of proof systems for non-classical logics into proof systems for other logics, especially classical logic, using an algebra of constraints. That is, one recovers a proof…
Model checking and testing are two areas with a similar goal: to verify that a system satisfies a property. They start with different hypothesis on the systems and develop many techniques with different notions of approximation, when an…
We focus on rational solutions or nearly-feasible rational solutions that serve as certificates of feasibility for polynomial optimization problems. We show that, under some separability conditions, certain cubic polynomially constrained…
A number of flexible tactic-based logical frameworks are nowadays available that can implement a wide range of mathematical theories using a common higher-order metalanguage. Used as proof assistants, one of the advantages of such powerful…
In this work we consider the following problem: in a Multi-Prover environment, how close can we get to prove the validity of an NP statement in Zero-Knowledge ? We exhibit a set of two novel Zero-Knowledge protocols for the 3-COLorability…
In the thesis we focus on designing an authentication system to authenticate users over a network with a username and a password. The system uses the zero-knowledge proof (ZKP) system as a password verification mechanism. The ZKP protocol…
CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive…
In considering the reliability of numerical programs, it is normal to "limit our study to the semantics dealing with numerical precision" (Martel, 2005). On the other hand, there is a great deal of work on the reliability of programs that…
We report on the development of an optimized and verified decision procedure for orthologic equalities and inequalities. This decision procedure is quadratic-time and is used as a sound, efficient and predictable approximation to classical…
The CSP (constraint satisfaction problems) is a class of problems deciding whether there exists a homomorphism from an instance relational structure to a target one. The CSP dichotomy is a profound result recently proved by Zhuk (2020, J.…
Relational verification of quantum programs has many potential applications in quantum and post-quantum security and other domains. We propose a relational program logic for quantum programs. The interpretation of our logic is based on a…
Cyp (Check Your Proofs) (Durner and Noschinski 2013; Traytel 2019) verifies proofs about Haskell-like programs. We extended Cyp with a pattern matcher for programs and proof terms, and a type checker. This allows to use Cyp for auto-grading…
Model checking and automated theorem proving are two pillars of formal methods. This paper investigates model checking from an automated theorem proving perspective, aiming at combining the expressiveness of automated theorem proving and…
Despite the vast body of research literature proposing algorithms with formal guarantees, the amount of verifiable code in today's systems remains minimal. This discrepancy stems from the inherent difficulty of verifying code, particularly…
The recent MIP*=RE theorem of Ji, Natarajan, Vidick, Wright, and Yuen shows that the complexity class MIP* of multiprover proof systems with entangled provers contains all recursively enumerable languages. Prior work of Grilo, Slofstra, and…
We present a general approach to planning with incomplete information in Answer Set Programming (ASP). More precisely, we consider the problems of conformant and conditional planning with sensing actions and assumptions. We represent…
As the usage of theorem prover technology expands, so too does the reliance on correctness of the tools. Metamath Zero is a verification system that aims for simplicity of logic and implementation, without compromising on efficiency of…
We define a fragment of propositional logic where isomorphic propositions, such as $A\land B$ and $B\land A$, or $A\Rightarrow (B\land C)$ and $(A\Rightarrow B)\land(A\Rightarrow C)$ are identified. We define System I, a proof language for…
Let $\mathbb{Q}$ (resp. $\mathbb{R}$) be the field of rational (resp. real) numbers and $X = (X_1, \ldots, X_n)$ be variables. Deciding the non-negativity of polynomials in $\mathbb{Q}[X]$ over $\mathbb{R}^n$ or over semi-algebraic domains…