👋 Hi! I’m Juan Manuel Copia.

I’m a software development engineer at Amazon and PhD researcher in Computer Science (IMDEA Software Institute, Universidad Politécnica de Madrid, advised by Alessandra Gorla).

My career bridges academic innovation and industrial software engineering, connecting deep research in program analysis and automated reasoning with the design, development, and deployment of scalable, real-world systems.

Currently, as a Software Development Engineer at Amazon, I design and deploy high-throughput services using AWS technologies (API Gateway, Lambda, DynamoDB, CDK). I also develop AI-driven solutions to boost developer velocity and service resilience.

My PhD research focuses on Software Analysis and Verification. I build systems that merge Symbolic Execution, Search-Based Optimization, and LLMs to automatically infer properties, detect flaws, and validate patch correctness.


Research & Engineering Interests

I’m passionate about building intelligent, agentic software that can reason, adapt, and collaborate autonomously. My current interests span:

  • AI: AI-assisted software engineering, AI agents and infrastructure for scalable, data-driven products.
  • Program Analysis & Lightweight Formal Methods: Symbolic execution, Search-based optimization, Software reliability and automated testing.

My long-term goal is to merge my background in software systems with modern AI techniques to design tools and systems that learn, self-improve, and operate at scale.


Publications

Search-based Inference of Class Invariants: How far can Simulated Annealing take us? J. M. Copia, F. Molina, N. Aguirre, M. Frias, A. Gorla, P. Ponzio. To appear in Symposium on Search-Based Software Engineering (SSBSE '25), Seoul, Republic of Korea, November 2025.

Search-based Inference of Class Invariants (Poster) J. M. Copia, F. Molina, N. Aguirre, M. Frias, A. Gorla, P. Ponzio. In 2025 Genetic and Evolutionary Computation Conference (GECCO '25), Malaga, Spain. [ https ]

Improving Patch Correctness Analysis via Random Testing and Large Language Models Facundo Molina, Juan Manuel Copia, Alessandra Gorla. In Proceedings of the 17th IEEE International Conference on Software Testing, Verification and Validation (ICST '24), Toronto, Canada, May 2024. [ https | .pdf  ]

Precise Lazy Initialization for Programs with Complex Heap Inputs Juan Manuel Copia, Facundo Molina, Nazareno Aguirre, Marcelo Frias, Alessandra Gorla, and Pablo Ponzio. In the 34th IEEE International Symposium on Software Reliability Engineering (ISSRE '23), Florence, Italy, October 2023. [ https | .pdf  ]

LISSA: Lazy Initialization with Specialized Solver Aid Juan Manuel Copia, Pablo Ponzio, Nazareno Aguirre, Alessandra Gorla, and Marcelo Frias. In the 37th IEEE/ACM International Conference on Automated Software Engineering (ASE '22), Oakland Center, Michigan, USA, October 2022. [ https | .pdf  ]

Use of Test Doubles in Android Testing: An In-Depth Investigation Mattia Fazzini, Chase Choi, Juan Manuel Copia, Gabriel Lee, Yoshiki Kakehi, Alessandra Gorla, and Alessandro Orso. In Proceedings of the 44th International Conference on Software Engineering (ICSE '22), Pittsburgh, USA, May 2022. [ https | .pdf  ]


Software Artifacts

Express — A tool that automatically infers method preconditions and class invariants using search-based algorithms. It generates executable predicates (Java code) for complex heap-allocated objects. [ code ]

FixCheck — A tool for improving patch correctness analysis in Java. It integrates static analysis, random testing, and large language models (LLMs) to generate tests that highlight and explain potential patch inconsistencies. [ code ]

PLI — A symbolic execution framework built on top of Java Symbolic PathFinder (JPF). It enhances symbolic reasoning for complex heap-allocated inputs, improving precision and scalability. [ code ]

SymSolve — A bounded exhaustive solver for symbolic structures with complex representation invariants. It determines the satisfiability of partially symbolic heaps via operational specifications. [ code ]

PySEAT — A symbolic execution engine for Python that applies lazy initialization to automate test generation and achieve high coverage in complex programs. [ code | .pdf ]


Contact

Email: jmcopia96@gmail.com

You can find my full CV here.