About me I am a software engineer at Synopsys working in the Software Integrity Group. Previously, I was a postdoc working on static analysis and automated software verification with Arie Gurfinkel at the University of Waterloo. I obtained my PhD in Artificial Intelligence at UPM while working in the IMDEA Software Institute with an FPU scholarship. I was part of the development team of the Ciao programming language, specially focused on the abstract interpreter of its preprocessor, CiaoPP. My research interests include static analysis and verification of software, abstract interpretation, (constraint) logic programming, and semantic code search. Particularly, I am interested in the scalability challenges that these techniques pose.

Isabel Garcia-Contreras, Ph.D. Ontario, Canada

Education

school PhD in Artificial Intelligence - Universidad Politécnica de Madrid
Thesis: A scalable static analysis framework for reliable program development exploiting incrementality and modularity
(DOI: 10.20868/UPM.thesis.68446) [slides]

school MSc in Artificial Intelligence - Universidad Politécnica de Madrid
Master Thesis: Code Search: A Semantic, Abstract Interpretation-based Approach

school Bachelor in Computer Engineering - Universidad Autónoma de Madrid
Final Project: Accelerating Multigigabit Ethernet Network Flow Generation using Dedicated Hardware (Spanish)

Selected publications

• Btor2MLIR: A Format for Hardware Verification. FMCAD'23 (to appear)
  J Tafese, I Garcia-Contreras, A Gurfinkel. [arXiv]
• Fast Approximations of Quantifier Elimination. CAV'23 (Distinguished Paper)
  I Garcia-Contreras, HG V K, S Shoham, A Gurfinkel. (DOI: 10.1007/978-3-031-37703-7_4) [arXiv] [slides]
• Efficient Modular SMT-Based Model Checking of Pointer Programs. SAS'22
  I Garcia-Contreras, A Gurfinkel, JA Navas. (DOI: 10.1007/978-3-031-22308-2_11)
• VeriFly: On-the-fly Assertion Checking via Incrementality. ICLP'21
  MA Sanchez-Ordaz, I Garcia-Contreras, V Perez-Carrasco, JF Morales, P Lopez-Garcia, MV Hermenegildo. (DOI: 10.1017/S1471068421000430)
• Incremental and Modular Context-sensitive Analysis. TPLP'21
  I Garcia-Contreras, JF Morales, MV Hermenegildo. (DOI: 10.1017/S1471068420000496). [arXiv][slides]
• Abstract Extensionality – On the Properties of Incomplete Abstract Interpretations. POPL'2020
  R Bruni, R Giacobazzi, R Gori, I Garcia-Contreras, and D Pavlovic. (DOI: 10.1145/3371096).
• Incremental Analysis of Logic Programs with Assertions and Open Predicates. LOPSTR'19
  I Garcia-Contreras, JF Morales, and MV Hermenegildo. (DOI: 10.1007/978-3-030-45260-5_3). [slides]
• Multivariant Assertion-based Guidance in Abstract Interpretation. LOPSTR'18
  I Garcia-Contreras, JF Morales, and MV Hermenegildo. (DOI: 10.1007/978-3-030-13838-7_11). [slides]
• Semantic Code Browsing. ICLP'16
  I Garcia-Contreras, JF Morales, and MV Hermenegildo. (DOI: 10.1017/S1471068416000417). [slides]

Service

• 2023: LOPSTR'23, FMCAD'23 Student Forum
• 2022: SOAP'22, CAV'22 , HSCC'22 (RE)
• 2021: CAV'21 (AE), VMCAI'21 (AE)
• Conference reviews: TACAS'23, NFM'22, TACAS'22, ICLP'19, ICLP'18, LOPSTR'16

Teaching

• Software Testing, Quality Assurance, and Maintenance (TA), University of Waterloo, Canada. Winter 2022.
• Declarative programming: Logic and constraints (TA), Technical University of Madrid (UPM). (Feb - July) on 2019, 2020, and 2021.