Formal Methods

Learning Randomized Reductions and Program Properties
We introduce Bitween, a linear regression-based automated learning algorithm that effectively discovers complex nonlinear randomized (self)-reductions and other arbitrary program invariants (e.g., loop invariants and post conditions) in mixed integer and floating-point programs.
Ferhat Erata, Orr Paradise, Timos Antonopoulos, ThanhVu Nguyen, Shafi Goldwasser, Ruzica Piskac
Cite Project Tool Website Preprint
Learning Randomized Reductions and Program Properties
We introduce Bitween, a linear regression-based automated learning algorithm that effectively discovers complex nonlinear randomized (self)-reductions and other arbitrary program invariants (e.g., loop invariants and post conditions) in mixed integer and floating-point programs.
Ferhat Erata, Orr Paradise, Timos Antonopoulos, ThanhVu Nguyen, Shafi Goldwasser, Ruzica Piskac
Tool Website Preprint
Learning Randomized Reductions and Program Properties
Survey of approaches and techniques for security verification of computer systems
This article surveys the landscape of security verification approaches and techniques for computer systems at various levels: from a …
Ferhat Erata, Shuwen Deng, Faisal Zaghloul, Wenjie Xiong, Onur Demir, Jakub Szefer
PDF Cite DOI URL