User Tools

Site Tools


Ongoing Projects

On this page you find information about the ongoing projects around the CPROVER code base. Before implementing a particular feature, please have a look here if someone is already working on something similar.

Description Affected code base Contact Status
Support the SMT-LIB theory of floating point CBMC solvers/smt2 Martin Merged but more work to do
General improvements and bug fixes to floating point CBMC solvers/floatbv Martin No known bugs (so am working on a new version so there are some!)
New floating point instrumentations CBMC analyses/ Martin Pending
Under-approximative acceleration CBMC goto-instrument/ Matt released in version 4.4
SMT2 backend parser with nested struct support CBMC solvers/smt2 Peter experimental, not merged in yet
Incremental BMC CBMC goto-symex/, cbmc/ Peter available on
Support for Heap theory CBMC solvers/smt2, goto-symex/ Peter ongoing, available on
Instrumentation for heap theory CBMC goto-instrument/ Peter ongoing
Instrumentation for MC/DC test generation CBMC goto-instrument/ Peter ongoing
Extension of acceleration instrumentation (to support Simulink-like code) CBMC goto-instrument/ Peter ongoing
Instrumentation for weak memory CBMC goto-instrument/ Vincent released in version 4.3; broken since 4.6; fixed in 5.0
Automatic memory fence insertion CBMC musketeer/ Vincent released in version 5.0
Support for weak memory models CBMC goto-symex/ Michael patches submitted, more models work in progress
Use of points-to analysis in symbolic execution CBMC goto-symex/, analyses/ Michael patches for supporting infrastructure submitted, main part work in progress
Linking objects with complex types CBMC linking/ Michael patches submitted
Improving and cleaning up the simplifier CBMC util/ Michael selected patches submitted, further ideas sought
Support for (static) thread priorities CBMC goto-symex/ Lihao Ongoing
Cleanup of static analysis and CFG code CBMC analyses/ Michael patches prepared, testing required
Dependence graph, slicing CBMC analyses/, goto-instrument/ Michael patches prepared, testing required
Rewrite of SSA renaming CBMC goto-symex/ Michael patches prepared, requires profiling
Field-sensitive SSA CBMC goto-symex/ Michael patches prepared, requires profiling
Alternative irep hashing, irep memory efficiency CBMC util/ Michael hashing patches included, memory efficiency patches require profiling
ongoing_projects.txt · Last modified: 2017/07/15 12:19 by kroening