Skip to content

Randomized dfs #4

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

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Conversation

polgreen
Copy link

Introduce randomized DFS search.

I have used the command line option --randomized in combination with --dfs, because in a future pull request I also use this to randomize a shortest path based search heuristic

@polgreen
Copy link
Author

I assume symex is dead since these PRs have sat here for 2 years without anyone noticing and the master branch fails all CI? If that's the case I won't bother rebasing

@kroening ?

@martin-cs
Copy link
Collaborator

I think symex may be dead. Most of the symex-like functionality is now in CBMC which (thanks to @karkhaz @tautschnig @peterschrammel ) can do per-path analysis.

@polgreen
Copy link
Author

polgreen commented Nov 1, 2019

RIP symex. I won't re-implement these PRs for the per-path analysis though, since I was the sole user and I'm no longer using it. The ideas behind them weren't that novel, so the only thing lost if these die is coding effort.

@karkhaz
Copy link

karkhaz commented Nov 1, 2019

However, the depth-first search mode in CBMC isn't randomized, it's just a standard DFS. Implementing a randomized version shouldn't be very difficult, though. Happy to help if anyone still needs this feature.

@polgreen
Copy link
Author

polgreen commented Nov 1, 2019

Whoops, sorry Khareem, posted at the same time.

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.

3 participants