Prototype slicer for preprocessing reachability verification tasks

Reachability slicer based on context-sensitive flow-insensitive separation analysis with typed polymorphic regions and dependency analysis with transitive closures. Intended to be used with a reachability verifier e.g. CPAchecker, Ultimate Automizer, CBMC, for verification tasks prepared from Linux device drivers. The slicing is performed modulo termination. So the slicer works under assumption that all the code (except for explicitly specified functions) necessary terminates and thus can be removed if it doesn't influence reachability.

Issue tracking

open closed Total
Bug 0 0 0
Feature 0 0 0
Support 0 0 0
User Story 0 0 0
Developer Request 0 0 0
Task 0 0 0
Feature_ 0 0 0

View all issues


Manager: Mikhail Mandrykin

Developer: Mikhail Mandrykin

Project Creator: Mikhail Mandrykin