Abstract

Abstract
Monitoring a system over time is as important as ever with the increasing use of cloud-native software architectures. This paper expands the set of patterns published in a previous paper (Liveness Endpoint, Readiness Endpoint and Synthetic Testing) with two solutions for supporting teams in diagnosing occurring issues — Deployment Tracking and Exception Tracking. These patterns advise tracking relevant events that occur in the system. The Deployment Tracking pattern provides means to limit the sources of an anomaly, and the Exception Tracking pattern makes a specific class of anomalies visible so that a team can act on them. Both patterns help practitioners identify the root cause of an issue, which is instrumental in fixing it. They can help even less experienced professionals to improve monitoring processes, and reduce the mean time to resolve problems with their application. These patterns draw on documented industry best practices and existing tools. In order to help the reader find other patterns that supplement the ones suggested in this study, relations to already-existing monitoring patterns are also examined.

Abstract
Optical Coherence Tomography (OCT) is the major diagnostic tool for the leading cause of blindness in developed countries: Diabetic Macular Edema (DME). Depending on the type of fluid accumulations, different treatments are needed. In particular, Cystoid Macular Edemas (CMEs) represent the most severe scenario, while Diffuse Retinal Thickening (DRT) is an early indicator of the disease but a challenging scenario to detect. While methodologies exist, their explanatory power is limited to the input sample itself. However, due to the complexity of these accumulations, this may not be enough for a clinician to assess the validity of the classification. Thus, in this work, we propose a novel approach based on multi-prototype networks with vision transformers to obtain an example-based explainable classification. Our proposal achieved robust results in two representative OCT devices, with a mean accuracy of 0.9099 ± 0.0083 and 0.8582 ± 0.0126 for CME and DRT-type fluid accumulations, respectively.

Abstract

Abstract

Abstract
With the incresasing importance of program verification, an issue that has been receiving more attention is the certification of verification tools, addressing the vernacular question: Who verifies the verifier?. In this paper we approach this meta-verification problem by focusing on a fundamental component of program verifiers: the Verification Conditions Generator (VCGen), responsible for producing a set of proof obligations from a program and a specification. The semantic foundations of VCGens lie in program logics, such as Hoare logic, Dynamic logic, or Separation logic, and related predicate transformers. Dynamic logic is the basis of the KeY system, one of the foremost deductive verifiers, whose logic makes use of the notion of update, which is quite intricate to formalize. In this paper we derive systematically, based on a KeY-style dynamic logic, a correct-by-construction VCGen for a toy programming language. Our workflow covers the entire process, from the logic to the VCGen. It is implemented in the Why3 tool, which is itself a program verifier. We prove the soundness and (an appropriate notion of) completeness of the logic, then define a VCGen for our language and establish its soundness. Dynamic logic is one of a variety of research topics that our dear friend and colleague Luis Soares Barbosa has, over the years, initiated and promoted at the University of Minho. It is a pleasure for us to dedicate this work to him on the occasion of his 60th birthday.