Formalizing the omega test to check systems of inequalities accurately
Formalizing the Omega Test in Dafny
Logic in Computer ScienceProgramming LanguagesSymbolic Computation
Summary
Some computer problems involve figuring out if sets of inequalities can all be true at the same time. The authors describe how they wrote and verified a computer program in Dafny that carefully implements the omega test algorithm to do this checking precisely. They also explain what they learned about the algorithm by formalizing it, making the process more reliable and understandable.
What this means in practice
- •For software verification teams: Use the formalized omega test to verify correctness of constraint-solving code in critical software components.
- •For compiler designers: Incorporate rigorously verified integer constraint solvers to improve precision in compiler optimizations that rely on inequality checks.
Authors
Ariadna Brănici-Faraon, Ştefan Ciobâcă, Diana-Elena Gratie
Abstract
We present a formalization in Dafny of the Omega Test, an algorithm used to decide the satisfiability of a system of inequalities. The implementation defines executable representations for rational numbers, linear expressions, inequalities, equalities, divisibility constraints, and systems of constraints, together with their semantic interpretation through valuations. We fully specify and verify the implementation in Dafny. We describe the lessons learned and how the formalization process led to new insights into the algorithm.