| 2024 | PERCOM | Self-Balancing Semi-Hierarchical Payment Channel Networks for Central Bank Digital Currencies. | Marco Benedetti, Francesco De Sclavis, Marco Favorito, Giuseppe Galano, Sara Giammusso, Antonio Muci, Matteo Nardelli |
| 2018 | SACMAT | Parametric RBAC Maintenance via Max-SAT. | Marco Benedetti, Marco Mori |
| 2008 | CP | Quantified Constraint Optimization. | Marco Benedetti, Arnaud Lallouet, Jrmie Vautard |
| 2008 | SAC | Modeling adversary scheduling with QCSP | Marco Benedetti, Arnaud Lallouet, Jrmie Vautard |
| 2007 | ICCAD | A performance-driven QBF-based iterative logic array representation with applications to verification, debug and test. | Hratch Mangassarian, Andreas G. Veneris, Sean Safarpour, Marco Benedetti, Duncan Exon Smith |
| 2007 | IJCAI | QCSP Made Practical by Virtue of Restricted Quantification. | Marco Benedetti, Arnaud Lallouet, Jrmie Vautard |
| 2006 | AAAI | Abstract Branching for Quantified Formulas. | Marco Benedetti |
| 2005 | CADE | sKizzo: A Suite to Evaluate and Certify QBFs. | Marco Benedetti |
| 2005 | IJCAI | Extracting Certificates from Quantified Boolean Formulas. | Marco Benedetti |
| 2005 | SAT | Quantifier Trees for QBFs. | Marco Benedetti |
| 2004 | LPAR | Evaluating QBFs via Symbolic Skolemization. | Marco Benedetti |
| 2004 | SAT | Incremental Compilation-to-SAT Procedures. | Marco Benedetti, Sara Bernardini |
| 2004 | SAT | Incremental Compilation-to-SAT Procedures. | Marco Benedetti, Sara Bernardini |
| 2003 | TACAS | Bounded Model Checking for Past LTL. | Marco Benedetti, Alessandro Cimatti |
| 2001 | CADE | Conditional Pure Literal Graphs. | Marco Benedetti |