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 […]
Then the program makes a few stack allocations before the first call to @mk: Conclusion Pointer analysis is a foundational static analysis. We hope you’ve enjoyed learning a bit more about it! More information about cclyzer++ can be found in the project documentation.
We are pleased to announce that Galois is open-sourcing cclyzer++, a new pointer analysis for languages that compile to LLVM, including C and C++. Pointer analysis is a foundational static analysis with applications to the problems of program optimization, verification, bug finding, and many others. At Galois, we designed cclyzer++ with two main use cases […]
Following our previous blog post, The Next Assembly Line, Galois continues our quest to invent tooling that can transform the DevOps process for developing and maintaining software. One of the unwritten pieces of common knowledge in software is that software rarely meets the models of design as implemented. As such, the notion of utilizing modern, […]
Conclusion You’ve now seen most of the essential features of cclyzer++. The next post will explore some more advanced topics and bring it all together with a larger example.
At the Mining Software Repositories (MSR2022) conference in May, we presented our LAGOON tool resulting from the DARPA SocialCyber AIE, and led a discussion session on reducing complexity of machine learning. LAGOON provides a comprehensive platform for analyzing and investigating open-source software (OSS) communities for potentially malicious contributors. This is accomplished by ingesting multiple types […]
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 […]
Cryptography continues to rapidly transform our world. It seems like every day there’s a new story about fully homomorphic encryption, blockchains, and how these technologies secure billions and even trillions of dollars in assets. We’ve talked about cryptographic algorithms and twice about cryptographic assurance. People who work with these concepts every day have been the […]
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 take pride in personally connecting with all interested partners, collaborators and potential clients. Please email us with a brief description of how you would like to be connected with Galois and we will do our best to respond within one business day.