Research

Here’s a list of my most relevant publications. If you’d like to read a more complete one and you like little squares, please see my DBLP profile.

Context-Free Temporal Logics

Model checking of context-free specifications on pushdown systems is one of my long-lasting lines of research. I introduced the temporal logic POTL [CAV21, LMCS22], which expresses context-free specifications that are more expressive than those that can be written in, e.g., LTL. POTL can express, for instance, Hoare-style pre/post-conditions, stack inspection, no-throw guarantees, and exception safety [CAV21]. Together with my students, I develop and maintain POMC , a model checker for procedural programs with exceptions against POTL specifications based on an explicit-state [CAV21, TOPLAS23, SEFM21] and an SMT [CAV24] engine. POTL is equivalent to the class of first-order definable Operator Precedence Languages [LMCS22].

In a previous attempt at developing a temporal logic for expressing operator-precedence properties, I introduced OPTL [GandALF18, TCS20]. OPTL is, however, less expressive [LMCS22] and less user-friendly than POTL.

Floating-Point Program Verification

I worked on constraint solving for floating-point arithmetic [Cons22] in collaboration with BUGSENG. The constraint solver, which can handle constraints involving the C/C++ standard math library [TOSEM21], has been integrated within the ECLAIR software verification framework.

Approximate Computing

I took part of the development of TAFFO , a tool that automatically translates floating-point computations in C/C++ programs to fixed-point formats [ESL20, TACO20, DAC21, SfX22], including calls to functions in the standard mathematical library [SusCom21]. TAFFO has been employ to successfully optimize several benchmarks and use cases, including applications based on machine learning [PD20].

Verification of Infrastructure-as-Code

Within the PIACERE Horizon 2020 project I worked, among other things, on a model checker for Infrastructure-as-Code (IaC) [InfoSys24]. [FIST22] contains a survey of existing static analysis techniques for IaC, from detection of code smells to model checking.