Samir Genaim

FM Conference 2026 Conference Paper

Towards Formally Verified Smart Contracts Compilation

• Elvira Albert
• Samir Genaim
• Enrique Martin-Martin

Abstract Many compilation stages of smart contracts on the Ethereum blockchain have been transitioned to the intermediate language. Tasks such as smart contract optimization and bytecode generation are—or will soon be—performed directly at the level in the compilers for the higher-level languages such as Solidity. In this paper, we develop a formal semantics of programs in Rocq, suitable for verification, which allows formal reasoning at the level of code or generation tools processing programs. Our semantics is expressive enough to be the basis for formal verification tools, and simple enough to make the development of such tools feasible. In order to prove its adequacy for verification, we develop in Rocq a checker (and associated soundness proofs), based on our semantics, able to verify the results of the liveness analysis stage of the official Solidity compiler, which opens the door towards formally verified Ethereum’s smart contracts compilation. Experiments on more than 1, 500 smart contracts show that we are able to automatically verify ’s liveness analysis results in negligible time.

LOPSTR Conference 2013 Conference Paper

A Transformational Approach to Resource Analysis with Typed-Norms

• Elvira Albert
• Samir Genaim
• Raúl Gutiérrez

Abstract In order to automatically infer the resource consumption of programs, analyzers track how data sizes change along a program’s execution. Typically, analyzers measure the sizes of data by applying norms which are mappings from data to natural numbers that represent the sizes of the corresponding data. When norms are defined by taking type information into account, they are named typed-norms. The main contribution of this paper is a transformational approach to resource analysis with typed-norms. The analysis is based on a transformation of the program into an intermediate abstract program in which each variable is abstracted with respect to all considered norms which are valid for its type. We also sketch a simple analysis that can be used to automatically infer the required, useful, typed-norms from programs.

TCS Journal 2013 Journal Article

Corrigendum to “Reachability-based acyclicity analysis by abstract interpretation” [Theoretical Computer Science 474 (2013) 60–79]

• Samir Genaim
• Damiano Zanardini

LPAR Conference 2013 Conference Paper

May-Happen-in-Parallel Analysis for Priority-Based Scheduling

• Elvira Albert
• Samir Genaim
• Enrique Martin-Martin

Abstract A may-happen-in-parallel (MHP) analysis infers the sets of pairs of program points that may execute in parallel along a program’s execution. This is an essential piece of information to detect data races, and also to infer more complex properties of concurrent programs, e. g. , deadlock freeness, termination and resource consumption analyses can greatly benefit from the MHP relations to increase their accuracy. Previous MHP analyses have assumed a worst case scenario by adopting a simplistic (non-deterministic) task scheduler which can select any available task. While the results of the analysis for a non-deterministic scheduler are obviously sound, they can lead to an overly pessimistic result. We present an MHP analysis for an asynchronous language with prioritized tasks buffers. Priority-based scheduling is arguably the most common scheduling strategy adopted in the implementation of concurrent languages. The challenge is to be able to take task priorities into account at static analysis time in order to filter out unfeasible MHP pairs.

TCS Journal 2013 Journal Article

Reachability-based acyclicity analysis by Abstract Interpretation

• Samir Genaim
• Damiano Zanardini

In programming languages with dynamic use of memory, such as Java, knowing that a reference variable x points to an acyclic data structure is valuable for the analysis of termination and resource usage (e. g. , execution time or memory consumption). For instance, this information guarantees that the depth of the data structure to which x points is greater than the depth of the data structure pointed to by x. f for any field f of x. This, in turn, allows bounding the number of iterations of a loop which traverses the structure by its depth, which is essential in order to prove the termination or infer the resource usage of the loop. The present paper provides an Abstract-Interpretation-based formalization of a static analysis for inferring acyclicity, which works on the reduced product of two abstract domains: reachability, which models the property that the location pointed to by a variable w can be reached by dereferencing another variable v (in this case, v is said to reach w ); and cyclicity, modeling the property that v can point to a cyclic data structure. The analysis is proven to be sound and optimal with respect to the chosen abstraction.

LPAR Conference 2012 Conference Paper

Automatic Inference of Resource Consumption Bounds

• Elvira Albert
• Puri Arenas
• Samir Genaim
• Miguel Gómez-Zamalloa
• Germán Puebla

Abstract One of the main features of programs is the amount of resources which are needed in order to run them. Different resources can be taken into consideration, such as the number of execution steps, amount of memory allocated, number of calls to certain methods, etc. Unfortunately, manually determining the resource consumption of programs is difficult and error-prone. We provide an overview of a state of the art framework for automatically obtaining both upper and lower bounds on the resource consumption of programs. The bounds obtained are functions on the size of the input arguments to the program and are obtained statically, i. e. , without running the program. Due to the approximations introduced, the framework can fail to obtain (non-trivial) bounds even if they exist. On the other hand, modulo implementation bugs, the bounds thus obtained are valid for any execution of the program. The framework has been implemented in the COSTA system and can provide useful bounds for realistic object-oriented and actor-based concurrent programs.

TCS Journal 2012 Journal Article

Cost analysis of object-oriented bytecode programs

• Elvira Albert
• Puri Arenas
• Samir Genaim
• German Puebla
• Damiano Zanardini

Cost analysis statically approximates the cost of programs in terms of their input data size. This paper presents, to the best of our knowledge, the first approach to the automatic cost analysis of object-oriented bytecode programs. In languages such as Java and C#, analyzing bytecode has a much wider application area than analyzing source code since the latter is often not available. Cost analysis in this context has to consider, among others, dynamic dispatch, jumps, the operand stack, and the heap. Our method takes a bytecode program and a cost model specifying the resource of interest, and generates cost relations which approximate the execution cost of the program with respect to such resource. We report on COSTA, an implementation for Java bytecode which can obtain upper bounds on cost for a large class of programs and complexity classes. Our basic techniques can be directly applied to infer cost relations for other object-oriented imperative languages, not necessarily in bytecode form.

LPAR Conference 2001 Conference Paper

Inferring Termination Conditions for Logic Programs Using Backwards Analysis

• Samir Genaim
• Michael Codish

Abstract This paper focuses on the inference of modes for which a logic program is guaranteed to terminate. This generalizes traditional termination analysis where an analyzer tries to verify termination for a specified mode. The contribution is a methodology which combines traditional termination analysis and backwards analysis to obtain termination inference. This leads to a better understanding of termination inference, simplifies its formal justification, and facilitates implementation. We evaluate the application of this approach to enhance an existing termination analyzer to perform also termination inference.