MCBAT: a practical tool for model counting constraints on bounded integer arrays. - Abtin Molavi; Mara Downing; Tommy Schneider; Lucas Bang (ESEC/SIGSOFT FSE, 2020)

MCBAT: Model Counting for Constraints over Bounded Integer Arrays. - Abtin Molavi; Tommy Schneider; Mara Downing; Lucas Bang (VSTTE, 2020)

Symbolic Execution + Model Counting + Entropy Maximization = Automatic Search Synthesis. - Mara Downing; Abtin Molavi; Lucas Bang (GandALF, 2020)

Hyperparameter Choice as Search Bias in AlphaZero. - Eric M. Weiner; George D. Montañez; Aaron Trujillo; Abtin Molavi (SMC, 2021)

Qubit Mapping and Routing via MaxSAT. - Abtin Molavi; Amanda Xu; Martin Diges; Lauren Pick; Swamit S. Tannu; Aws Albarghouthi (MICRO, 2022)

Compilation for Surface Code Quantum Computers. - Abtin Molavi; Amanda Xu; Swamit Tannu; Aws Albarghouthi (CoRR, 2023)

Synthesizing Quantum-Circuit Optimizers. - Amanda Xu; Abtin Molavi; Lauren Pick; Swamit Tannu; Aws Albarghouthi (Proc. ACM Program. Lang., 2023)

Optimizing Quantum Circuits, Fast and Slow. - Amanda Xu; Abtin Molavi; Swamit Tannu; Aws Albarghouthi (ASPLOS (1), 2025)

Dependency-Aware Compilation for Surface Code Quantum Architectures. - Abtin Molavi; Amanda Xu; Swamit Tannu; Aws Albarghouthi (Proc. ACM Program. Lang., 2025)

Generating Compilers for Qubit Mapping and Routing. - Abtin Molavi; Amanda Xu; Ethan Cecchetti; Swamit Tannu; Aws Albarghouthi (CoRR, 2025)