2 papers
cs.LO2026
The Formalization of two Computational Models in Dafny
Ştefan Ciobâc\b{a}, Diana-Elena Gratie, Dragoş-Irinel Rotariu
We describe the formalization in Dafny of two computational models, Turing Machines and the Lambda Calculus. We present several application of the formalizations: machine proofs of…
cs.LO2026
Formalizing the Omega Test in Dafny
Ariadna Brănici-Faraon, Ştefan Ciobâcă, Diana-Elena Gratie
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 representat…