I recently had the opportunity to give a talk at the 2023 GHC Contributors’ Workshop, held at the Rapperswil-Jona campus of the Eastern Switzerland University of Applied Sciences (OST). The aim of this workshop was to help people learn how to work on the Glasgow Haskell Compiler (GHC), understand its internals better, and ultimately, increase […]

In this post, we describe a new memory model that we have added to our Macaw binary analysis framework which dramatically improves its performance when dealing with large binaries. Galois continues to invest in our binary analysis tools because they address a significant problem: many developers distribute closed source binaries that cannot be analyzed with […]

Overview We have added support for semi-automated proof assistance and repair to Crux, Galois’s symbolic testing tool for C/C++ and Rust. These new capabilities build on support for logical abduction provided by the cvc5 SMT solver that suggests possible facts for failed proof goals, that, when assumed, make the proof goals provable. This feature can […]

We are pleased to announce the release of Crux 0.6. Crux is a tool for verifying programs containing inline specifications. Crux works with both C/C++ code (via Crux-LLVM) and Rust code (via Crux-MIR). This release brings a variety of improvements, including: Crux-LLVM now has improved support for LLVM debug metadata when the debug-intrinsics option is […]

We are pleased to announce the release of Cryptol 2.13.0. Cryptol is a language for writing and specifying cryptographic algorithms. This release brings a variety of improvements, including: The sortBy function is now implemented using merge sort instead of insertion sort. This improves both asymptotic and observed performance on sorting tasks. “Type mismatch” errors now […]

This year Galois participated in the annual Competition on Software Verification (SV-COMP) for the first time with our verification tool, Crux. Preparing Crux to be in competition shape has been a project several years in the making, and we are very pleased to have reached this milestone. In this post, we will take a closer […]

We’ve been working to improve usability for SAW, our tool for verification of C and Java programs. The primary way that users interact with SAW is its specification and scripting language. In order to make SAW as accessible as possible, Python can now be used as that language for SAW! We’ve built an example to […]