Búsqueda avanzada

El autor Paqui Lucio ha publicado 8 artículo(s):

1 - An Assertional Proof of the Stability and Correctness of Natural Mergesort

Natural Mergesort [9] is a sorting algorithm for linear data structures (arrays and lists) that has been widely studied mainly due to its good properties. It has Nlog(N) worst-case complexity and, even in the case of arrays, is slightly easier to code than heapsort. Further, it performs very well on input data that is already mostly sorted. Another good property is stability. A sorting algorithm is stable if it maintains the relative order of records with equal keys. The most obvious application of a stable algorithm is sorting using different (primary, secondary, etc.) keys. Stability is, as we show in lemma EqMultisets, stronger than the property of preserving the multiset of elements (from the input list to the sorted output list). Hence, stability, along with sortedness, implies the correctness of sorting algorithms (including the permutation property). Recently, Sternagel [13] has published an Isabelle/HOL proof of the correctness and stability of natural mergesort as a proof pearl. Sternagel [13], firstly, specifies the algorithm as a functional program and, then, formalizes and proves the desired properties using the proof-assistant Isabelle/HOL. The proof is non-assertional and uses higher-order constructions. Indeed, it is strongly based on two skillful ad-hoc induction schemes. The first one for handling the mutually recursive functions involved in the splitting of the input into ascending sequences. The second induction scheme is related to the merging of the ascending lists. Correctness and stability are deduced from auxiliary lemmas which are proved by means of these induction schemes and with the help of a subtle generalization of the predicate sorted. The definition of that generalization and the induction schemes require the power of higher-order logic. In particular, the stability property is formalized in higher-order logic. More recently, de Gouw et al. [7] discussed a semi-automated formal proof of the correctness and stability of two sorting algorithms on arrays: Counting sort and Radix sort. This proof is formalized using the theorem-prover KeY [2]. The implementation code is written in Java. The specification is written (using the Java Modeling Language, JML) in an extension of first-order logic with permutation predicates, which have recently been added [1] to the KeY system. There are many other formalizations of the natural mergesort algorithm and also of different sorting algorithms (e.g. insertion sort, quicksort, heapsort, radix sort, etc.) in various systems, such as Coq [3], Isabelle/HOL [12], Why3 [6], ACL2 [8], KeY [2], etc. However, to the best of our knowledge, stability is only considered in [13], [7], and in our assertional proof. In this paper, we present an implementation of natural mergesort over an algebraic data type of lists. The code is enriched with its contract-based specification and a proof of its correctness and its stability. Our proof is assertional, i.e. it uses assert statements, inserted in the code, to enable the (fully) automatic verification. The assertions are first-order formulas that explain how and why the program works. The proof is supported by a few definitions that are easy to understand, and a few lemmas that isolate useful properties. Moreover, only non-trivial lemmas have detailed proofs and these are short and easy to read and to understand. Hence, in our opinion, the presented proof is quite clear and elegant. The program-proof is implemented in the state-of-the-art verifier Dafny [10]. The Dafny programming language supports a mixture of imperative, object-oriented programming and functional programming. In this paper, we use mostly functions, methods, and algebraic datatypes. The Dafny specification language includes the usual assertional language for contracts of pre/post conditions, invariants, decreasing expressions for termination proofs, etc. Since Dafny is designed with the main purpose of facilitating the construction of correct code, Dafny notation is compact and easy to understand. For the sake of readability and conciseness, the Dafny proof language includes constructs for structuring proofs such as lemmas and calculational proofs [11]. Dafny automatically generates executable .NET code for verified programs. The presented proof is made on the basis of some lemmas that ensure natural properties. Most of the proofs are inductive and use calculations [11] when appropriate. We believe that our program-proof is a simple and intuitive example of how a practical verification tool can be used by software developers with a minimum of familiarity with contract-based specifications and first-order assertions. We aim to contribute to the spread of the educational use of automatic tools in the development of formally verified software. We are convinced that this kind of example is useful for the introduction of formal software development methods and tools in software engineering courses. To sum up, we present a mechanically verified implementation of the sorting algorithm Natural Mergesort that consists of a few methods specified by their contracts of pre/post conditions. Methods are annotated with assertions that allow the automatic verification of the contract satisfaction. Along the paper we provide and explain the complete text of the program-proof.

Autores: K. Rustan M. Leino / Paqui Lucio / 
Palabras Clave:

2 - Towards the Automatic Verification of QCSP tractability results (Trabajo en progreso)

We deal with the quantied constraint satisfaction problem (QCSP) which consists in deciding, given an structure and a first-order sentence built from atoms, with conjunction and quantication, whether or not the sentence is true on the structure. We study a known proof system which has been used to derive QCSP tractability results. Our contribution is to formalize this proof system into an automatically veried theory, so that it can be used (in a near future) as a basis for automatically verify tractability results.

Autores: Alex Abuin / Hubie Chen / Montserrat Hermo / Paqui Lucio / 
Palabras Clave: Automatic verification - Dafny - inductive predicate - proof system - tractability results

3 - Context-based Model Checking using SMT-solvers (Trabajo en progreso)

In this paper we propose a new idea for the implementation of symbolic model checking. Our pro- posal takes advantage of two technologies. First, SMT-solvers as efficient auxiliary tools to perform a large proportion of the computational task. Second, the context-based tableau that is especially well suited for providing certificates of proved properties, as well as counterexamples of disproved properties. We mainly introduce the algorithm to be implemented, along with illustrative examples.

Autores: Alex Abuin / Unai Díaz de Cerio / Montserrat Hermo / Paqui Lucio / 
Palabras Clave: Model checking - SAT - SMT - Solvers - Tableux

4 -

6 - One-pass Context-based Tableaux Systems for CTL and ECTL

When building tableau for temporal logic formulae, applying a two-pass con- struction, we first check the validity of the given tableaux input by creating a tableau graph, and then, in the second ‘pass’, we check if all the eventualities are satisfied. In one-pass tableaux checking the validity of the input does not require these auxiliary constructions. This paper continues the development of one-pass tableau method for temporal logics introducing tree-style one-pass tableau systems for Computation Tree Logic (CTL) and shows how this can be extended to capture Extended CTL (ECTL). A distinctive feature here is the utilisation, for the core tableau construction, of the concept of a context of an eventuality which forces its earliest fulfilment. Relevant algorithms for obtain- ing a systematic tableau for these branching-time logics are also defined. We prove the soundness and completeness of the method. With these developments of a tree-shaped one-pass tableau for CTL and ECTL, we have formalisms which are well suited for the automation and are amenable for the implementation, and for the formulation of dual sequent calculi. This brings us one step closer to the application of one-pass context-based tableaux in certified model checking for a variety of CTL-type branching-time logics.

Autores: Alex Abuin / Alexander Bolotov / Montserrat Hermo / Paqui Lucio / 
Palabras Clave: branching-time - expressiveness - fairness - Temporal Logic

7 - Using Model Checking in Requirement-based Test Generation for Reactive Systems

In this article we propose an automatic test generation technique for evaluating the implementation of a reactive system with respect to the set of requirements from which it has been developed. We consider reactive systems that interact with its environment via variables whose values (at each instant) depends on events or sensors. Our test cases are graphs that represent a collection of executions (or traces) of the system that captures all possible behaviours of the environment. Our proposal is a technique to automatically construct these graphs exploding the ability of model checkers to generate counter-examples for temporal properties that are not satisfied by a system model. Further work includes to implement a prototype for experimenting the technique on a test suite of industrial requirements, and also to design and implement some techniques to gain scalability.

Autores: Montserrat Hermo / Paqui Lucio / Josu Oca / 
Palabras Clave: Model checking - Reactive Systems - Test Generation

8 - Verified Model Checking for Conjunctive Positive Logic

La referencia completa es:Abuin, A., Díaz de Cerio, U., Hermo, M. and Lucio, P., Verified Model Checking for Conjunctive Positive Logic. SN COMPUTER SCIENCE, VOL 2, Springer 2021.

Autores: Alex Abuin / Unai Díaz de Cerio / Montserrat Hermo / Paqui Lucio / 
Palabras Clave: Conjunctive positive logic - Dafny - Model checking - proof system - Quantified constraint satisfaction problem - Verification