Searcharxiv⌕ Search

arXiv subjects

Ahmed Rezine

Publications and source records attributed to Ahmed Rezine.

8 recordsLinked to original sources
arXiv2025

Formal Local Implication Between Two Neural Networks

Given two neural network classifiers with the same input and output domains, our goal is to compare the two networks in relation to each other over an entire input region (e.g., within a vicinity of an input sample). To this end, we establish the foundation of formal local implication between two networks, i.e., N2 implies N1, in an entire input region D. That is, network N1 consistently makes a correct decision every time network N2 does, and it does so in an entire input region D. We further propose a sound formulation for establishing such formally-verified (provably correct) local implications. The proposed formulation is relevant in the context of several application domains, e.g., for comparing a trained network and its corresponding compact (e.g., pruned, quantized, distilled) networks. We evaluate our formulation based on the MNIST, CIFAR10, and two real-world medical datasets, to show its relevance.

cs.LG↗
arXiv2024

VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees

Machine learning techniques often lack formal correctness guarantees, evidenced by the widespread adversarial examples that plague most deep-learning applications. This lack of formal guarantees resulted in several research efforts that aim at verifying Deep Neural Networks (DNNs), with a particular focus on safety-critical applications. However, formal verification techniques still face major scalability and precision challenges. The over-approximation introduced during the formal verification process to tackle the scalability challenge often results in inconclusive analysis. To address this challenge, we propose a novel framework to generate Verification-Friendly Neural Networks (VNNs). We present a post-training optimization framework to achieve a balance between preserving prediction performance and verification-friendliness. Our proposed framework results in VNNs that are comparable to the original DNNs in terms of prediction performance, while amenable to formal verification techniques. This essentially enables us to establish robustness for more VNNs than their DNN counterparts, in a time-efficient manner.

cs.LG↗
arXiv2021

On Reachability in Parameterized Phaser Programs

We address the problem of statically checking safety properties (such as assertions or deadlocks) for parameterized phaser programs. Phasers embody a non-trivial and modern synchronization construct used to orchestrate executions of parallel tasks. This generic construct supports dynamic parallelism with runtime registrations and deregistrations of spawned tasks. It generalizes many synchronization patterns such as collective and point-to-point schemes. For instance, phasers can enforce barriers or producer-consumer synchronization patterns among all or subsets of the running tasks. We consider in this work programs that may generate arbitrarily many tasks and phasers. We study different formulations of the verification problem and propose an exact procedure that is guaranteed to terminate for some reachability problems even in the presence of unbounded phases and arbitrarily many spawned tasks. In addition, we prove undecidability results for several problems on which our procedure cannot be guaranteed to terminate.

cs.PL↗
arXiv2017

Safety Verification of Phaser Programs

We address the problem of statically checking control state reachability (as in possibility of assertion violations, race conditions or runtime errors) and plain reachability (as in deadlock-freedom) of phaser programs. Phasers are a modern non-trivial synchronization construct that supports dynamic parallelism with runtime registration and deregistration of spawned tasks. They allow for collective and point-to-point synchronizations. For instance, phasers can enforce barriers or producer-consumer synchronization schemes among all or subsets of the running tasks. Implementations %of these recent and dynamic synchronization are found in modern languages such as X10 or Habanero Java. Phasers essentially associate phases to individual tasks and use their runtime values to restrict possible concurrent executions. Unbounded phases may result in infinite transition systems even in the case of programs only creating finite numbers of tasks and phasers. We introduce an exact gap-order based procedure that always terminates when checking control reachability for programs generating bounded numbers of coexisting tasks and phasers. We also show verifying plain reachability is undecidable even for programs generating few tasks and phasers. We then explain how to turn our procedure into a sound analysis for checking plain reachability (including deadlock freedom). We report on preliminary experiments with our open source tool.

cs.PL↗
arXiv2016

Quantifying the Information Leak in Cache Attacks through Symbolic Execution

Cache timing attacks allow attackers to infer the properties of a secret execution by observing cache hits and misses. But how much information can actually leak through such attacks? For a given program, a cache model, and an input, our CHALICE framework leverages symbolic execution to compute the amount of information that can possibly leak through cache attacks. At the core of CHALICE is a novel approach to quantify information leak that can highlight critical cache side-channel leaks on arbitrary binary code. In our evaluation on real-world programs from OpenSSL and Linux GDK libraries, CHALICE effectively quantifies information leaks: For an AES-128 implementation on Linux, for instance, CHALICE finds that a cache attack can leak as much as 127 out of 128 bits of the encryption key.

cs.CR↗
arXiv2013

Proceedings 14th International Workshop on Verification of Infinite-State Systems

This volume contains the proceedings of Infinity'12, the 14th International Workshop on Verification of Infinite-State Systems, which was held in Paris, France on the 27th of August 2012 as a satellite event of FM'12. The aim of the INFINITY workshop is to provide a forum for researchers interested in the development of formal methods and algorithmic techniques for the analysis of systems with infinitely many states, and their application in automated verification of complex software and hardware systems.

cs.LO↗
arXiv2012

Ordered Counter-Abstraction

We introduce a new symbolic representation based on an original generalization of counter abstraction. Unlike classical counter abstraction (used in the analysis of parameterized systems with unordered or unstructured topologies) the new representation is tailored for proving properties of linearly ordered parameterized systems, i.e., systems with arbitrary many finite processes placed in an array. The relative positions in the array capture the relative priorities of the processes. Configurations of such systems are finite words of arbitrary lengths. The processes communicate using global transitions constrained by their relative priorities. Intuitively, an element of the symbolic representation has a base and a set of counters. It denotes configurations that respect the constraints imposed by the counters and that have the base as a sub word. We use the new representation in a uniform and automatic Counter Example Guided Refinement scheme. We introduce a relaxation operator that allows a well quasi ordering argument for the termination of each iteration of the refinement loop. We explain how to refine the relaxation to systematically prune out false positives. We implemented a tool to illustrate the approach on a number of parameterized systems.

cs.LO↗