Skip to content

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