Semantic Optimization of Queries in Deductive Object-Oriented Database. - Marcelo F. Frias; Silvia E. Gordillo (ADBIS, 1995)

PLATO: A Tool to Assist Programming as Term Rewriting and Therem Proving. - Andre J. Sampaio; Armando Martin Haeberer; Claudio T. Prates; Cristina D. Ururahy; Marcelo F. Frias; Neudson C. Albuquerque (TAPSOFT, 1995)

Adding Design Strategies to Fork Algebras. - Marcelo F. Frias; Gabriel Baum; Armando Martin Haeberer (Ershov Memorial Conference, 1996)

From Specifications to Programs: A Fork-Algebraic Approach to Bridge the Gap. - Gabriel Baum; Marcelo F. Frias; Armando Martin Haeberer; Pablo E. Martínez López (MFCS, 1996)

Fork Algebras. - Armando Martin Haeberer; Marcelo F. Frias; Gabriel Baum; Paulo A. S. Veloso (Relational Methods in Computer Science, 1997)

Representability and Program Construction within Fork Algebras (Part II). - Marcelo F. Frias; Gabriel Baum; Armando Martin Haeberer (RelMiCS, 1997)

Completeness of the Relational Calculus MU2. - Marcelo F. Frias; Roger D. Maddux (RelMiCS, 1997)

Fork Algebras in Algebra, Logic and Computer Science. - Marcelo F. Frias; Gabriel Baum; Armando Martin Haeberer (Fundam. Informaticae, 1997)

A Finite Axiomatization for Fork Algebras. - Marcelo F. Frias; Armando Martin Haeberer; Paulo A. S. Veloso (Log. J. IGPL, 1997)

A calculus for program construction based on fork algebras, generic algorithms and design strategies. - Marcelo F. Frias; Gabriel Baum; Armando Martin Haeberer (RelMiCS, 1998)

A Logic for Real-Time Systems Specification, Its Algebraic Semantics, and Equational Calculus. - Gabriel Baum; Marcelo F. Frias; T. S. E. Maibaum (AMAST, 1998)

Representability and Program Construction within Fork Algebras. - Marcelo F. Frias; Gabriel Baum; Armando Martin Haeberer (Log. J. IGPL, 1998)

Editorial. - Marcelo F. Frias; Armando Martin Haeberer (Log. J. IGPL, 1998)

Equational Reasoning in Non–Classical Logics. - Marcelo F. Frias; Ewa Orlowska (J. Appl. Non Class. Logics, 1998)

How to say Greedy in Fork Algebras. - Marcelo F. Frias; Gabriel Baum; Esteban de la Canal (RelMiCS, 2000)

Interpretability of First-Order Dynamic Logic in a Relational Calculus. - Marcelo F. Frias; Gabriel Baum; T. S. E. Maibaum (RelMiCS, 2001)

Completeness of a relational calculus for program schemes. - Marcelo F. Frias; Roger D. Maddux (Theor. Comput. Sci., 2001)

Fork Algebras in Algebra, Logic and Computer Science - Marcelo F. Frias (World Scientific, 2002)

Taking Alloy to the Movies. - Marcelo F. Frias; Carlos López Pombo; Gabriel Baum; Nazareno Aguirre; T. S. E. Maibaum (FME, 2003)

An Equational Calculus for Alloy. - Marcelo F. Frias; Carlos López Pombo; Nazareno Aguirre (ICFEM, 2004)

DynAlloy: upgrading alloy with actions. - Marcelo F. Frias; Juan P. Galeotti; Carlos López Pombo; Nazareno Aguirre (ICSE, 2005)

A strategy for efficient verification of relational specifications, based on monotonicity analysis. - Marcelo F. Frias; Rodolfo Gamarra; Gabriela Steren; Lorena Bourg (ASE, 2005)

Reasoning about static and dynamic properties in alloy: A purely relational approach. - Marcelo F. Frias; Carlos López Pombo; Gabriel A. Baum; Nazareno Aguirre; T. S. E. Maibaum (ACM Trans. Softw. Eng. Methodol., 2005)

Monotonicity Analysis Can Speed Up Verification. - Marcelo F. Frias; Rodolfo Gamarra; Gabriela Steren; Lorena Bourg (RelMiCS, 2006)

Fork Algebras as a Sufficiently Rich Universal Institution. - Carlos López Pombo; Marcelo F. Frias (AMAST, 2006)

DynAlloy as a Formal Method for the Analysis of Java Programs. - Juan P. Galeotti; Marcelo F. Frias (SET, 2006)

Interpretability of first-order linear temporal logics in fork algebras. - Marcelo F. Frias; Carlos López Pombo (J. Log. Algebraic Methods Program., 2006)

Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications. - Marcelo F. Frias; Carlos López Pombo; Mariano M. Moscato (TACAS, 2007)

Efficient Analysis of DynAlloy Specifications. - Marcelo F. Frias; Carlos López Pombo; Juan P. Galeotti; Nazareno Aguirre (ACM Trans. Softw. Eng. Methodol., 2007)

Towards Abstraction for DynAlloy Specifications. - Nazareno Aguirre; Marcelo F. Frias; Pablo Ponzio; Brian J. Cardiff; Juan P. Galeotti; Germán Regis (ICFEM, 2008)

Describing and Analyzing Behaviours over Tabular Specifications Using (Dyn)Alloy. - Nazareno Aguirre; Marcelo F. Frias; Mariano M. Moscato; T. S. E. Maibaum; Alan Wassyng (FASE, 2009)

Alloy+HotCore: A Fast Approximation to Unsat Core. - Nicolás D'Ippolito; Marcelo F. Frias; Juan P. Galeotti; Esteban Lanzarotti; Sergio Mera (ASM, 2010)

ParAlloy: Towards a Framework for Efficient Parallel Analysis of Alloy Models. - Nicolás Rosner; Juan P. Galeotti; Carlos López Pombo; Marcelo F. Frias (ASM, 2010)

Dynamite 2.0: New Features Based on UnSAT-Core Extraction to Improve Verification of Software Requirements. - Mariano M. Moscato; Carlos López Pombo; Marcelo F. Frias (ICTAC, 2010)

Complete Calculi for Structured Specifications in Fork Algebra. - Carlos Gustavo López Pombo; Marcelo Fabiùn Frias (ICTAC, 2010)

Analysis of invariants for efficient bounded verification. - Juan P. Galeotti; Nicolás Rosner; Carlos López Pombo; Marcelo F. Frias (ISSTA, 2010)

A Dataflow Analysis to Improve SAT-Based Bounded Program Verification. - Bruno Cuervo Parrino; Juan P. Galeotti; Diego Garbervetsky; Marcelo F. Frias (SEFM, 2011)

Incorporating Coverage Criteria in Bounded Exhaustive Black Box Test Generation of Structural Inputs. - Nazareno Aguirre; Valeria S. Bengolea; Marcelo F. Frias; Juan P. Galeotti (TAP@TOOLS, 2011)

Abstraction Based Automated Test Generation from Formal Tabular Requirements Specifications. - Renzo Degiovanni; Pablo Ponzio; Nazareno Aguirre; Marcelo F. Frias (TAP@TOOLS, 2011)

Using Coverage Criteria on RepOK to Reduce Bounded-Exhaustive Test Suites. - Valeria S. Bengolea; Nazareno Aguirre; Darko Marinov; Marcelo F. Frias (TAP@TOOLS, 2012)

Improving Test Generation under Rich Contracts by Tight Bounds and Incremental SAT Solving. - Pablo Abad; Nazareno Aguirre; Valeria S. Bengolea; Daniel Alfredo Ciolek; Marcelo F. Frias; Juan P. Galeotti; Tom Maibaum; Mariano M. Moscato; Nicolás Rosner; Ignacio Vissani (ICST, 2013)

Parallel bounded analysis in code with rich invariants by refinement of field bounds. - Nicolás Rosner; Juan P. Galeotti; Santiago Bermúdez; Guido Marucci Blas; Santiago Perez De Rosso; Lucas Pizzagalli; Luciano Zemín; Marcelo F. Frias (ISSTA, 2013)

Ranger: Parallel analysis of alloy models by range partitioning. - Nicolás Rosner; Junaid Haroon Siddiqui; Nazareno Aguirre; Sarfraz Khurshid; Marcelo F. Frias (ASE, 2013)

Bounded Lazy Initialization. - Jaco Geldenhuys; Nazareno Aguirre; Marcelo F. Frias; Willem Visser (NASA Formal Methods, 2013)

Parallel Bounded Verification of Alloy Models by TranScoping. - Nicolás Rosner; Carlos Gustavo López Pombo; Nazareno Aguirre; Ali Jaoua; Ali Mili 001; Marcelo F. Frias (VSTTE, 2013)

HeteroGenius: A Framework for Hybrid Analysis of Heterogeneous Software Specifications. - Manuel Giménez; Mariano M. Moscato; Carlos Gustavo López Pombo; Marcelo F. Frias (LAFM, 2013)

TACO: Efficient SAT-Based Bounded Verification Using Symmetry Breaking and Tight Bounds. - Juan P. Galeotti; Nicolás Rosner; Carlos Gustavo López Pombo; Marcelo F. Frias (IEEE Trans. Software Eng., 2013)

On Faults and Faulty Programs. - Ali Mili 001; Marcelo F. Frias; Ali Jaoua (RAMiCS, 2014)

Efficient Tight Field Bounds Computation Based on Shape Predicates. - Pablo Ponzio; Nicolás Rosner; Nazareno Aguirre; Marcelo F. Frias (FM, 2014)

Bounded exhaustive test input generation from hybrid invariants. - Nicolás Rosner; Valeria S. Bengolea; Pablo Ponzio; Shadi Abdul Khalek; Nazareno Aguirre; Marcelo F. Frias; Sarfraz Khurshid (OOPSLA, 2014)

Semantic metrics for software products. - Ali Mili 001; Ali Jaoua; Marcelo F. Frias; Rasha Gaffer Mohamed Helali (Innov. Syst. Softw. Eng., 2014)

Inference engine based on closure and join operators over Truth Table Binary Relations. - Samir Elloumi; Bilel Boulifa; Ali Jaoua; Mohammad Saleh; Jameela Al Otaibi; Marcelo F. Frias (J. Log. Algebraic Methods Program., 2014)

RepOK-based reduction of bounded exhaustive testing. - Valeria S. Bengolea; Nazareno Aguirre; Darko Marinov; Marcelo F. Frias (Softw. Test. Verification Reliab., 2014)

Dynamite: A tool for the verification of alloy models based on PVS. - Mariano M. Moscato; Carlos López Pombo; Marcelo F. Frias (ACM Trans. Softw. Eng. Methodol., 2014)

Relational Mathematics for Relative Correctness. - Jules Desharnais; Nafi Diallo; Wided Ghardallou; Marcelo F. Frias; Ali Jaoua; Ali Mili 001 (RAMiCS, 2015)

Model Counting for Complex Data Structures. - Antonio Filieri; Marcelo F. Frias; Corina S. Pasareanu; Willem Visser (SPIN, 2015)

TacoFlow: optimizing SAT program verification using dataflow analysis. - Bruno Cuervo Parrino; Juan Pablo Galeotti; Diego Garbervetsky; Marcelo F. Frias (Softw. Syst. Model., 2015)

BLISS: Improved Symbolic Execution by Bounded Lazy Initialization with SAT Support. - Nicolás Rosner; Jaco Geldenhuys; Nazareno Aguirre; Willem Visser; Marcelo F. Frias (IEEE Trans. Software Eng., 2015)

Debugging without Testing. - Wided Ghardallou; Nafi Diallo; Ali Mili 001; Marcelo F. Frias (ICST, 2016)

An Evolutionary Approach to Translate Operational Specifications into Declarative Specifications. - Facundo Molina; César Cornejo; Renzo Degiovanni; Germán Regis; Pablo F. Castro; Nazareno Aguirre; Marcelo F. Frias (SBMF, 2016)

Field-exhaustive testing. - Pablo Ponzio; Nazareno Aguirre; Marcelo F. Frias; Willem Visser (SIGSOFT FSE, 2016)

An Analysis of the Suitability of Test-Based Patch Acceptance Criteria. - Luciano Zemín; Simón Gutiérrez Brida; Ariel Godio; César Cornejo; Renzo Degiovanni; Germán Regis; Nazareno Aguirre; Marcelo F. Frias (SBST@ICSE, 2017)

DynAlloy analyzer: a tool for the specification and analysis of alloy models with dynamic behaviour. - Germán Regis; César Cornejo; Simón Gutiérrez Brida; Mariano Politano; Fernando D. Raverta; Pablo Ponzio; Nazareno Aguirre; Juan Pablo Galeotti; Marcelo F. Frias (ESEC/SIGSOFT FSE, 2017)

What is a fault? and why does it matter? - Nafi Diallo; Wided Ghardallou; Jules Desharnais; Marcelo F. Frias; Ali Jaoua; Ali Mili 001 (Innov. Syst. Softw. Eng., 2017)

Goal-conflict likelihood assessment based on model counting. - Renzo Degiovanni; Pablo F. Castro; Marcelo Arroyo; Marcelo Ruiz; Nazareno Aguirre; Marcelo F. Frias (ICSE, 2018)

From operational to declarative specifications using a genetic algorithm. - Facundo Molina; Renzo Degiovanni; Germán Regis; Pablo F. Castro; Nazareno Aguirre; Marcelo F. Frias (SBST@ICSE, 2018)

On the effect of object redundancy elimination in randomly testing collection classes. - Pablo Ponzio; Valeria S. Bengolea; Simón Gutiérrez Brida; Gastón Scilingo; Nazareno Aguirre; Marcelo F. Frias (SBST@ICSE, 2018)

Automated workarounds from Java program specifications based on SAT solving. - Marcelo Uva; Pablo Ponzio; Germán Regis; Nazareno Aguirre; Marcelo F. Frias (Int. J. Softw. Tools Technol. Transf., 2018)

Improving lazy abstraction for SCR specifications through constraint relaxation. - Renzo Degiovanni; Pablo Ponzio; Nazareno Aguirre; Marcelo F. Frias (Softw. Test. Verification Reliab., 2018)

Automatically Identifying Sufficient Object Builders from Module APIs. - Pablo Ponzio; Valeria S. Bengolea; Mariano Politano; Nazareno Aguirre; Marcelo F. Frias (FASE, 2019)

Training binary classifiers as data structure invariants. - Facundo Molina; Renzo Degiovanni; Pablo Ponzio; Germán Regis; Nazareno Aguirre; Marcelo F. Frias (ICSE, 2019)

Efficient Test Generation Guided by Field Coverage Criteria. - Ariel Godio; Valeria S. Bengolea; Pablo Ponzio; Nazareno Aguirre; Marcelo Fabian Frias (ASE, 2019)

Stryker: Scaling Specification-Based Program Repair by Pruning Infeasible Mutants with SAT. - Luciano Zemín; Simón Gutiérrez Brida; Santiago Bermúdez; Santiago Perez De Rosso; Nazareno Aguirre; Ali Mili 001; Ali Jaoua; Marcelo F. Frias (CoRR, 2019)

An evolutionary approach to translating operational specifications into declarative specifications. - Facundo Molina; César Cornejo; Renzo Degiovanni; Germán Regis; Pablo F. Castro; Nazareno Aguirre; Marcelo F. Frias (Sci. Comput. Program., 2019)

On the construction of explosive relation algebras. - Carlos Gustavo López Pombo; Marcelo F. Frias; T. S. E. Maibaum (CoRR, 2020)

Efficient Bounded Model Checking of Heap-Manipulating Programs using Tight Field Bounds. - Pablo Ponzio; Ariel Godio; Nicolás Rosner; Marcelo Arroyo; Nazareno Aguirre; Marcelo F. Frias (FASE, 2021)

Bounded Exhaustive Search of Alloy Specification Repairs. - Simón Gutiérrez Brida; Germán Regis; Guolong Zheng; Hamid Bagheri; ThanhVu Nguyen; Nazareno Aguirre; Marcelo F. Frias (ICSE, 2021)

Artifact of Bounded Exhaustive Search of Alloy Specification Repairs. - Simón Gutiérrez Brida; Germán Regis; Guolong Zheng; Hamid Bagheri; ThanhVu Nguyen; Nazareno Aguirre; Marcelo F. Frias (ICSE (Companion Volume), 2021)

EvoSpex: An Evolutionary Algorithm for Learning Postconditions. - Facundo Molina; Pablo Ponzio; Nazareno Aguirre; Marcelo F. Frias (ICSE, 2021)

EvoSpex: An Evolutionary Algorithm for Learning Postconditions (artifact). - Facundo Molina; Pablo Ponzio; Nazareno Aguirre; Marcelo F. Frias (ICSE (Companion Volume), 2021)

FLACK: Counterexample-Guided Fault Localization for Alloy Models. - Guolong Zheng; ThanhVu Nguyen; Simón Gutiérrez Brida; Germán Regis; Marcelo F. Frias; Nazareno Aguirre; Hamid Bagheri (ICSE, 2021)

Artifact of 'FLACK: Counterexample-Guided Fault Localization for Alloy Models'. - Guolong Zheng; ThanhVu Nguyen; Simón Gutiérrez Brida; Germán Regis; Marcelo F. Frias; Nazareno Aguirre; Hamid Bagheri (ICSE (Companion Volume), 2021)

BeAFix: An Automated Repair Tool for Faulty Alloy Models. - Simón Gutiérrez Brida; Germán Regis; Guolong Zheng; Hamid Bagheri; ThanhVu Nguyen; Nazareno Aguirre; Marcelo F. Frias (ASE, 2021)

FLACK: Localizing Faults in Alloy Models. - Guolong Zheng; ThanhVu Nguyen; Simón Gutiérrez Brida; Germán Regis; Marcelo F. Frias; Nazareno Aguirre; Hamid Bagheri (ASE, 2021)

Learning to Prune Infeasible Paths in Generalized Symbolic Execution. - Facundo Molina; Pablo Ponzio; Nazareno Aguirre; Marcelo F. Frias (ISSRE, 2022)

ATR: template-based repair for Alloy specifications. - Guolong Zheng; ThanhVu Nguyen; Simón Gutiérrez Brida; Germán Regis; Nazareno Aguirre; Marcelo F. Frias; Hamid Bagheri (ISSTA, 2022)

ICEBAR: Feedback-Driven Iterative Repair of Alloy Specifications. - Simón Gutiérrez Brida; Germán Regis; Guolong Zheng; Hamid Bagheri; ThanhVu Nguyen; Nazareno Aguirre; Marcelo F. Frias (ASE, 2022)

LISSA: Lazy Initialization with Specialized Solver Aid. - Juan Manuel Copia; Pablo Ponzio; Nazareno Aguirre; Alessandra Gorla; Marcelo F. Frias (ASE, 2022)

Efficient Bounded Exhaustive Input Generation from Program APIs. - Mariano Politano; Valeria S. Bengolea; Facundo Molina; Nazareno Aguirre; Marcelo F. Frias; Pablo Ponzio (FASE, 2023)

Precise Lazy Initialization for Programs with Complex Heap Inputs. - Juan Manuel Copia; Facundo Molina; Nazareno Aguirre; Marcelo F. Frias; Alessandra Gorla; Pablo Ponzio (ISSRE, 2023)

EvoSpex: A Search-Based Tool for Postcondition Inference. - Facundo Molina; Pablo Ponzio; Nazareno Aguirre; Marcelo F. Frias (ISSTA, 2023)

A Study of the Electrum and DynAlloy Dynamic Behavior Notations. - César Cornejo; Germán Regis; Nazareno Aguirre; Marcelo F. Frias (IEEE Trans. Software Eng., 2023)

An Analysis of the Impact of Field-Value Instance Navigation in Alloy's Model Finding. - César Cornejo; María Marta Novaira; Sonia Permigiani; Nazareno Aguirre; Marcelo F. Frias; Simón Gutiérrez Brida; Germán Regis (ABZ, 2024)

Abstraction-Aware Inference of Metamorphic Relations. - Agustín Nolasco; Facundo Molina; Renzo Degiovanni; Alessandra Gorla; Diego Garbervetsky; Mike Papadakis; Sebastián Uchitel; Nazareno Aguirre; Marcelo F. Frias (Proc. ACM Softw. Eng., 2024)

BEAPI: A tool for bounded exhaustive input generation from APIs. - Mariano Politano; Valeria S. Bengolea; Facundo Molina; Nazareno Aguirre; Marcelo F. Frias; Pablo Ponzio (Sci. Comput. Program., 2024)

Abstraction-Aware Inference of Metamorphic Relations (Replication Package). - Agustín Nolasco; Facundo Molina; Renzo Degiovanni; Alessandra Gorla; Diego Garbervetsky; Mike Papadakis; Sebastián Uchitel; Nazareno Aguirre; Marcelo F. Frias (Zenodo, 2024)

An Empirical Study on the Suitability of Test-based Patch Acceptance Criteria. - Luciano Zemín; Ariel Godio; César Cornejo; Renzo Degiovanni; Simón Gutiérrez Brida; Germán Regis; Nazareno Aguirre; Marcelo Fabian Frias (ACM Trans. Softw. Eng. Methodol., 2025)