Paolo Di Biase

Paolo Di Biase is a PhD student in Computer Science at the Gran Sasso Science Institute (GSSI).

He earned his BSc from the University of Molise (UniMol) in 2023 (110/110) with a thesis on the design and implementation of an application for traceability in the forest wood supply chain, and began an MSc in Software Systems Security the same year, specializing in program analysis and software verification.
In January 2025, he started collaborating with Gennaro Parlato in the Program Analysis in the Clouds Lab (PAC Lab) through a UniMol research scholarship, working on bounded model checking for concurrent programs and the parallelization of SAT solving.
In February 2025, he joined the Erasmus+ Traineeship program and completed a two-month internship at Diffblue in Oxford (UK), under the supervision of Peter Schrammel, studying CBMC, the bounded model checker maintained by Diffblue, and implementing Iekke, a SAT-based verification tool for concurrent programs, as part of the research for his master’s thesis.
He completed his MSc in October 2025 (110/110 cum laude) with a thesis on bounded-round partial order representation for efficient bounded model checking of concurrent programs, and joined GSSI as a PhD student in November 2025.

Research Interests

• SAT/SMT solvers
• Program analysis and software verification
• Model checking: algorithms and tools
• Verification of Concurrent Software

Current Research Projects

• Heuristics for SAT / Decision Procedures for SMT
• Parallel SAT solving
• Iekke: Bounded Model checking of concurrent programs via sequentialization and partial order (SV-COMP 2026 bronze medal, Concurrency)

Publications

• Iekkë: A Bounded-Round Partial-Order Encoding Verification Tool for Concurrent C Programs
  P. Di Biase, B. Fischer, S. La Torre, P. Schrammel, G. Parlato
  SPLASH Companion '26, 2026. [DOI]
• Iekke: A SAT-based Bounded-Round Verifier for Multi-threaded Programs (Competition Contribution)
  P. Di Biase, B. Fischer, S. La Torre, P. Schrammel, G. Parlato
  Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2026), LNCS 16506, Springer, 2026. [DOI]

Software/Tools

• Iekke: BMC tool for concurrent C programs. Built on top of Deagle (front-end) and MiniSAT 2.2.1 (back-end), it simulates sequentialization using partial order constraints, for a fixed number of rounds.

Academic Service

• July 2026 — Master thesis Co-Supervisor, Symbolic POR for Nearly Free: Canonical Encodings for Read-From Classes in BMC (candidate: Andrea Pino di Cristofaro).
• Mar.–May 2026 — Artifact Evaluation Committee, 37th International Conference on Computer Aided Verification (CAV 2026).
• Apr. 2026 — Master thesis Co-Supervisor, Scalable Bounded Model Checking via Parallel SAT and Domain-Aware Heuristics (candidate: Vittorio Perozzi).

Conferences & Seminars

• Apr. 2026 — Presented Iekke: A SAT-based Bounded-Round Verifier for Multi-threaded Programs (Competition Contribution) at TACAS 2026 - Turin (IT).
• Oct. 2025 — SAT solving seminar, University of Molise, for the course on Software Security and Program Analysis (MSc in Software Systems Security).
• Nov. 2024 — SAT solving seminar, University of Molise, for the course on Software Security and Program Analysis (MSc in Software Systems Security).

Awards

• Jun. 2026 — Petrone Award, University of Molise.
• Apr. 2026 — Bronze medal, SV-COMP 2026 (Concurrency category), Sosy-Lab.
• Jan. 2025 — Research Grant in Software Analysis, University of Molise.

Curriculum Vitae

His CV is available here.