Showing 1–10 of 10 results for author: Ekici, B

Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)

Authors: Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark Barrett, Cesare Tinelli

Abstract: 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-vector formulas in the Satisfiability Modulo Theories (SMT) solver CVC4. While many of these were proved in a completely automatic fashion for any bit-width, some were only proved for bit-widths up to 65, even though they ar… ▽ More 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-vector formulas in the Satisfiability Modulo Theories (SMT) solver CVC4. While many of these were proved in a completely automatic fashion for any bit-width, some were only proved for bit-widths up to 65, even though they are being used to solve formulas over arbitrary bit-widths. In this paper we describe our initial efforts in proving a subset of these invertibility conditions in the Coq proof assistant. We describe the Coq library that we use, as well as the extensions that we introduced to it. △ Less

Submitted 26 August, 2019; originally announced August 2019.

Comments: In Proceedings PxTP 2019, arXiv:1908.08639. Presented as an extended abstract

Journal ref: EPTCS 301, 2019, pp. 18-26

Concrete Semantics with Coq and CoqHammer

Authors: Łukasz Czajka, Burak Ekici, Cezary Kaliszyk

Abstract: 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 the book using the Coq proof assistant. In order to achieve a similar brevity of the formal text we extensively use CoqHammer, as well as Coq Ltac-level automation. We compare the formalization efficiency, compactness,… ▽ More 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 the book using the Coq proof assistant. In order to achieve a similar brevity of the formal text we extensively use CoqHammer, as well as Coq Ltac-level automation. We compare the formalization efficiency, compactness, and the readability of the proof scripts originating from a Coq re-formalization of two chapters from the book. △ Less

Submitted 20 August, 2018; originally announced August 2018.

Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)

Authors: Burak Ekici, Guy Katz, Chantal Keller, Alain Mebsout, Andrew J. Reynolds, Cesare Tinelli

Abstract: 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 first-order certificates implemented and proved correct in Coq, SMTCoq offers facilities both to check external SAT and SMT answers and to improve Coq's automation using such solvers, in a safe way. Currently supporting… ▽ More 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 first-order certificates implemented and proved correct in Coq, SMTCoq offers facilities both to check external SAT and SMT answers and to improve Coq's automation using such solvers, in a safe way. Currently supporting the SAT solver zChaff, and the SMT solver veriT for the combination of the theories of congruence closure and linear integer arithmetic, SMTCoq is meant to be extendable with a reasonable amount of effort: we present work in progress to support the SMT solver CVC4 and the theory of bit vectors. △ Less

Submitted 19 June, 2016; originally announced June 2016.

Comments: In Proceedings HaTT 2016, arXiv:1606.05427

Journal ref: EPTCS 210, 2016, pp. 21-29

IMP with exceptions over decorated logic

Authors: Burak Ekici

Abstract: 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 term may involve. In a point-free categorical language,called the `decorated logic', we formalize the mutable state and the exception effects first separately, exploiting anice duality between them, and then combined. T… ▽ More 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 term may involve. In a point-free categorical language,called the `decorated logic', we formalize the mutable state and the exception effects first separately, exploiting anice duality between them, and then combined. The combined decorated logic is used as the target language forthe denotational semantics of the IMP+Exc imperative programming language, and allows us to prove equivalencesbetween programs written in IMP+Exc. The combined logic is encoded in Coq, and this encoding is used to certifysome program equivalence proofs. △ Less

Submitted 16 October, 2018; v1 submitted 18 March, 2015; originally announced March 2015.

Hilbert-Post completeness for the state and the exception effects

Authors: Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Damien Pous, Jean-Claude Reynaud

Abstract: 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 effect, our framework can be seen as a generalization of Pretnar's work on this subject. We first introduce a relative notion of Hilbert-Post completeness, well-suited to the composition of effects. Then we prove that the e… ▽ More 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 effect, our framework can be seen as a generalization of Pretnar's work on this subject. We first introduce a relative notion of Hilbert-Post completeness, well-suited to the composition of effects. Then we prove that the exception effect is relatively Hilbert-Post complete, as well as the "core" language which may be used for implementing it; these proofs have been formalized and checked with the proof assistant Coq. △ Less

Submitted 8 October, 2015; v1 submitted 3 March, 2015; originally announced March 2015.

Comments: Siegfried Rump (Hamburg University of Technology), Chee Yap (Courant Institute, NYU). Sixth International Conference on Mathematical Aspects of Computer and Information Sciences , Nov 2015, Berlin, Germany. 2015, LNCS

Procedural and Non-Procedural Implementation of Search Strategies in Control Network Programming

Authors: Kostadin Kratchanov, Emilia Golemanova, Tzanko Golemanov, Tuncay Ercan, Burak Ekici

Abstract: 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 interesting possibility is non - procedural solutions that can be developed for most local search algorithms. A generic solution is described for procedural implementations. 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 interesting possibility is non - procedural solutions that can be developed for most local search algorithms. A generic solution is described for procedural implementations. △ Less

Submitted 12 December, 2014; originally announced December 2014.

Program certification with computational effects

Authors: Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Damien Pous

Abstract: 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 apply programs which have been written for matrices with coefficients modulo some prime number to matrices with coefficients modulo some composite number. A way to implement dynamic evaluation in modern computing language… ▽ More 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 apply programs which have been written for matrices with coefficients modulo some prime number to matrices with coefficients modulo some composite number. A way to implement dynamic evaluation in modern computing languages is to use the exceptions mechanism provided by the language. In this paper, we pesent a proof system for exceptions which involves both raising and handling, by extending Moggi's approach based on monads. Moreover, the core part of this proof system is dual to a proof system for the state effect in imperative languages, which relies on the categorical notion of comonad. Both proof systems are implemented in the Coq proof assistant, and they are combined in order to deal with both effects at the same time. △ Less

Submitted 26 November, 2014; originally announced November 2014.

Certification of programs with computational effects

Authors: Burak Ekici

Abstract: In purely functional programming languages imperative features, more generally computational effects are prohibited. However, non-functional lan- guages do involve effects. The theory of decorated logic provides a rigorous for- malism (with a refinement in operation signatures) for proving program properties with respect to computational effects. The aim of this thesis is to first develop Coq libr… ▽ More In purely functional programming languages imperative features, more generally computational effects are prohibited. However, non-functional lan- guages do involve effects. The theory of decorated logic provides a rigorous for- malism (with a refinement in operation signatures) for proving program properties with respect to computational effects. The aim of this thesis is to first develop Coq libraries and tools for verifying program properties in decorated settings as- sociated with several effects: states, local state, exceptions, non-termination, etc. Then, these tools will be combined to deal with several effects. △ Less

Submitted 26 November, 2014; originally announced November 2014.

Certified proofs in programs involving exceptions

Authors: Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Jean-Claude Reynaud

Abstract: 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, exception handling is an efficient way to implement the dynamic evaluation paradigm: for instance, in linear algebra, dynamic evaluation can be used for applying programs which have been written for matrices with coeffici… ▽ More 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, exception handling is an efficient way to implement the dynamic evaluation paradigm: for instance, in linear algebra, dynamic evaluation can be used for applying programs which have been written for matrices with coefficients in a field to matrices with coefficients in a ring. Thus, a proof system for computer algebra should include a treatement of exceptions, which must rely on a careful description of a semantics of exceptions. The categorical notion of monad can be used for formalizing the raising of exceptions: this has been proposed by Moggi and implemented in Haskell. In this paper, we provide a proof system for exceptions which involves both raising and handling, by extending Moggi's approach. Moreover, the core part of this proof system is dual to a proof system for side effects in imperative languages, which relies on the categorical notion of comonad. Both proof systems are implemented in the Coq proof assistant. △ Less

Submitted 13 March, 2014; v1 submitted 9 October, 2013; originally announced October 2013.

Formal verification in Coq of program properties involving the global state effect

Authors: Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Damien Pous

Abstract: 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 verification in Coq of properties of programs manipulating the global state effect. These properties are expressed in a proof system which is close to the syntax, as in effect systems, in the sense that the state does not appea… ▽ More 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 verification in Coq of properties of programs manipulating the global state effect. These properties are expressed in a proof system which is close to the syntax, as in effect systems, in the sense that the state does not appear explicitly in the type of expressions which manipulate it. Rather, the state appears via decorations added to terms and to equations. In this system, proofs of programs thus present two aspects: properties can be verified {\em up to effects} or the effects can be taken into account. The design of our Coq library consequently reflects these two aspects: our framework is centered around the construction of two inductive and dependent types, one for terms up to effects and one for the manipulation of decorations. △ Less

Submitted 14 October, 2013; v1 submitted 2 October, 2013; originally announced October 2013.