CV

Academic background, research experience, and selected achievements.

Contact Information

Name Giuseppe Spallitta
Professional Title Postdoctoral Associate in Computer Science

Professional Summary

Researcher in formal verification and automated reasoning, with a focus on model counting and model enumeration for SAT and SMT. Current research investigates the relationship between quantum computing and SAT solving in both directions: using SAT-based techniques for quantum verification and using quantum computing to optimize SAT-solving tasks.

Experience

  • 2025 - present

    Houston, Texas, USA

    Postdoctoral Associate
    Rice University
    Research with Moshe Y. Vardi on model counting and enumeration and their applications to real-world reasoning problems.
  • 2023 - 2023

    Freiburg, Germany

    Visiting Researcher
    University of Freiburg
    Several-month research visit under the supervision of Armin Biere, working on SAT and SMT model-enumeration techniques.
  • 2020 - 2025

    Trento, Italy

    Doctoral Researcher
    University of Trento
    Research in formal verification and automated reasoning, focusing on efficient procedures and applications for AllSAT and AllSMT.
    • Teaching assistant for Formal Methods and Automated Reasoning.

Education

  • 2020 - 2025

    Trento, Italy

    Ph.D. with honors
    University of Trento
    Information and Communication Technology
    • Advisor: Roberto Sebastiani
    • Thesis: Efficient and Effective Model Enumeration in SAT and SMT: Investigating Novel Procedures and Applications
  • 2018 - 2020

    Trento, Italy

    Master's degree
    University of Trento
    Computer Science
  • 2015 - 2018

    Trento, Italy

    Bachelor's degree
    University of Trento
    Computer Science

Awards

  • 2026
    Runner-up, Fahiem Bacchus PhD Award in Satisfiability
    SAT Association

    Recognized as a runner-up for my Ph.D. thesis. Award information.

  • 2025
    First Place, Poster Competition
    VIII Italian Research Day in the World, Houston

    Winning poster presented as a postdoctoral researcher at Rice University.

International Recognition

  • Feb. 2026 Invited participant at NII Shonan Meeting No. 238, Model Counting: From Theory to Practice

Services

Journal reviewer: Journal of Automated Reasoning (Springer Nature); Integration (Elsevier)
Conference reviewer: International Conference on Theory and Applications of Satisfiability Testing (SAT 2023 and SAT 2024)

Organization

Tutorial: Solving Real-World Problems with Logic: A Hands-On Guide to Satisfiability Modulo Theories and Optimization Modulo Theories — ECAI 2025 (webpage here)

Invited Talks

  • Feb. 2024 Effective Prime Factorization via Quantum Annealing by Modular Locally-Structured Embedding — invited talk at D-Wave

Teaching

  • Fall 2025 Guest Lecturer, COMP 409/509: Logic in Computer Science and Artificial Intelligence, Rice University — taught four class sessions as a substitute for Moshe Y. Vardi
  • 2020–2025 Teaching Assistant, Formal Methods / Automated Reasoning, University of Trento
  • 2018–2022 Mathematics Tutor, University of Trento — with Anneliese Defranceschi

Supervision

Emanuele Civini: MSc thesis: Implementing and Evaluating d-DNNFs Modulo Theories
Massimo Michelutti: MSc thesis: Implementing and Evaluating Boolean Decision Diagrams Modulo Theories
Thomas Dallavia: MSc thesis: Solving OMT(NRA) and OMT(NTA) by Combining Logic-to-Optimization and Nonlinear Constrained Optimization Techniques
Gabriele Masina: MSc thesis: Extending Weighted Model Integration with Structure Awareness and Multiple Integration Approaches

Skills

Research areas: Automated Reasoning, Formal Verification, SAT, SMT, AllSAT, AllSMT, Model Counting, Model Enumeration
Applications: Knowledge Compilation, Weighted Model Integration, Probabilistic Inference, Quantum Annealing

Languages

Italian : Native or bilingual proficiency
English : Professional working proficiency