Elvira Albert

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 2025 Conference Paper

Verifying Smart Contracts in Yul via Transformation to CHC by Interpreter Specialization

• Elvira Albert
• Emanuele De Angelis
• Fabio Fioravanti
• Alejandro Hernández-Cerezo
• Giulia Matricardi

Abstract Yul is an intermediate representation that lies in between the (high-level) source code and the (low-level) bytecode languages for Ethereum smart contracts. Although it was proposed to favour the development of verification and optimization techniques, there exists no verifier that can be applied on Yul code directly yet. In this paper, we present a transformational approach to verifying Yul code by transforming it into an equivalent set of Constrained Horn Clauses (CHCs), leading, to the best of our knowledge, to the first approach to directly verify Yul code. Our transformational approach applies the first Futamura projection, i. e. , specializes a Yul interpreter written in CHC with respect tothe Yul code to be verified. The verification of the transformed CHC code can rely on existing tools for CHC verification, namely we have used Z3 with the SPACER engine on our case studies.

LOPSTR Conference 2017 Conference Paper

Generation of Initial Contexts for Effective Deadlock Detection

• Elvira Albert
• Miguel Gómez-Zamalloa
• Miguel Isabel

Abstract 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.

LOPSTR Conference 2016 Conference Paper

A Formal, Resource Consumption-Preserving Translation of Actors to Haskell

• Elvira Albert
• Nikolaos Bezirgiannis
• Frank S. de Boer
• Enrique Martin-Martin

Abstract We present a formal translation of an actor-based language with cooperative scheduling to the functional language Haskell. The translation is proven correct with respect to a formal semantics of the source language and a high-level operational semantics of the target, i. e. a subset of Haskell. The main correctness theorem is expressed in terms of a simulation relation between the operational semantics of actor programs and their translation. This allows us to then prove that the resource consumption is preserved over this translation, as we establish an equivalence of the cost of the original and Haskell-translated execution traces.

TCS Journal 2015 Journal Article

A multi-domain incremental analysis engine and its application to incremental resource analysis

• Elvira Albert
• Jesús Correas
• Germán Puebla
• Guillermo Román-Díez

The aim of incremental analysis is, given a program, its analysis results, and a series of changes to the program, to obtain the new analysis results as efficiently as possible and, ideally, without having to (re-)analyze fragments of code which are not affected by the changes. Incremental analysis can significantly reduce both the time and the memory requirements of analysis. The first contribution of this article is a multi-domain incremental fixed-point algorithm for a sequential Java-like language. The algorithm is multi-domain in the sense that it interleaves the (re-)analysis for multiple domains by taking into account dependencies among them. Importantly, this allows the incremental analyzer to invalidate only those analysis results previously inferred by certain dependent domains. The second contribution is an incremental resource usage analysis which, in its first phase, uses the multi-domain incremental fixed-point algorithm to carry out all global pre-analyses required to infer cost in an interleaved way. Such resource analysis is parametric on the cost metrics one wants to measure (e. g. , number of executed instructions, number of objects created, etc.). Besides, we present a novel form of cost summaries which allows us to incrementally reconstruct only those components of cost functions affected by the changes. Experimental results in the costa system show that the proposed incremental analysis provides significant performance gains, ranging from a speedup of 1. 48 up to 5. 13 times faster than non-incremental analysis.

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.

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.

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.

LOPSTR Conference 2011 Conference Paper

Resource-Driven CLP-Based Test Case Generation

• Elvira Albert
• Miguel Gómez-Zamalloa
• José Miguel Rojas

Abstract Test Data Generation (TDG) aims at automatically obtaining test inputs which can then be used by a software testing tool to validate the functional behaviour of the program. In this paper, we propose resource-aware TDG, whose purpose is to generate test cases (from which the test inputs are obtained) with associated resource consumption s. The framework is parametric w. r. t. the notion of resource (it can measure memory, steps, etc.) and allows using software testing to detect bugs related to non-functional aspects of the program. As a further step, we introduce resource-driven TDG whose purpose is to guide the TDG process by taking resource consumption into account. Interestingly, given a resource policy, TDG is guided to generate test cases that adhere to the policy and avoid the generation of test cases which violate it.

LOPSTR Conference 2010 Conference Paper

Compositional CLP-Based Test Data Generation for Imperative Languages

• Elvira Albert
• Miguel Gómez-Zamalloa
• José Miguel Rojas
• Germán Puebla

Abstract Glass-box test data generation (TDG) is the process of automatically generating test input data for a program by considering its internal structure. This is generally accomplished by performing symbolic execution of the program where the contents of variables are expressions rather than concrete values. The main idea in CLP-based TDG is to translate imperative programs into equivalent CLP ones and then rely on the standard evaluation mechanism of CLP to symbolically execute the imperative program. Performing symbolic execution on large programs becomes quickly expensive due to the large number and the size of paths that need to be explored. In this paper, we propose compositional reasoning in CLP-based TDG where large programs can be handled by testing parts (such as components, modules, libraries, methods, etc.) separately and then by composing the test cases obtained for these parts to get the required information on the whole program. Importantly, compositional reasoning also gives us a practical solution to handle native code, which may be unavailable or written in a different programming language. Namely, we can model the behavior of a native method by means of test cases and compositional reasoning is able to use them.

LOPSTR Conference 2008 Conference Paper

Test Data Generation of Bytecode by CLP Partial Evaluation

• Elvira Albert
• Miguel Gómez-Zamalloa
• Germán Puebla

Abstract We employ existing partial evaluation (PE) techniques developed for Constraint Logic Programming (CLP) in order to automatically generate test-case generators for glass-box testing of bytecode. Our approach consists of two independent CLP PE phases. (1) First, the bytecode is transformed into an equivalent (decompiled) CLP program. This is already a well studied transformation which can be done either by using an ad-hoc decompiler or by specialising a bytecode interpreter by means of existing PE techniques. (2) A second PE is performed in order to supervise the generation of test-cases by execution of the CLP decompiled program. Interestingly, we employ control strategies previously defined in the context of CLP PE in order to capture coverage criteria for glass-box testing of bytecode. A unique feature of our approach is that, this second PE phase allows generating not only test-cases but also test-case generators. To the best of our knowledge, this is the first time that (CLP) PE techniques are applied for test-case generation as well as to generate test-case generators.

LOPSTR Conference 2007 Conference Paper

Type-Based Homeomorphic Embedding and Its Applications to Online Partial Evaluation

• Elvira Albert
• John P. Gallagher
• Miguel Gómez-Zamalloa
• Germán Puebla

Abstract Homeomorphic Embedding ( HEm ) has proven to be very powerful for supervising termination of computations, provided that such computations are performed over a finite signature, i. e. , the number of constants and function symbols involved is finite. However, there are situations, for example numeric computations, which involve an infinite (or too large) signature, in which HEm does not guarantee termination. Some extensions to HEm for the case of infinite signatures have been proposed which guarantee termination, but they either do not provide systematic means for generating such extensions or the extensions are too simplistic and do not produce the expected results in practice. We introduce Type-based Homeomorphic Embedding ( TbHEm ) as an extension of the standard, untyped HEm to deal with infinite signatures. In the paper, we show how TbHEm can be used to improve the accuracy of online partial evaluation. For this purpose, we propose an approach to constructing suitable types for partial evaluation automatically based on existing analysis tools for constraint logic programs. We also present useful properties of types which allow us to take full advantage of TbHEm in practice. Experimental results are reported which show that our work improves the state of the practice of online partial evaluation.

LPAR Conference 2006 Conference Paper

An Incremental Approach to Abstraction-Carrying Code

• Elvira Albert
• Puri Arenas
• Germán Puebla

Abstract Abstraction-Carrying Code (ACC) has recently been proposed as a framework for Proof-Carrying Code (PCC) in which the code supplier provides a program together with an abstraction (or abstract model of the program) whose validity entails compliance with a predefined safety policy. Existing approaches for PCC are developed under the assumption that the consumer reads and validates the entire program w. r. t. the full certificate at once, in a non incremental way. In the context of ACC, we propose an incremental approach to PCC for the generation of certificates and the checking of untrusted update s of a (trusted) program, i. e. , when a producer provides a modified version of a previously validated program. Our proposal is that, if the consumer keeps the original (fixed-point) abstraction, it is possible to provide only the program updates and the incremental certificate (i. e. , the difference of abstractions). Furthermore, it is now possible to define an incremental checking algorithm which, given the new updates and its incremental certificate, only re-checks the fixpoint for each procedure affected by the updates and the propagation of the effect of these fixpoint changes. As a consequence, both certificate transmission time and checking time can be reduced significantly.

LOPSTR Conference 2005 Conference Paper

Converting One Type-Based Abstract Domain to Another

• John P. Gallagher
• Germán Puebla
• Elvira Albert

Abstract The specific problem that motivates this paper is how to obtain abstract descriptions of the meanings of imported predicates (such as built-ins) that can be used when analysing a module of a logic program with respect to some abstract domain. We assume that abstract descriptions of the imported predicates are available in terms of some “standard” assertions. The first task is to define an abstract domain corresponding to the assertions for a given module and express the descriptions as objects in that domain. Following that they are automatically transformed into the analysis domain of interest. We develop a method which has been applied in order to generate call and success patterns from the CiaoPP assertions for built-ins, for any given regular type-based domain. In the paper we present the method as an instance of the more general problem of mapping elements of one abstract domain to another, with as little loss in precision as possible.

LOPSTR Conference 2005 Conference Paper

Non-leftmost Unfolding in Partial Evaluation of Logic Programs with Impure Predicates

• Elvira Albert
• Germán Puebla
• John P. Gallagher

Abstract Partial evaluation of logic programs which contain impure predicates poses non-trivial challenges. Impure predicates include those which produce side-effects, raise errors (or exceptions), and those whose truth value varies according to the degree of instantiation of arguments. In particular, non-leftmost unfolding steps can produce incorrect results since the independence of the computation rule no longer holds in the presence of impure predicates. Existing proposals allow non-leftmost unfolding steps, but at the cost of accuracy: bindings and failure are not propagated backwards to predicates which are potentially impure. In this work we propose a partial evaluation scheme which substantially reduces the situations in which such backpropagation has to be avoided. With this aim, our partial evaluator takes into account the information about purity of predicates expressed in terms of assertions. This allows some optimizations which are not feasible using existing partial evaluation techniques. We argue that our proposal goes beyond existing ones in that it is a) accurate, since the classification of pure vs impure is done at the level of atoms instead of predicates, b) extensible, as the information about purity can be added to programs using assertions without having to modify the partial evaluator itself, and c) automatic, since (backwards) analysis can be used to automatically infer the required assertions. Our approach has been implemented in the context of CiaoPP, the abstract interpretation-based preprocessor of the Ciao logic programming system.

LPAR Conference 2004 Conference Paper

Abstraction-Carrying Code

• Elvira Albert
• Germán Puebla
• Manuel V. Hermenegildo

Abstract Proof-Carrying Code (PCC) is a general approach to mobile code safety in which programs are augmented with a certificate (or proof). The practical uptake of PCC greatly depends on the existence of a variety of enabling technologies which allow both to prove programs correct and to replace a costly verification process by an efficient checking procedure on the consumer side. In this work we propose Abstraction-Carrying Code (ACC), a novel approach which uses abstract interpretation as enabling technology. We argue that the large body of applications of abstract interpretation to program verification is amenable to the overall PCC scheme. In particular, we rely on an expressive class of safety policies which can be defined over different abstract domains. We use an abstraction (or abstract model) of the program computed by standard static analyzers as a certificate. The validity of the abstraction on the consumer side is checked in a single-pass by a very efficient and specialized abstract-interpreter. We believe that ACC brings the expressiveness, flexibility and automation which is inherent in abstract interpretation techniques to the area of mobile code safety. We have implemented and benchmarked ACC within the Ciao system preprocessor. The experimental results show that the checking phase is indeed faster than the proof generation phase, and that the sizes of certificates are reasonable.

LOPSTR Conference 2004 Conference Paper

Efficient Local Unfolding with Ancestor Stacks for Full Prolog

• Germán Puebla
• Elvira Albert
• Manuel V. Hermenegildo

Abstract The integration of powerful partial evaluation methods into practical compilers for logic programs is still far from reality. This is related both to 1) efficiency issues and to 2) the complications of dealing with practical programs. Regarding efficiency, the most successful unfolding rules used nowadays are based on structural orders applied over (covering) ancestors, i. e. , a subsequence of the atoms selected during a derivation. Unfortunately, maintaining the structure of the ancestor relation during unfolding introduces significant overhead. We propose an efficient, practical local unfolding rule based on the notion of covering ancestors which can be used in combination with any structural order and allows a stack-based implementation without losing any opportunities for specialization. Regarding the second issue, we propose assertion-based techniques which allow our approach to deal with real programs that include (Prolog) built-ins and external predicates in a very extensible manner. Finally, we report on our implementation of these techniques in a practical partial evaluator, embedded in a state of the art compiler which uses global analysis extensively (the Ciao compiler and, specifically, its preprocessor CiaoPP ). The performance analysis of the resulting system shows that our techniques, in addition to dealing with practical programs, are also significantly more efficient in time and somewhat more efficient in memory than traditional tree-based implementations.

LOPSTR Conference 2001 Conference Paper

Symbolic Profiling for Multi-paradigm Declarative Languages

• Elvira Albert
• Germán Vidal

Abstract We present the basis of a source-level profiler for multi-paradigm declarative languages which integrate features from (lazy) functional and logic programming. Our profiling scheme is symbolic in the sense that it is independent of the particular language implementation. This is achieved by counting the number of basic operations performed during the execution of program calls, e. g. , the number of unfolding steps, the number of matching operations, etc. The main contribution of this paper is the formal specification of the attribution of execution costs to cost centers, which is particularly difficult in the context of lazy languages. A prototype implementation of the symbolic profiler has been undertaken for the multi-paradigm language Curry. Preliminary results demonstrate the practicality of our approach and its applications in the field of program transformation.

LOPSTR Conference 2000 Conference Paper

Measuring the Effectiveness of Partial Evaluation

• Elvira Albert
• Sergio Antoy
• Germán Vidal

LPAR Conference 2000 Conference Paper

Using an Abstract Representation to Specialize Functional Logic Programs

• Elvira Albert
• Michael Hanus
• Germán Vidal

Abstract This paper introduces a novel approach for the specialization of functional logic languages. We consider a maximally simplified abstract representation of programs (which still contains all the necessary information) and define a non-standard semantics for these programs. Both things mixed together allow us to design a simple and concise partial evaluation method for modern functional logic languages, avoiding several limitations of previous approaches. Moreover, since these languages can be automatically translated into the abstract representation, our technique is widely applicable. In order to assess the practicality of our approach, we have developed a partial evaluation tool for the multi-paradigm language Curry. The partial evaluator is written in Curry itself and has been tested on an extensive benchmark suite (even a meta-interpreter). To the best of our knowledge, this is the first purely declarative partial evaluator for a functional logic language.

LPAR Conference 1999 Conference Paper

A Partial Evaluation Framework for Curry Programs

• Elvira Albert
• María Alpuente
• Michael Hanus
• Germán Vidal

Abstract In this work, we develop a partial evaluation technique for residuating functional logic programs, which generalize the concurrent computation models for logic programs with delays to functional logic programs. We show how to lift the nondeterministic choices from run time to specialization time. We ascertain the conditions under which the original and the transformed program have the same answer expressions for the considered class of queries as well as the same floundering behavior. All these results are relevant for program optimization in Curry, a functional logic language which is intended to become a standard in this area. Preliminary empirical evaluation of the specialized Curry programs demonstrates that our technique also works well in practice and leads to substantial performance improvements. To our knowledge, this work is the first attempt to formally define and prove correct a general scheme for the partial evaluation of functional logic programs with delays.