“Integer Reasoning Modulo Different Constants in SMT” by Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor, Alp Bassa, Sorawee Porncharoenwase, Işil Dillig, and Clark Barrett. In Proceedings of the 37^th International Conference on Computer Aided Verification (CAV '25), (Ruzica Piskac and Zvonimir Rakamaric, eds.), July 2025, pp. 339-362. Zagreb, Croatia.
This paper presents a new refutation procedure for multimodular systems of integer constraints that commonly arise when verifying cryptographic protocols. These systems, involving polynomial equalities and disequalities modulo different constants, are challenging for existing solvers due to their inability to exploit multimodular structure. To address this issue, our method partitions constraints by modulus and uses lifting and lowering techniques to share information across subsystems, supported by algebraic tools like weighted Gr bner bases. Our experiments show that the proposed method outperforms existing state-of-the-art solvers in verifying cryptographic implementations related to Montgomery arithmetic and zero-knowledge proofs.
BibTeX entry:
@inproceedings{POP+25,
author = {Elizaveta Pertseva and Alex Ozdemir and Shankara Pailoor and
Alp Bassa and Sorawee Porncharoenwase and I{\c{s}}il Dillig and
Clark Barrett},
editor = {Ruzica Piskac and Zvonimir Rakamari{\'c}},
title = {Integer Reasoning Modulo Different Constants in{\^A}~SMT},
booktitle = {Proceedings of the {\it 37^{th}} International Conference
on Computer Aided Verification (CAV '25)},
series = {Lecture Notes in Computer Science},
volume = {15931},
pages = {339--362},
publisher = {Springer},
month = jul,
year = {2025},
doi = {10.1007/978-3-031-98668-0_17},
note = {Zagreb, Croatia},
url = {https://doi.org/10.1007/978-3-031-98668-0_17}
}
(This webpage was created with bibtex2web.)