According to their paper (OSDI'08), symbolic execution tool KLEE needs about 1 hour to generate test cases for a single COREUTIL application. I am wondering if it can run in parallel?(say, multi-threaded on multicore or even GPU)?
Can symbolic execution tool KLEE run in parallel?
851 Views Asked by JackWM At
1
There are 1 best solutions below
Related Questions in DEBUGGING
- How to pass the value of a function of one class to a function of another with the @property decorator
- Visual Studio C++, breakpoints not stopping debugging DLL (GODOT GDExtention)
- Playwright JS: Getting an error when debugging using line numbers
- C++ skips line when promting for user to enter name of person being added to a string array
- Xcode: Can't Attach to process
- unity navmeshsurface prefab not found or whatever
- It seems to be a bug about "base::trace()" or "methods:::.TraceWithMethods()"?
- How to check reference counting issues when doing direct manipulations of CPython objects?
- How to scroll to the bottom of console window in PyCharm2019 automatically?
- need help debugging prolog
- Is there a way to deactivate (but not delete) conditional breakpoints when debugging?
- How can i debug a python exe which is created by using pyinstaller?
- Increment or Decrement volume programmatically on Xiaomi device adjusts it by 10 steps instead of one step
- Checking request JSON with image data
- Why cannot I set font of `xlabel` in `plotmf` in MATLAB?
Related Questions in STATIC-ANALYSIS
- Ansible role analysis with Checkov - facts evaluation?
- Flutter SonarQube: "The main branch has no lines of code."
- the expressionType and includePath of CDT parser
- Adding entry to program header table
- Static checker that number of arguments to python logging matches number of placeholders
- Why am I getting this error when using dataflow in Codeql
- How to disallow exception to curly_braces_in_flow_control_structures linter rule in dart?
- Security scan flagged local variable for heap inspection in C Function
- Is it possible to use Eclipse JDT static analysis for null annotations when compiling from the command line?
- Remove directory from sonar analyzer
- Sonar qube issue in using aes-256-cbc algoritm, stating Make sure that encrypting data is safe here
- Programming language/library that uses dataflow analysis to fetch only required data from the database
- Export comments from Fortify Software Security Center
- Changing lint configuration based on Cargo profile
- Can I reproduce eslint's "prefer-object-spread" rule using ast-grep?
Related Questions in SYMBOLIC-COMPUTATION
- Matlab - Symbolic matrix ranks different after vpa application
- Use symbolic matlab for flexible number of arguments and functions
- Matlab symbolic equation rearranging
- cannot open Singular on a running emacs
- Mincuts from graphs to find permutations that break the system into disjoint sets?
- Multiply symbolic function by differential operator to create derivative
- 5D tensor in Theano
- SymPy symbolic integration returns error
- Can symbolic execution tool KLEE run in parallel?
- How to construct a subring of a polynomial ring in Magma
- Matlab Symbolic expression creates overflow
- Computer Algebra Systems that support variable sized matrices
- Create general symbolic array using MATLAB
- Common Lisp - symbolic polynomial calculation
- Replacing symbolic derivatives in MATLAB
Related Questions in KLEE
- Setting up KLEE for testing a specific Linux kernel function
- How to solve "ptrace operation not permitted"?
- What is the difference between branch and fork function in Executor.cpp on KLEE?
- Why IR is needed for symbolic execution?
- How do I create a testcase that targets a specified branch?
- I am unable to get back the file I saved after exiting from the Klee
- KLEE: ERROR: Loading file /usr/local/lib/klee/runtime/klee-uclibc.bca failed: Invalid record
- How to use llvm target initialize function
- Is this how to test a stateful API with klee symbolic execution?
- Undefined reference to klee when building s2e
- KLEE: Appending variables with different alignment need to be linked
- LLVM interate over the content of a structure accessed through pointer in KLEE code
- How to use the max-time tag with klee
- Configure Error on KLEE Docker: C compiler cannot create executables
- C compiler cannot create executables during build of Coreutils with LLVM
Trending Questions
- UIImageView Frame Doesn't Reflect Constraints
- Is it possible to use adb commands to click on a view by finding its ID?
- How to create a new web character symbol recognizable by html/javascript?
- Why isn't my CSS3 animation smooth in Google Chrome (but very smooth on other browsers)?
- Heap Gives Page Fault
- Connect ffmpeg to Visual Studio 2008
- Both Object- and ValueAnimator jumps when Duration is set above API LvL 24
- How to avoid default initialization of objects in std::vector?
- second argument of the command line arguments in a format other than char** argv or char* argv[]
- How to improve efficiency of algorithm which generates next lexicographic permutation?
- Navigating to the another actvity app getting crash in android
- How to read the particular message format in android and store in sqlite database?
- Resetting inventory status after order is cancelled
- Efficiently compute powers of X in SSE/AVX
- Insert into an external database using ajax and php : POST 500 (Internal Server Error)
Popular # Hahtags
Popular Questions
- How do I undo the most recent local commits in Git?
- How can I remove a specific item from an array in JavaScript?
- How do I delete a Git branch locally and remotely?
- Find all files containing a specific text (string) on Linux?
- How do I revert a Git repository to a previous commit?
- How do I create an HTML button that acts like a link?
- How do I check out a remote Git branch?
- How do I force "git pull" to overwrite local files?
- How do I list all files of a directory?
- How to check whether a string contains a substring in JavaScript?
- How do I redirect to another webpage?
- How can I iterate over rows in a Pandas DataFrame?
- How do I convert a String to an int in Java?
- Does Python have a string 'contains' substring method?
- How do I check if a string contains a specific word?
Most static analysis tools are built using languages which are essentially single-threaded (C, C++, Java).
While parallelism support is available in such languages, as a general rule the static analysis tool builders do not take advantage of it. Part of the problem is that the parallelism in such tools is highly irregular, and does not come in easily-found large chunks which keeps the overhead down, a necessity for ensuring efficient parallelism. This makes it hard for the tools designers to find/designate such chunks, and they are already fighting the difficult problem of making their tool work.
KLEE itself I don't think is parallel for this reason. There is work on dividing the analysis supporting test generation into big chunks to hand to parallel running copies of KLEE ("Cloud9"); this is one way to divide the work up but these are really big computational grains, distributed across a cloud of independent processors. One of the key issues is "load balancing" (giving the right amount of work to each copy so that the parallelelism is well used). See http://dslab.epfl.ch/pubs/cloud9.pdf
(See my bio for a line of tools that has explicitly parallel foundations with fine-grain computations based on SMT).