Abstract
We study principles and models for reasoning inductively about properties of distributed systems, based on programmed atomic handlers equipped with contracts. We present the Why3-do library, leveraging a state of the art software verifier for reasoning about distributed systems based on our models. A number of examples involving invariants containing existential and nested quantifiers (including Dijsktra’s self-stabilizing systems) illustrate how the library promotes contract-based modular development, abstraction barriers, and automated proofs.

Abstract
The present Special Issue of the Journal of Logical and Algebraic Methods in Programming was planned as a tribute to Jose Manuel Esgalhado Valenca on the occasion of his Jubilation. A tribute to a professor, in the deepest sense of the word, a colleague and a friend, but above all to a long and inspiring academic journey that has so profoundly shaped the development of Informatics as a scientific area in Portugal. A scientific area that, as he taught us, needs to be understood broadly: not only as an independent research domain, but also as an educational pillar, a strategy for social and economic development, a foundation for a multifaceted professional career. This preface introduces some steps of such a journey. The Special Issue features a selection of scientific papers written by his collaborators, colleagues and friends, covering the different areas Jose Valenca helped to launch and consolidate in Portugal, namely computational logic, verification and mechanized reasoning, and information security. (c) 2022 Published by Elsevier Inc.

Abstract
Deductive verification has gained paramount attention from both academia and industry. Although intensive research in this direction covers almost all mainstream languages, the research community has paid little attention to the verification of database applications. This paper proposes a comprehensive set of Verification Conditions (VCs) generation techniques from database programs, adapting Symbolic Execution, Conditional Normal Form, and Weakest Precondition. The validity checking of the generated VCs for a database program determines its correctness w.r.t. the annotated database properties. The developed prototype DBverify based on our theoretical foundation allows us to instantiate VC generation from PL/SQL codes, yielding to detailed performance analysis of the three approaches under different circumstances. With respect to the literature, the proposed approach shows its competence to support crucial SQL features (aggregate functions, nested queries, NULL values, and set operations) and the embedding of SQL codes within a host imperative language. For the chosen set of benchmark PL/SQL codes annotated with relevant properties of interest, our experiment shows that only 38% of procedures are correct, while 62% violate either all or part of the annotated properties. The primary cause for the latter case is mostly due to the acceptance of runtime inputs in SQL statements without proper checking.

Abstract

Abstract
This paper introduces a synthesis procedure for the satisfiability problem of RMTL-integral formulas as SAT solving modulo theories. RMTL-integral is a real-time version of metric temporal logic (MTL) extended by a duration quantifier allowing to measure time durations. For any given formula, a SAT instance modulo the theory of arrays, uninterpreted functions with equality and non-linear real-arithmetic is synthesized and may then be further investigated using appropriate SMT solvers. We show the benefits of using RMTL-integral with the given SMT encoding on a diversified set of examples that include in particular its application in the area of schedulability analysis. Therefore, we introduce a simple language for formalizing schedulability problems and show how to formulate timing constraints as RMTL-integral formulas. Our practical evaluation based on our synthesis and Z3 as back-end SMT solver also shows the feasibility of the overall approach.