David E. Narváez


I am postdoc working under the supervision of Dr. Binoy Ravindran at the intersection of formal verification and binary analysis. I finished my PhD at RIT under the supervision of Edith Hemaspaandra and Stanisław P. Radziszowski on the topic of constraint satisfaction techniques for combinatorial problems (see my AAAI 18 Doctoral Consortium paper). I did my BS in Computer Systems Engineering at UTP (I am, as a matter of fact, from Panama) and my MS in Computer Science at RIT.


My main interests are formal verification and solving combinatorial problems using constraint satisfaction techniques. Within those topic, there are several specific areas I am interested in.

Selected, Refereed Publications

(You can find a more complete list on DBLP.)

[1] Edith Hemaspaandra and David E. Narváez. Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification. In Kevin Buzzard and Temur Kutsia, editors, Intelligent Computer Mathematics, pages 241--255, Cham, September 2022. Springer International Publishing. [ bib | DOI ]
[2] Joshua Brakensiek, Marijn Heule, John Mackey, and David Narváez. The resolution of Keller’s conjecture. Journal of Automated Reasoning, 66(3):277--300, May 2022. [ bib | DOI ]
[3] Ivona Bezáková, Kimberly Fluet, Edith Hemaspaandra, Hannah Miller, and David E. Narváez. Effective succinct feedback for intro CS theory: A JFLAP extension. In Proceedings of the 53rd ACM Technical Symposium on Computer Science Education V. 1, SIGCSE 2022, pages 976--982, New York, NY, USA, February 2022. Association for Computing Machinery. [ bib | DOI ]
[4] Lane A. Hemaspaandra and David E. Narváez. The opacity of backbones. Information and Computation, 281:104772, December 2021. [ bib | DOI ]
[5] Hannah Miller and David E. Narváez. Toward determining NFA equivalence via QBFs (student abstract). Proceedings of the AAAI Conference on Artificial Intelligence, 35(18):15849--15850, May 2021. [ bib | DOI ]
[6] Chula Jayawardene, David E. Narváez, and Stanislaw P. Radziszowski. Star-critical Ramsey numbers for cycles versus K4. Discussiones Mathematicae Graph Theory, 41(2):381--390, May 2021. [ bib | DOI ]
[7] Lane A. Hemaspaandra and David E. Narváez. Existence versus exploitation: the opacity of backdoors and backbones. Progress in Artificial Intelligence, 10(3):297--308, March 2021. [ bib | DOI ]
[8] Ivona Bezáková, Edith Hemaspaandra, Aryeh Lieberman, Hannah Miller, and David E. Narváez. Prototype of an automated feedback tool for intro CS theory. In 51st ACM Technical Symposium on Computer Science Education, SIGCSE ’20, page 1311. ACM, 2020. [ bib | DOI ]
[9] David E. Narváez. A QSAT benchmark based on vertex-Folkman problems. In 34th AAAI Conference on Artificial Intelligence (Student Abstracts), volume 34, pages 13881--13882. AAAI Press, 2020. [ bib | DOI ]
[10] David E. Narváez. Formalizing CNF SAT symmetry breaking in PVS. In Julia M. Badger and Kristin Yvonne Rozier, editors, NASA Formal Methods Symposium, volume 11460 of Lecture Notes in Computer Science, pages 341--354. Springer, 2019. [ bib | DOI ]
[11] Zack Fitzsimmons, Edith Hemaspaandra, Alexander Hoover, and David E. Narváez. Very hard electoral control problems. In 33rd AAAI Conference on Artificial Intelligence, volume 33, pages 1933--1940. AAAI Press, 2019. [ bib | DOI ]
[12] David E. Narváez. Exploring the use of Shatter for AllSAT through Ramsey-type problems. In 32nd AAAI Conference on Artificial Intelligence, pages 8123--8124. AAAI Press, February 2018. [ bib | DOI ]
[13] David E. Narváez. Constraint satisfaction techniques for combinatorial problems. In The Twenty-Third AAAI/SIGAI Doctoral Consortium, pages 8028--8029. AAAI Press, February 2018. [ bib | DOI ]