PROVING PROPERTIES OF DISCRETE-VALUED FUNCTIONS USING DEDUCTIVE PROOF: APPLICATION TO THE SQUARE ROOT

Vassil Todorov (1, 2, 3) , Safouan Taha (1, 4, 2) , Frédéric Boulanger (1, 4, 2) , Armando Hernandez (3)

1 LRI - Laboratoire de Recherche en Informatique
2 Université Paris-Saclay
3 Groupe PSA - Centre Technique de Vélizy [Vélizy-Villacoublay]
4 CentraleSupélec

Domains: Modeling and Simulation; Software Engineering [cs.SE]; Formal Languages and Automata Theory [cs.FL]

Vassil Todorov, Safouan Taha, Frédéric Boulanger, Armando Hernandez. PROVING PROPERTIES OF DISCRETE-VALUED FUNCTIONS USING DEDUCTIVE PROOF: APPLICATION TO THE SQUARE ROOT. System Informatics, 2019, 14, ⟨10.31144/si.2307-6410.2019.n14.p45-54⟩. ⟨hal-02322645⟩