Research Interests
- Automated Reasoning
- SAT and SAT modulo theories (SMT)
- Formal Methods
- Model Checking
- Neural Networks Verification
Publications
Current Projects
- BTOR2YICES
- Yices2: An SMT solver
Past Projects
- CVC4: An SMT solver
- Kratos: A software analyzer for C programs
- LazyBV2Int: An SMT solver for Bit-Vectors
- Marabou: A neural network verfication tool
- MathSAT5: An SMT solver
- nuXmv: A symbolic model checker
- Pcassco: A parallel SAT solver
- Pono: A symbolic model checker
- prophic3: Counterexample guided prophecy for model checking transition systems with arrays
- Simulink2SMV: A translator for Simulink designs to SMV
- Verilog2SMV: A translator for Verilog programs to SMV
Academic Service
- Co-Chair of FMCAD 2025
- PC Member of ECAI 2025
- PC Member of SPIN 2025
- PC Member of SBMF 2024
- PC Member of SMT 2024
- PC Member of FM 2024
- PC Member of FMCAD 2024
- PC Member of SBMF 2023
- PC Member of SMT 2023
- PC Member of VSTTE 2023
- PC Member of TACAS-AE 2023
- PC Member of FMCAD 2022
- Co-organizer of NFM-AI-SAFETY 2020
- PC Member of NFM 2020
- PC Member of PAAR 2020
- PC Member of SC2 2020
- PC Member of TACAS-AE 2020
Competitions
- Yices2 at the SMT-COMP 2025
- Yices2 at the SMT-COMP 2024
- Yices2 at the SMT-COMP 2023
- CVC4 at the SMT-COMP 2020
- ic3ia at the CHC-COMP 2020
- lazybv2int at the SMT-COMP 2020
- Pono at the Hardware Model Checking Competition 2020
- Prophic3 at the CHC-COMP 2020
- Cosa2 at the Hardware Model Checking Competition 2019
- MathSAT5 at the SMT-COMP 2019
- CLAS at the SAT Competition 2014
- Pcassco at the SAT Competition 2014
- Pcassco at the SAT Competition 2013