Loop Invariants

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