相关论文: Why Just Boogie? Translating Between Intermediate …
Automated program verifiers are typically implemented using an intermediate verification language (IVL), such as Boogie or Why3. A verifier front-end translates the input program and specification into an IVL program, while the back-end…
A program verifier produces reliable results only if both the logic used to justify the program's correctness is sound, and the implementation of the program verifier is itself correct. Whereas it is common to formally prove soundness of…
Lightweight validation technique, such as those based on random testing, are sometimes practical alternatives to full formal verification -- providing valuable benefits, such as finding bugs, without requiring a disproportionate effort. In…
In theorem prover or SMT solver based verification, the program to be verified is often given in an intermediate verification language such as Boogie, Why, or CHC. This setting raises new challenges. We investigate a preprocessing step…
Static program verifiers such as Spec#, Dafny, jStar, and VeriFast define the state of the art in automated functional verification techniques. The next open challenges are to make verification tools usable even by programmers not fluent in…
This dissertation discusses several problems loosely related, because they all involve a verification condition generator. The Boogie language is introduced; the architecture of a verification-generator is described. Then come more…
The Message Passing Interface specification (MPI) defines a portable message-passing API used to program parallel computers. MPI programs manifest a number of challenges on what concerns correctness: sent and expected values in…
This paper presents a quantitative program verification infrastructure for discrete probabilistic programs. Our infrastructure can be viewed as the probabilistic analogue of Boogie: its central components are an intermediate verification…
Program verifiers are not exempt from the bugs that affect nearly every piece of software. In addition, they often exhibit brittle behavior: their performance changes considerably with details of how the input program is expressed-details…
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…
Program verification tools are often implemented as front-end translations of an input program into an intermediate verification language (IVL) such as Boogie, GIL, Viper, or Why3. The resulting IVL program is then verified using an…
The breakneck evolution of modern programming languages aggravates the development of deductive verification tools, which struggle to timely and fully support all new language features. To address this challenge, we present ByteBack: a…
A program's exceptional behavior can substantially complicate its control flow, and hence accurately reasoning about the program's correctness. On the other hand, formally verifying realistic programs is likely to involve exceptions -- a…
Verifying relations between programs arises as a task in various verification contexts such as optimizing transformations, relating new versions of programs with older versions (regression verification), and noninterference. However,…
This paper presents a framework that integrates Large Language Models (LLMs) into translation validation, targeting LLVM compiler transformations where formal verification tools fall short. Our framework first utilizes existing formal…
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…
Large language models (LLMs) have shown increasing competence in solving mathematical reasoning problems. However, many open-source LLMs still struggle with errors in calculation and semantic understanding during intermediate reasoning…
Large language models (LLMs) have demonstrated remarkable progress in code generation, but many existing benchmarks are approaching saturation and offer little guarantee on the trustworthiness of the generated programs. To improve…
A bug or error is a common problem that any software or computer program may encounter. It can occur from badly writing the program, a typing error or bad memory management. However, errors can become a significant issue if the unsafe…
The exploitation of smart-contract vulnerabilities can have catastrophic consequences such as the loss of millions of pounds worth of crypto assets. Formal verification can be a useful tool in identifying vulnerabilities and proving that…