Home

Denis Bueno

dlbueno@umich.edu
@codebueno

I finished my PhD in 2021 at the University of Michigan, studying with Karem Sakallah (also previously with Michael Bailey, now at UIUC). Before Ann Arbor, I received my Bachelor's degree from Georgia Tech and my Master's from Cornell.

I'm interested in formal software verification, static program analysis, and security.

News

Publications

Software Model Checking with Uninterpreted Functions
My dissertation.
@phdthesis{Bueno:Diss2021, author = {Denis Bueno}, title = {Software Model Checking with Uninterpreted Functions}, school = {University of Michigan}, url = {http://hdl.handle.net/2027.42/168092}, year = {2021} }
EUFicient Reachability in Software with Arrays
with Arlen Cox and Karem A. Sakallah. In Formal Methods for Computer-Aided Design (FMCAD), 2020.
@inproceedings{Bueno+:FMCAD2020, author = {Denis Bueno and Arlen Cox and Karem A. Sakallah}, title = {EUFicient Reachability in Software with Arrays}, pages = {57--66}, crossref = {FMCAD:2020} } @proceedings{FMCAD:2020, title = {Formal Methods in Computer Aided Design}, publisher = {{IEEE}}, year = {2020}, url = {https://ieeexplore.ieee.org/xpl/conhome/9283613/proceeding}, isbn = {978-3-85448-042-6} }
Horn2VMT: Translating Horn Reachability into Transition Systems
with Karem A. Sakallah. In Horn Clauses for Verification and Synthesis, 2020. Available online.
@inproceedings{Bueno-Sakallah:HCVS20, author = {Denis Bueno and Karem Sakallah}, title = {{Horn2VMT}: Translating Horn Reachability into Transition Systems}, year = {2020}, booktitle = {Proceedings 8th International Workshop on Verification and Program Transformation and 7th Workshop on Horn Clauses for Verification and Synthesis}, doi = {10.4204/EPTCS.320}, pages = {163--167}}
EUForia: complete software model checking with uninterpreted functions
with Karem A. Sakallah. In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2019.
@inproceedings{Bueno-Sakallah:VMCAI19, author = {Denis Bueno and Karem A. Sakallah}, title = {euforia: Complete Software Model Checking with Uninterpreted Functions}, pages = {363--385}, year = {2019}, crossref = {VMCAI:19} } @proceedings{VMCAI:19, editor = {Constantin Enea and Ruzica Piskac}, title = {Verification, Model Checking, and Abstract Interpretation}, booktitle = {Verification, Model Checking, and Abstract Interpretation}, series = {Lecture Notes in Computer Science}, volume = {11388}, publisher = {Springer}, year = {2019} }
This is a post-peer-review, pre-copyedit version of an article published in Verification, Model Checking, and Abstract Interpretation. The final authenticated version is available online at: http://dx.doi.org/https://dx.doi.org/10.1007/978-3-030-11245-5.
Improving performance of CDCL SAT solvers by automated design of variable selection heuristics
Marketa Illetskova, Alex R. Bertels, Joshua M. Tuggle, Adam Harter, Samuel Richter, Daniel R. Tauritz, Samuel A. Mulder, Denis Bueno, Michelle Leger, and William M. Siever. In SSCI, 2017.
@inproceedings{Illetskova+:SSCI17, author = {Marketa Illetskova and Alex R. Bertels and Joshua M. Tuggle and Adam Harter and Samuel Richter and Daniel R. Tauritz and Samuel A. Mulder and Denis Bueno and Michelle Leger and William M. Siever}, title = {Improving performance of {CDCL} {SAT} solvers by automated design of variable selection heuristics}, pages = {1--8}, year = {2017}, crossref = {SSCI:17} } @proceedings{SSCI:17, title = {Symposium Series on Computational Intelligence}, booktitle = {Symposium Series on Computational Intelligence}, publisher = {{IEEE}}, year = {2017} }
Detecting traditional packers, decisively
with Kevin J. Compton, Karem A. Sakallah, and Michael Bailey. In Research in Attacks, Intrusions, and Defenses (RAID), 2013.
@inproceedings{Bueno+:RAID2013, author = {Denis Bueno and Kevin J. Compton and Karem A. Sakallah and Michael Bailey}, title = {Detecting Traditional Packers, Decisively}, year = {2013}, pages = {184--203}, crossref = {RAID:13}} @proceedings{RAID:13, publisher = {Springer}, series = {Lecture Notes in Computer Science}, booktitle = {Research in Attacks, Intrusions, and Defenses}, title = {Research in Attacks, Intrusions, and Defenses}, volume = {8145}, editor = {Salvatore J. Stolfo and Angelos Stavrou and Charles V. Wright}, year = {2013}}
Last modified: 2021-06-16