We extend an open source static analysis framework to incorporate a range of exploratory static analysis methods, including code slicing zero/non-zero testing, and value flow analysis. We extend the same infrastructure to support embedding of properties within the program and automated checking of those properties using model checking. Key novelties of this proposal is user-driven combination of techniques and an open source result.
Keywords: Operating Systems, Hypervisors, High Assurance, Static Analysis, Open Source, Assurance Maintenance.
