Yazar "Ekici, Burak" için listeleme
-
Formal Verification of Bit-Vector Invertibility Conditions in Coq
Ekici, Burak; Viswanathan, Arjun; Zohar, Yoni; Tinelli, Cesare; Barrett, Clark Stanford University, (Springer Science and Business Media Deutschland GmbH, 2023)We prove the correctness of invertibility conditions for the theory of fixed-width bit-vectors—used to solve quantified bit-vector formulas in the Satisfiability Modulo Theories (SMT) solver cvc5— in the Coq proof assistant. ... -
A Sound Definitional Interpreter for a Simply Typed Functional Language
Ekici, Burak (MDPI, 2023)In this paper, we develop, in the proof assistant Coq, a definitional interpreter and a type-checker for a simply typed functional language, and formally prove that the mentioned type-checker is sound with respect to the ...
