Related papers: Practical Deductive Verification of OCaml Programs…
OCaml is particularly well-fitted for formal verification. On one hand, it is a multi-paradigm language with a well-defined semantics, allowing one to write clean, concise, type-safe, and efficient code. On the other hand, it is a language…
We present our work on the collaborative use of dynamic and static analysis tools for the verification of software written in the OCaml language. We build upon Gospel, a specification language for OCaml that can be used both in dynamic and…
Functional programming offers the perfect ground for building correct-by-construction software. Languages of such paradigm normally feature state-of-the-art type systems, good abstraction mechanisms, and well-defined execution models. We…
Albeit being a central notion of every programming language, formally and modularly reasoning about iteration proves itself to be a non-trivial feat, specially in the context of higher-order iteration. In this paper, we present a generic…
In this report, we present the preliminary work developed for our research project for the APDC (\'Area Pr\'atica de Desenvolvimento Curricular) course. The main goal of this project is to develop a framework, on top of the Why3 tool, for…
Algebraic effects and handlers are a powerful abstraction to build non-local control-flow mechanisms such as resumable exceptions, lightweight threads, co-routines, generators, and asynchronous I/O. All of such features have very evolved…
This paper presents a translation from Gospel-annotated OCaml programs into Viper, an intermediate verification language featuring Separation Logic. The practical goal is to extend Cameleer with a new back-end to prove heap-dependent OCaml…
Motivated by experience in programming and in the teaching of programming, we make another assault on the longstanding problem of debugging. Having explored why debuggers are not used as widely as one might expect, especially in functional…
We present a library for generic programming in OCaml, adapting some techniques borrowed from other functional languages. The library makes use of three recent additions to OCaml: generalised abstract datatypes are essential to reflect…
We make another assault on the longstanding problem of debugging. After exploring why debuggers are not used as widely as one might expect, especially in functional programming environments, we define the characteristics of a debugger which…
In this position paper, we present a prototype of a visualizer for functional programs. Such programs, whose evaluation model is the reduction of an expression to a value through repeated application of rewriting rules, and which tend to…
We study the problem of completely automatically verifying uninterpreted programs---programs that work over arbitrary data models that provide an interpretation for the constants, functions and relations the program uses. The verification…
We present a novel and well automatable approach to formal verification of programs with underspecified semantics, i.e., a language semantics that leaves open the order of certain evaluations. First, we reduce this problem to…
We show that verification of object-oriented programs by means of the assertional method can be achieved in a simple way by exploiting a syntax-directed transformation from object-oriented programs to recursive programs. This transformation…
Even competent programmers make mistakes. Automatic verification can detect errors, but leaves the frustrating task of finding the erroneous line of code to the user. This paper presents an automatic approach for identifying potential error…
Deductive verification has become a mature paradigm for the verification of industrial software. Applying deductive verification, however, requires that every function in the code base is annotated with a function contract specifying its…
Recent work has shown that Large Language Models (LLMs) are not only a suitable tool for code generation but also capable of generating annotation-based code specifications. Scaling these methodologies may allow us to deduce provable…
We want to verify the correctness of optimization phases in the GraalVM compiler, which consist of many thousands of lines of complex Java code performing sophisticated graph transformations. We have built high-level models of the data…
We define an extension of lambda-calculus with dependents types that enables us to encode transparent and opaque probabilistic programs and prove a strong normalisation result for it by a reducibility technique. While transparent…
We propose an operationally-based deductive proof method for program equivalence. It is based on encoding the language semantics as logically constrained term rewriting systems (LCTRSs) and the two programs as terms. The main feature of our…