Formal Verification and Correctness

URI permanente para esta colección:

https://hdl.handle.net/11705/PROLE/2018/FVC
Artículos en la categoría Formal Verification and Correctness publicados en las Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018).
Notificar un error en esta colección

Examinar

Envíos recientes

Mostrando 1 - 3 de 3
  • Miniatura
    Resumen
    Modeling Systems and Proving their Correctness with Event-B and Rodin
    Carro, Manuel. Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018), 2018-09-17.
    Event-B is a formal development method. It can be used to model and verify correctness of sequential, concurrent, and reactive systems. It uses (infinite) discrete transition systems to capture how the model evolves and first-order logic and typed set theory to express the desirable properties of the system. The proofs that these properties hold are performed using sequent calculus. There are deduction rules specific for useful theories. Event-B is however is not restricted to classical set-theoretical notations and the sequent calculus: it includes notations for defining transitions over states of the model which resembles a programming language, and a rich mathematical toolkit (including operations and relations on sets and functions) to build complex models easily.
  • Miniatura
    Resumen
    An Exercise in Proving Red-Black Trees Correct
    Peña Marí, Ricardo. Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018), 2018-09-17.
    Red-black trees are an efficient data structure that constitutes the basis for implementing maps, multimaps, sets and multisets, in the standard libraries of many programming languages. It achieves logarithmic costs for searching, inserting, and deleting keys, but keeping them balanced frequently requires to deal with a high number of cases. However, a variant called "Left-Leaning", due to Robert Sedgewick, reduces the number of cases to a few ones. We present here a functional version of these red-black trees and prove them correct with respect to a model-based specification, being the model of a red-black tree a set of elements. We have used the Dafny verification platform, which provides the programming language, the assertion language, and the verifier. The latter is an up-to-date SMT solver (Satisfiability Modulo Theories), which can deal with a rather large decidable fragment of the first-order logic.
  • Miniatura
    Artículo
    A Correct Compiler from Mini-ML to a Big-Step Machine Verified Using Natural Semantics in Coq
    Zúñiga, Ángel; Bel-Enguix, Gemma. Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018), 2018-09-17.
    This paper presents a correct compiler of a small functional language, Mini-ML, formalized in Coq. The literature of functional compiler verification in proof assistants usually reports the use of ad hoc formalizations. This work emphasized the use of natural semantics as uniform and unifying framework for this task. As a result of following this approach, a new big-step semantics machine with call by value is introduced, inspired by the SECD of Landin and the MSECD of Leroy. Since this machine uses de Bruijn indices, as first step is giving a (correct verified) translation from named Mini-ML to de Bruijn notation Mini-ML in the natural semantics setting. To the best of the author's knowledge, this is the first mechanization of a correct compiler of a functional language, using natural semantics as verifying framework in a proof assistant, such as, a working compiler capable to be used in real life can be obtained from it.