State of the art in software verification and witness validation: SV-COMP 2024
D Beyer - International Conference on Tools and Algorithms for …, 2024 - Springer
The 13th edition of the Competition on Software Verification (SV-COMP 2024) was the
largest competition of its kind so far: A total of 76 tools for verification and witness validation …
largest competition of its kind so far: A total of 76 tools for verification and witness validation …
Competition on software verification and witness validation: SV-COMP 2023
D Beyer - International Conference on Tools and Algorithms for …, 2023 - Springer
The 12th edition of the Competition on Software Verification (SV-COMP 2023) is again the
largest overview of tools for software verification, evaluating 52 verification systems from 34 …
largest overview of tools for software verification, evaluating 52 verification systems from 34 …
Progress on software verification: SV-COMP 2022
D Beyer - International Conference on Tools and Algorithms for …, 2022 - Springer
The 11th edition of the Competition on Software Verification (SV-COMP 2022) provides the
largest ever overview of tools for software verification. The competition is an annual …
largest ever overview of tools for software verification. The competition is an annual …
SoK: Computer-aided cryptography
Computer-aided cryptography is an active area of research that develops and applies
formal, machine-checkable approaches to the design, analysis, and implementation of …
formal, machine-checkable approaches to the design, analysis, and implementation of …
Leveraging Rust types for modular specification and verification
Rust's type system ensures memory safety: well-typed Rust programs are guaranteed to not
exhibit problems such as dangling pointers, data races, and unexpected side effects through …
exhibit problems such as dangling pointers, data races, and unexpected side effects through …
Evercrypt: A fast, verified, cross-platform cryptographic provider
J Protzenko, B Parno, A Fromherz… - … IEEE Symposium on …, 2020 - ieeexplore.ieee.org
We present EverCrypt: a comprehensive collection of verified, high-performance
cryptographic functionalities available via a carefully designed API. The API provably …
cryptographic functionalities available via a carefully designed API. The API provably …
Vale: Verifying {High-Performance} Cryptographic Assembly Code
B Bond, C Hawblitzel, M Kapritsos, KRM Leino… - 26th USENIX security …, 2017 - usenix.org
High-performance cryptographic code often relies on complex hand-tuned assembly
language that is customized for individual hardware platforms. Such code is difficult to …
language that is customized for individual hardware platforms. Such code is difficult to …
Continuous reasoning: Scaling the impact of formal methods
PW O'Hearn - Proceedings of the 33rd annual ACM/IEEE symposium …, 2018 - dl.acm.org
This paper describes work in continuous reasoning, where formal reasoning about a
(changing) codebase is done in a fashion which mirrors the iterative, continuous model of …
(changing) codebase is done in a fashion which mirrors the iterative, continuous model of …
High-assurance cryptography in the spectre era
G Barthe, S Cauligi, B Grégoire… - … IEEE Symposium on …, 2021 - ieeexplore.ieee.org
High-assurance cryptography leverages methods from program verification and
cryptography engineering to deliver efficient cryptographic software with machine-checked …
cryptography engineering to deliver efficient cryptographic software with machine-checked …
Gillian, part i: a multi-language platform for symbolic execution
We introduce Gillian, a platform for developing symbolic analysis tools for programming
languages. Here, we focus on the symbolic execution engine at the heart of Gillian, which is …
languages. Here, we focus on the symbolic execution engine at the heart of Gillian, which is …