7 citations · 21 across the 10 of their papers we have counts for
10 papers
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)
Burak Ekici, Arjun Viswanathan, Yoni Zohar +2
This work is a part of an ongoing effort to prove the correctness of invertibility conditions for the theory of fixed-width bit-vectors, which are used to solve quantified bit-vect…
Concrete Semantics with Coq and CoqHammer
Łukasz Czajka, Burak Ekici, Cezary Kaliszyk
The "Concrete Semantics" book gives an introduction to imperative programming languages accompanied by an Isabelle/HOL formalization. In this paper we discuss a re-formalization of…
Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)
Burak Ekici, Guy Katz, Chantal Keller +3
This extended abstract reports on current progress of SMTCoq, a communication tool between the Coq proof assistant and external SAT and SMT solvers. Based on a checker for generic…
IMP with exceptions over decorated logic
Burak Ekici
In this paper, we facilitate the reasoning about impure programming languages, by annotating terms with `decorations' that describe what computational (side) effect evaluation of a…
Hilbert-Post completeness for the state and the exception effects
Jean-Guillaume Dumas, Dominique Duval, Burak Ekici +2
In this paper, we present a novel framework for studying the syntactic completeness of computational effects and we apply it to the exception effect. When applied to the states eff…
Procedural and Non-Procedural Implementation of Search Strategies in Control Network Programming
Kostadin Kratchanov, Emilia Golemanova, Tzanko Golemanov +2
This report presents the general picture of how Control Network Programming can be effectively used for implementing various search strategies, both blind and informed. An interest…
Program certification with computational effects
Jean-Guillaume Dumas, Dominique Duval, Burak Ekici +1
Dynamic evaluation is a paradigm in computer algebra which was introduced for computing with algebraic numbers. In linear algebra, for instance, dynamic evaluation can be used to a…
Certification of programs with computational effects
Burak Ekici
In purely functional programming languages imperative features, more generally computational effects are prohibited. However, non-functional lan- guages do involve effects. The the…
Formal verification in Coq of program properties involving the global state effect
Jean-Guillaume Dumas, Dominique Duval, Burak Ekici +1
The syntax of an imperative language does not mention explicitly the state, while its denotational semantics has to mention it. In this paper we present a framework for the verific…
Certified proofs in programs involving exceptions
Jean-Guillaume Dumas, Dominique Duval, Burak Ekici +1
Exception handling is provided by most modern programming languages. It allows to deal with anomalous or exceptional events which require special processing. In computer algebra, e…