Home

Denis Bueno

dlbueno@umich.edu
@codebueno

I am a PhD candidate at the University of Michigan studying with Karem Sakallah (also previously with Michael Bailey, now at UIUC). Before coming to 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.

Publications

EUFicient Reachability in Software with Arrays
with Arlen Cox and Karem A. Sakallah. In Formal Methods for Computer-Aided Design (FMCAD), 2020, to appear.
Horn2VMT: Translating Horn Reachability into Transition Systems
with Karem A. Sakallah. In Horn Clauses for Verification and Synthesis, 2020. Available online.
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: 2020-08-20