Added benchmarks from AWS NSym (Arm Symbolic Simulator) #16
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
This is great! Thank you for your contribution. It is also a good reminder for us that it is time to prepare a new benchmark submission repository for the coming release cycle. Unfortunately, we bumped against some limitations with the current Github workflow last year. We will have to overhaul those. I will leave this pull request open for now, and let you know when the new repository is ready. |
|
The new repository is now ready: https://github.com/SMT-LIB/benchmark-submission |
|
I've just opened a PR against the 2024 benchmark submission repo: |
|
Thank you very much! I will close the pull request here. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We have included some benchmarks produced by NSym, our symbolic simulator for Arm assembly code. The problems fit into two categories. The first are the raw benchmarks produced by the simulator, many of which are unknown by current solvers. The second are the problems after some manual and automated rewriting which makes the problems much easier to solve. We hope this will help motivate the community to identify opportunities to improve machine-code proofs via SMT.
Courtesy of Amazon Web Services - Automated Reasoning Group - Low Level Code Reasoning Team.