Related papers: A Higher-Order Abstract Syntax Approach to the Ver…
We present a generic framework that facilitates object level reasoning with logics that are encoded within the Higher Order Logic theorem proving environment of HOL Light. This involves proving statements in any logic using intuitive…
Verification of functional correctness of control programs is an essential task for the development of space electronics; it is difficult and time-consuming and typically outweighs design and programming tasks in terms of development hours.…
Modern processors deploy a variety of weak memory models, which for efficiency reasons may (appear to) execute instructions in an order different to that specified by the program text. The consequences of instruction reordering can be…
We consider the problem of synthesizing programs with numerical constants that optimize a quantitative objective, such as accuracy, over a set of input-output examples. We propose a general framework for optimal synthesis of such programs…
Developing suitable formal semantics can be of great help in the understanding, design and implementation of a programming language, and act as a guide for software development tools like analyzers or partial evaluators. In this sense, full…
Interpretation methods and their restrictions to polynomials have been deeply used to control the termination and complexity of first-order term rewrite systems. This paper extends interpretation methods to a pure higher order functional…
Large language models (LLMs) have demonstrated strong reasoning and tool-use capabilities, yet they often fail in real-world tool-interactions due to incorrect parameterization, poor tool selection, or misinterpretation of user intent.…
Many security- and performance-critical domains, such as cryptography, rely on low-level verification to minimize the trusted computing surface and allow code to be written directly in assembly. However, verifying assembly code against a…
Many practical engineering systems and their components have multiple performance levels and failure modes. If these systems form a monotonically increasing structure function (system model) with respect to the performance of their…
This tool paper presents Caos: a methodology and a programming framework for computer-aided design of structural operational semantics for formal models. This framework includes a set of Scala libraries and a workflow to produce visual and…
Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which has…
Constraint Handling Rules (CHR) is a rule-based programming language which is typically embedded into a general-purpose language. There exists a plethora of implementations of CHR for numerous host languages. However, the existing…
Verification proofs encode complete program behavior, yet we discard them after checking correctness. We present compiling by proving, a paradigm that transforms these proofs into optimized execution rules. By constructing All-Path…
Language models (LMs) are often expected to generate strings in some formal language; for example, structured data, API calls, or code snippets. Although LMs can be tuned to improve their adherence to formal syntax, this does not guarantee…
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…
This paper presents an example of formal reasoning about the semantics of a Prolog program of practical importance (the SAT solver of Howe and King). The program is treated as a definite clause logic program with added control. The logic…
This paper proposes {\pi}, a formal semantic framework for compiler construction together with program validation. {\pi} is comprised by {\pi} Lib, a set of programming languages constructs inspired by Peter Mosses' Component-Based…
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…
The C programming language and its cousins such as C++ stipulate the static storage of sets of structured data: Developers have to commit to one, invariant data model -- typically a structure-of-arrays (SoA) or an array-of-structs (AoS) --…
The paper presents a comprehensive analysis of the European AI Act in terms of its logical modalities, with the aim of preparing its formal representation, for example, within the logic-pluralistic Knowledge Engineering Framework and…