Milestone expires on Dec 31, 2020
Unstarted Issues (open and unassigned)
- Add missing POSIX features
- create VM images for all historical versions of DIVINE
- Verification of boost's concurrent data structures
- Add support of usage glibc instead of PDCLib
- Verification of lvmetad (LVM2's metadata caching daemon)
- Verification of clvmd (LVM2's cluster locking & coordination daemon)
- Verification of lvmlockd (LVM2's new distributed locking daemon)
- Visualization of heap of program/counterexample
- Probabilistic extension for data-symbolic verification
- Objective C/C++ verification with DIVINE
- Syscall record and replay.
- Verification of Folly.
- Parametrized-Precision Verification for C/C++.
- Verification of NSCD (glibc's name serice cache daemon)
- Verification of Hazard Pointers.
- Verification of Intel TBB concurrent data structures
- Support for WIN32 threads.
- Partial Order for LLVM.
- Timed LLVM & UppAll to LLVM.
- Probabilistic Store Reachability.
- DVE to C++/DiVM translation.
- CTL* Model Checking.
- Slicing Parallel Programs using Dependency Graphs
Completed Issues (closed)