arXiv subjects

Miguel Isabel

Publications and source records attributed to Miguel Isabel.

3 recordsLinked to original sources

arXiv2026

An Effective Orchestral Approach to Satisfiability Modulo Prime Fields

Zero-knowledge proofs (ZKPs) are an emerging technology that has become the solution to efficiently provide security and privacy along with the transparency requirement of blockchains. ZKPs are usually expressed by means of arithmetic circuits and, more generally, systems of polynomial equations in a large prime field (commonly ranging from 64-bit to 256-bit values). An increasing interest to apply formal verification techniques to ensure soundness and completeness properties of ZKP protocols has shown the need of developing powerful SMT solvers able to handle such constraint systems. In this paper we consider the problem of deciding the satisfiability of existentially quantified first-order formulas defined over polynomial equations on a prime field. We present a new DPLL($T$)-based approach in which the theory solver orchestrates several modules with different trade-offs between completeness and efficiency. We have implemented the proposed techniques in a prototype that already shows better results than existing state-of-the-art tools on both benchmarks from the domain of ZKP compiler correctness and new benchmarks coming from the verification of arithmetic circuits for ZKPs. \keywords{SMT \and Finite field \and Polynomials \and Zero-Knowledge Proofs.

cs.LO↗

arXiv2020

Actor-Based Model Checking for SDN Networks

Software-Defined Networking (SDN) is a networking paradigm that has become increasingly popular in the last decade. The unprecedented control over the global behavior of the network it provides opens a range of new opportunities for formal methods and much work has appeared in the last few years on providing bridges between SDN and verification. This article advances this research line and provides a link between SDN and traditional work on formal methods for verification of concurrent and distributed software---actor-based modelling. We show how SDN programs can be seamlessly modelled using \emph{actors}, and thus existing advanced model checking techniques developed for actors can be directly applied to verify a range of properties of SDN networks, including consistency of flow tables, violation of safety policies, and forwarding loops. Our model checker for SDN networks is available through an online web interface, that also provides the SDN actor-models for a number of well-known SDN benchmarks.

cs.NI↗

arXiv2017

On the Generation of Initial Contexts for Effective Deadlock Detection

It has been recently proposed that testing based on symbolic execution can be used in conjunction with static deadlock analysis to define a deadlock detection framework that: (i) can show deadlock presence, in that case a concrete test-case and trace are obtained, and (ii) can also prove deadlock freedom. Such symbolic execution starts from an initial distributed context, i.e., a set of locations and their initial tasks. Considering all possibilities results in a combinatorial explosion on the different distributed contexts that must be considered. This paper proposes a technique to effectively generate initial contexts that can lead to deadlock, using the possible conflicting task interactions identified by static analysis, discarding other distributed contexts that cannot lead to deadlock. The proposed technique has been integrated in the above-mentioned deadlock detection framework hence enabling it to analyze systems without the need of any user supplied initial context.

cs.PL↗