This thesis presents a methodology for the formal verification of memory organizations in System-on-Chip (SoC) designs described in IP-XACT. The approach involves modeling the address map structures of the design's IP-XACT description and its spreadsheet-based global address map specification into a unified graph model we developed, called an Address Map Graph (AMG). Additionally, it introduces an analysis of AMGs to determine the equivalence of their mapped addresses, called Graph Bitmapping Equivalence (GBE). The methodology was implemented through a series of modular programs integrated into a solution flow. These programs process the spreadsheet memory specifications and IP-XACT design representations into AMGs and perform efficient GBE calculation and detailed reporting. The solution was evaluated using a state-of-the-art mid-size SoC design as a case study. Verification of results was performed using commercially available design analysis tools. The results demonstrated the developed solution was effective to analyze and verify the memory organization of complex SoC designs and to assist in identifying the causes of discrepancies.

Software reuse in the form of dependencies has become widespread in software development. However, dependencies have the potential to suffer from vulnerabilities, thereby potentially putting depending projects at risk. Dependency analysis software can be used to manage vulnerable dependencies, such as Dependabot. Yet, such programs are generally inaccurate as a result of false positives, due to the limitations of package-level analysis. In the case of a false positive vulnerability recommendation, a software project imports a vulnerable dependency, but does not use any of its vulnerable functions. While most developers already do not pay enough attention to using vulnerable dependencies, false positives can only make this worse. Instead, function-level vulnerability analysis has the capability to eliminate package-level false positives. In this paper, research is performed to gain quantitative insight in the improvement of function-level over package-level analysis in terms of recommendation correctness. A package-level analysis simulation in combination with a function-level analysis was performed, built with the FASTEN framework. The latter uses RTA call graph generation and method tracing to remove package-level false positives. In total, 4071 open-source repositories were analyzed with 393 open-source vulnerabilities, of which 259 projects had positive recommendations. Comparison shows that 85\% of package-level recommendations are false positives, which are removed by performing function-level analysis instead. This indicates significant improvement by function-level analysis. Research on greater data sets would be needed for further insight in this improvement.