The Def-inite Approach to Dependency Analysis. - Samir Genaim; Michael Codish (ESOP, 2001)

Higher-Precision Groundness Analysis. - Michael Codish; Samir Genaim; Harald Søndergaard; Peter J. Stuckey (ICLP, 2001)

Worst-case groundness analysis using definite boolean functions. - Samir Genaim; Jacob M. Howe; Michael Codish (Theory Pract. Log. Program., 2001)

Reuse of Results in Termination Analysis of Typed Logic Programs. - Maurice Bruynooghe; Michael Codish; Samir Genaim; Wim Vanhoof (SAS, 2002)

Combining Norms to Prove Termination. - Samir Genaim; Michael Codish; John P. Gallagher; Vitaly Lagoon (VMCAI, 2002)

Goal-Independent Suspension Analysis for Logic Programs with Dynamic Scheduling. - Samir Genaim; Andy King (ESOP, 2003)

Proving Termination One Loop at a Time. - Michael Codish; Samir Genaim (WLPE, 2003)

Information Flow Analysis for Java Bytecode. - Samir Genaim; Fausto Spoto (VMCAI, 2005)

Inferring Termination Conditions for Logic Programs using Backwards Analysis. - Samir Genaim; Michael Codish (Theory Pract. Log. Program., 2005)

Detecting Determinacy in Prolog Programs. - Andy King; Lunjin Lu; Samir Genaim (ICLP, 2006)

Cost Analysis of Java Bytecode. - Elvira Albert; Puri Arenas; Samir Genaim; Germán Puebla; Damiano Zanardini (ESOP, 2007)

COSTA: Design and Implementation of a Cost and Termination Analyzer for Java Bytecode. - Elvira Albert; Puri Arenas; Samir Genaim; German Puebla; Damiano Zanardini (FMCO, 2007)

Heap space analysis for java bytecode. - Elvira Albert; Samir Genaim; Miguel Gómez-Zamalloa (ISMM, 2007)

Experiments in Cost Analysis of Java Bytecode. - Elvira Albert; Puri Arenas; Samir Genaim; Germán Puebla; Damiano Zanardini (Bytecode@ETAPS, 2007)

Termination analysis of logic programs through combination of type-based norms. - Maurice Bruynooghe; Michael Codish; John P. Gallagher; Samir Genaim; Wim Vanhoof (ACM Trans. Program. Lang. Syst., 2007)

Termination Analysis of Java Bytecode. - Elvira Albert; Puri Arenas; Michael Codish; Samir Genaim; Germán Puebla; Damiano Zanardini (FMOODS, 2008)

Removing useless variables in cost analysis of Java bytecode. - Elvira Albert; Puri Arenas; Samir Genaim; Germán Puebla; Damiano Zanardini (SAC, 2008)

Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis. - Elvira Albert; Puri Arenas; Samir Genaim; Germán Puebla (SAS, 2008)

Cost Relation Systems: A Language-Independent Target Language for Cost Analysis. - Elvira Albert; Puri Arenas; Samir Genaim; Germán Puebla (PROLE, 2008)

Inferring non-suspension conditions for logic programs with dynamic scheduling. - Samir Genaim; Andy King (ACM Trans. Comput. Log., 2008)

Asymptotic Resource Usage Bounds. - Elvira Albert; Diego Esteban Alonso-Blas; Puri Arenas; Samir Genaim; German Puebla (APLAS, 2009)

Field-Sensitive Value Analysis by Field-Insensitive Analysis. - Elvira Albert; Puri Arenas; Samir Genaim; Germán Puebla (FM, 2009)

Comparing Cost Functions in Resource Analysis. - Elvira Albert; Puri Arenas; Samir Genaim; Israel Herraiz; German Puebla (FOPARA, 2009)

Resource Usage Analysis and Its Application to Resource Certification. - Elvira Albert; Puri Arenas; Samir Genaim; Germán Puebla; Damiano Zanardini (FOSAD, 2009)

Live heap space analysis for languages with garbage collection. - Elvira Albert; Samir Genaim; Miguel Gómez-Zamalloa (ISMM, 2009)

A declarative encoding of telecommunications feature subscription in SAT. - Michael Codish; Samir Genaim; Peter J. Stuckey (PPDP, 2009)

Termination and Cost Analysis with COSTA and its User Interfaces. - Elvira Albert; Puri Arenas; Samir Genaim; Miguel Gómez-Zamalloa; German Puebla; Diana V. Ramírez-Deantes; Guillermo Román-Díez; Damiano Zanardini (PROLE, 2009)

Preface. - Elvira Albert; Samir Genaim (BYTECODE@ETAPS, 2009)

Parametric inference of memory requirements for garbage collected languages. - Elvira Albert; Samir Genaim; Miguel Gómez-Zamalloa (ISMM, 2010)

From Object Fields to Local Variables: A Practical Approach to Field-Sensitive Analysis. - Elvira Albert; Puri Arenas; Samir Genaim; German Puebla; Diana V. Ramírez-Deantes (SAS, 2010)

Cost Analysis of Concurrent OO Programs. - Elvira Albert; Puri Arenas; Samir Genaim; Miguel Gómez-Zamalloa; German Puebla (APLAS, 2011)

Simulating Concurrent Behaviors with Worst-Case Cost Bounds. - Elvira Albert; Samir Genaim; Miguel Gómez-Zamalloa; Einar Broch Johnsen; Rudolf Schlatte; Silvia Lizeth Tapia Tarifa (FM, 2011)

Task-level analysis for a language with async/finish parallelism. - Elvira Albert; Puri Arenas; Samir Genaim; Damiano Zanardini (LCTES, 2011)

Verified resource guarantees using COSTA and KeY. - Elvira Albert; Richard Bubel; Samir Genaim; Reiner Hähnle; Germán Puebla; Guillermo Román-Díez (PEPM, 2011)

More Precise Yet Widely Applicable Cost Analysis. - Elvira Albert; Samir Genaim; Abu Naser Masud (VMCAI, 2011)

Handling Non-linear Operations in the Value Analysis of COSTA. - Diego Esteban Alonso-Blas; Puri Arenas; Samir Genaim (Bytecode@ETAPS, 2011)

Closed-Form Upper Bounds in Static Cost Analysis. - Elvira Albert; Puri Arenas; Samir Genaim; Germán Puebla (J. Autom. Reason., 2011)

Verified Resource Guarantees for Heap Manipulating Programs. - Elvira Albert; Richard Bubel; Samir Genaim; Reiner Hähnle; Guillermo Román-Díez (FASE, 2012)

Automatic Inference of Bounds on Resource Consumption. - Elvira Albert; Diego Esteban Alonso-Blas; Puri Arenas; Jesús Correas; Antonio Flores-Montoya; Samir Genaim; Miguel Gómez-Zamalloa; Abu Naser Masud; German Puebla; José Miguel Rojas; Guillermo Román-Díez; Damiano Zanardini (FMCO, 2012)

Analysis of May-Happen-in-Parallel in Concurrent Objects. - Elvira Albert; Antonio Flores-Montoya; Samir Genaim (FMOODS/FORTE, 2012)

Automatic Inference of Resource Consumption Bounds. - Elvira Albert; Puri Arenas; Samir Genaim; Miguel Gómez-Zamalloa; Germán Puebla (LPAR, 2012)

COSTABS: a cost and termination analyzer for ABS. - Elvira Albert; Puri Arenas; Samir Genaim; Miguel Gómez-Zamalloa; Germán Puebla (PEPM, 2012)

On the Limits of the Classical Approach to Cost Analysis. - Diego Esteban Alonso-Blas; Samir Genaim (SAS, 2012)

MayPar: a may-happen-in-parallel analyzer for concurrent objects. - Elvira Albert; Antonio Flores-Montoya; Samir Genaim (SIGSOFT FSE, 2012)

Cost analysis of object-oriented bytecode programs. - Elvira Albert; Puri Arenas; Samir Genaim; German Puebla; Damiano Zanardini (Theor. Comput. Sci., 2012)

On the Termination of Integer Loops. - Amir M. Ben-Amram; Samir Genaim; Abu Naser Masud (ACM Trans. Program. Lang. Syst., 2012)

Termination and Cost Analysis of Loops with Concurrent Interleavings. - Elvira Albert; Antonio Flores-Montoya; Samir Genaim; Enrique Martin-Martin (ATVA, 2013)

Precise Cost Analysis via Local Reasoning. - Diego Esteban Alonso-Blas; Puri Arenas; Samir Genaim (ATVA, 2013)

Proving Termination Starting from the End. - Pierre Ganty; Samir Genaim (CAV, 2013)

May-Happen-in-Parallel Based Deadlock Analysis for Concurrent Objects. - Antonio Flores-Montoya; Elvira Albert; Samir Genaim (FMOODS/FORTE, 2013)

A Transformational Approach to Resource Analysis with Typed-Norms. - Elvira Albert; Samir Genaim; Raúl Gutiérrez (LOPSTR, 2013)

May-Happen-in-Parallel Analysis for Priority-Based Scheduling. - Elvira Albert; Samir Genaim; Enrique Martin-Martin (LPAR, 2013)

On the linear ranking problem for integer linear-constraint loops. - Amir M. Ben-Amram; Samir Genaim (POPL, 2013)

Inference of Field-Dependent Cyclicity. - Damiano Zanardini; Samir Genaim (CoRR, 2013)

Heap space analysis for garbage collected languages. - Elvira Albert; Samir Genaim; Miguel Gómez-Zamalloa (Sci. Comput. Program., 2013)

Reachability-based acyclicity analysis by Abstract Interpretation. - Samir Genaim; Damiano Zanardini (Theor. Comput. Sci., 2013)

Corrigendum to "Reachability-based acyclicity analysis by abstract interpretation" [Theoretical Computer Science 474 (2013) 60-79]. - Samir Genaim; Damiano Zanardini (Theor. Comput. Sci., 2013)

On the Inference of Resource Usage Upper and Lower Bounds. - Elvira Albert; Samir Genaim; Abu Naser Masud (ACM Trans. Comput. Log., 2013)

SACO: Static Analyzer for Concurrent Objects. - Elvira Albert; Puri Arenas; Antonio Flores-Montoya; Samir Genaim; Miguel Gómez-Zamalloa; Enrique Martin-Martin; German Puebla; Guillermo Román-Díez (TACAS, 2014)

Ranking Functions for Linear-Constraint Loops. - Amir M. Ben-Amram; Samir Genaim (J. ACM, 2014)

Conditional termination of loops over heap-allocated data. - Elvira Albert; Puri Arenas; Samir Genaim; Germán Puebla; Guillermo Román-Díez (Sci. Comput. Program., 2014)

Inference of Field-Sensitive Reachability and Cyclicity. - Damiano Zanardini; Samir Genaim (ACM Trans. Comput. Log., 2014)

Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions. - Amir M. Ben-Amram; Samir Genaim (CAV (2), 2015)

Resource Analysis: From Sequential to Concurrent and Distributed Programs. - Elvira Albert; Puri Arenas; Jesús Correas; Samir Genaim; Miguel Gómez-Zamalloa; Enrique Martin-Martin; Germán Puebla; Guillermo Román-Díez (FM, 2015)

May-Happen-in-Parallel Analysis with Condition Synchronization. - Elvira Albert; Antonio Flores-Montoya; Samir Genaim (FOPARA, 2015)

From non-zenoness verification to termination. - Pierre Ganty; Samir Genaim; Ratan Lal; Pavithra Prabhakar (MEMOCODE, 2015)

Preparing HPC Applications for Exascale: Challenges and Recommendations. - Erika Ábrahám; Costas Bekas; Ivona Brandic; Samir Genaim; Einar Broch Johnsen; Ivan Kondov; Sabri Pllana; Achim Streit (NBiS, 2015)

May-Happen-in-Parallel Analysis for Asynchronous Programs with Inter-Procedural Synchronization. - Elvira Albert; Samir Genaim; Pablo Gordillo (SAS, 2015)

A practical comparator of cost functions and its applications. - Elvira Albert; Puri Arenas; Samir Genaim; Germán Puebla (Sci. Comput. Program., 2015)

Object-sensitive cost analysis for concurrent objects. - Elvira Albert; Puri Arenas; Jesús Correas Fernández; Samir Genaim; Miguel Gómez-Zamalloa; Germán Puebla; Guillermo Román-Díez (Softw. Test. Verification Reliab., 2015)

A formal verification framework for static analysis - As well as its instantiation to the resource analyzer COSTA and formal verification tool KeY. - Elvira Albert; Richard Bubel; Samir Genaim; Reiner Hähnle; Germán Puebla; Guillermo Román-Díez (Softw. Syst. Model., 2016)

May-Happen-in-Parallel Analysis for Actor-Based Concurrency. - Elvira Albert; Antonio Flores-Montoya; Samir Genaim; Enrique Martin-Martin (ACM Trans. Comput. Log., 2016)

May-Happen-in-Parallel Analysis with Returned Futures. - Elvira Albert; Samir Genaim; Pablo Gordillo (ATVA, 2017)

On Multiphase-Linear Ranking Functions. - Amir M. Ben-Amram; Samir Genaim (CAV (2), 2017)

EasyInterface: A Toolkit for Rapid Development of GUIs for Research Prototype Tools. - Jesús Doménech; Samir Genaim; Einar Broch Johnsen; Rudolf Schlatte (FASE, 2017)

Rely-Guarantee Termination and Cost Analyses of Loops with Concurrent Interleavings. - Elvira Albert; Antonio Flores-Montoya; Samir Genaim; Enrique Martin-Martin (J. Autom. Reason., 2017)

Multiphase-Linear Ranking Functions and Their Relation to Recurrent Sets. - Amir M. Ben-Amram; Jesús J. Doménech; Samir Genaim (SAS, 2019)

Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis. - Jesús J. Doménech; John P. Gallagher; Samir Genaim (Theory Pract. Log. Program., 2019)

A Transformational Approach to Resource Analysis with Typed-norms Inference. - Elvira Albert; Samir Genaim; Raúl Gutiérrez; Enrique Martin-Martin (Theory Pract. Log. Program., 2020)

Lower-Bound Synthesis Using Loop Specialization and Max-SMT. - Elvira Albert; Samir Genaim; Enrique Martin-Martin; Alicia Merayo; Albert Rubio (CAV (2), 2021)

Termination Analysis of Programs with Multiphase Control-Flow. - Jesús J. Doménech; Samir Genaim (HCVS@ETAPS, 2021)

When COSTA Met KeY: Verified Cost Bounds. - Elvira Albert; Samir Genaim; Alicia Merayo; Guillermo Román-Díez (The Logic of Software. A Tasting Menu of Formal Methods, 2022)

Artifact of the Paper "Formally Verified EVM Block-Optimizations". - Elvira Albert; Samir Genaim; Daniel Kirchner; Enrique Martin-Martin (Zenodo, 2022)

Formally Verified EVM Block-Optimizations. - Elvira Albert; Samir Genaim; Daniel Kirchner; Enrique Martin-Martin (CAV (3), 2023)

Artifact of the Paper "Formally Verified EVM Block-Optimizations". - Elvira Albert; Samir Genaim; Daniel Kirchner; Enrique Martin-Martin (Zenodo, 2023)

Artifact of the Paper "Formally Verified EVM Block-Optimizations". - Elvira Albert; Samir Genaim; Daniel Kirchner; Enrique Martin-Martin (Zenodo, 2023)

Neural-guided superoptimization in ethereum. - Matheus Araújo Aguiar; Elvira Albert; Samir Genaim; Pablo Gordillo; Alejandro Hernández-Cerezo; Daniel Kirchner; Albert Rubio (Inf. Softw. Technol., 2025)

Secure Optimizations on Ethereum Bytecode Jump-Free Sequences. - Elvira Albert; Samir Genaim; Daniel Kirchner; Enrique Martin-Martin (IEEE Trans. Dependable Secur. Comput., 2025)