CONFEST 2026

Q+F

Exact Evaluation of Probabilistic Programs with Cylindrical Algebraic Decomposition

Mohamed Hamza Bandukara, Fredrik Dahlqvist, Niki Omidvari

in Room Bin session Q+F Session 5 - Probabilistic and Temporal Logic Semantics (on,  Thu, 13:30, 2 talks over 60 min)

We present a method for computing the exact output distribution of small programs with random inputs. Specifically, we are interested in inline programs manipulating sensor data such as e.g. GPS or inertial measurement sensors whose inputs have a known or well- modelled distribution. These programs typically only include relatively few variables, arithmetic operations, square roots and if-else statements. This small syntax allows us to recast the problem of computing the ex- act output distribution as a cylindrical algebraic decomposition problem followed by symbolic integration. We present this method in detail and show with a prototype that it can successfully be applied to benchmarks from the literature on floating-point arithmetic and small programs from open-source sensor libraries.


Other talks in Q+F Session 5 - Probabilistic and Temporal Logic Semantics:

 Program   Q+F Program