Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Added an FAQ about array theory in CBMC #8

Open
wants to merge 3 commits into
base: main
Choose a base branch
from

Conversation

akshayutture
Copy link

Issue #, if available:
Need an FAQ about CBMC's array-theory feature.

Description of changes:
Added an FAQ about CBMC's array-theory feature.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

@akshayutture
Copy link
Author

Do you think it is necessary to provide users with a primer on array-theory?

@tautschnig
Copy link
Member

At some point we need to consider where to draw the line: training material that both appeals to people completely new to verification (providing a gentle transition from testing to verification) as well as covering details about the decision procedure seems quite a stretch. Now I completely get that users are impacted by this, and quite likely it is users that are rather new to verification. But really I think this means we need to prioritize working on the array back-end.

@akshayutture
Copy link
Author

akshayutture commented Jul 29, 2022

Okay yeah that makes a lot of sense. The tutorial does seem to focus on new users and this point may be a little too detailed for new CBMC users. I'll close this PR then.

@jimgrundy jimgrundy reopened this Aug 10, 2022
@jimgrundy
Copy link
Contributor

Actually... I've been encountering the need to force the tool to use the array theory.
Rather than killing this I propose that we
1/ Add a section on Infrequently Asked Questions (aka advanced questions)
2/ Add a date to the material so people know when it was written

Copy link
Contributor

@jimgrundy jimgrundy left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants