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

Add support to verify concurrent programs #41

Open
hbgit opened this issue Jul 3, 2020 · 0 comments
Open

Add support to verify concurrent programs #41

hbgit opened this issue Jul 3, 2020 · 0 comments
Assignees
Projects

Comments

@hbgit
Copy link
Owner

hbgit commented Jul 3, 2020

Add support for concurrency programs, e.g., the category ConcurrencySafety.

One possible solution is to adopt Lazy-Cseq* (https://www.southampton.ac.uk/~gp1y10/cseq/) tool to generate the C code, then apply Map2Check tool with its features to improve de verification. Note that Lazy-Cseq generates nondet calls for KLEE.

*CSeq is a framework that facilitates the development of code-to-code translations for concurrent C programs with POSIX threads based on sequentialization.

@hbgit hbgit self-assigned this Jul 3, 2020
@hbgit hbgit added this to In progress in Next Steps Jul 3, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
Next Steps
  
In progress
Development

No branches or pull requests

1 participant