Gianluca Redondi

Postdoc

Gianluca Redondi
E-mail
Google ScholarCitations
DBLPProfile
LinkedInProfile

Biography

I am a postdoctoral researcher in the Formal Methods unit at FBK, led by Stefano Tonetta. I received my Ph.D. in Computer Science from the University of Trento in 2024, with a thesis on SMT-based verification of parameterized systems, supervised by Alessandro Cimatti and Alberto Griggio. During my Ph.D. I visited the University of Texas at Austin, working with Kenneth L. McMillan. Before that, I received an M.Sc. in Mathematics from the University of Milan, with a thesis supervised by Silvio Ghilardi.

My research focuses on SMT-based model checking of infinite-state and parameterized systems, in particular the inference of quantified invariants. Since 2023 I have been working on the formal verification of railway control systems in the ACC projects.

Software

  • Lambda: model checker for parameterized systems and systems with quantifiers (developer and maintainer)
  • pySMT (contributor)
  • IC3IA (contributor)

Recent Talks

  • Verification of Configurable SRA Systems, IJCAR 2026 (slides)
  • Formal Analysis of a Railway Signaling Block Designed in AIDA, RSSRail 2025 (slides)
  • Automated Parameterized Verification of a Railway Protection System with Dafny, CAV 2025 (slides)
  • SMT-based Verification of Parameterized Systems, Ph.D. defense, University of Trento, 2024 (slides)

Publications

  1. Cimatti Alessandro; Griggio Alberto; Lidström Christian; Redondi Gianluca; Trenti Dylan, Verification of Configurable SRA Systems
  2. Cavada Roberto; Cimatti Alessandro; Griggio Alberto; Lidström Christian; Redondi Gianluca; Scaglione Giuseppe; Tessi Matteo; Trenti Dylan, Automated Parameterized Verification of a Railway Protection System with Dafny
  3. Cavada Roberto; Cimatti Alessandro; Griggio Alberto; Lidström Christian; Redondi Gianluca; Tessi Matteo; Trenti Dylan, Formal Analysis of a Railway Signaling Block Designed in AIDA
  4. Redondi Gianluca; Cimatti Alessandro; Griggio Alberto; Mcmillan Kenneth, Invariant Checking for SMT-based Systems with Quantifiers
  5. Cimatti Alessandro; Griggio Alberto; Redondi Gianluca, Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking
  6. Redondi Gianluca; Cimatti Alessandro; Griggio Alberto, Towards Verification Modulo Theories of asynchronous systems via abstraction refinement
  7. Cimatti Alessandro; Griggio Alberto; Redondi Gianluca, Verification of SMT Systems with Quantifiers
  8. Cimatti Alessandro; Griggio Alberto; Redondi Gianluca, Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning

Recent PostsGianluca Redondi

  • No articles found.