• abstract interpretation
• bug detection
• formal methods
• java
• static analysis

Software has become indispensable in modern society, with its complexity increasing at a tremendous rate year after year. The omnipresence of software systems in critical sectors such as aerospace, healthcare, finance, and autonomous systems has made their reliability paramount, given that the consequences of errors, defects, or bugs can be catastrophic.
Failures in these domains can lead to severe economic loss, privacy breaches, or even endanger human lives. As a result, the demand for tools that rigorously ensure the correctness and security of software before deployment has never been more pressing. Among such tools, static analyzers play a critical role by detecting potential issues in the code without requiring its execution.
Static analyzers can identify bugs, verify system properties, and guarantee certain correctness conditions, making them essential for developing reliable software in high-stakes environments.

In this thesis, we present a JAVA implementation of the Abstract Interpretation framework, a formal technique for static program analysis. Abstract Interpretation allows for the derivation of sound approximations of a program's behavior by mapping its execution into an abstract domain. This process enables us to detect inconsistencies in the semantics of a program and identify errors, such as potential runtime exceptions or security vulnerabilities, without the need for actual program execution. Our implementation focuses on creating a static analysis that is correct by construction, meaning it guarantees soundness given a well-defined abstraction. By offering rigorous mathematical underpinnings, Abstract Interpretation can verify properties of the program that are crucial for safety and security, especially in complex systems where traditional testing approaches may be inadequate.

More specifically, we begin by introducing the fundamental principles of Abstract Interpretation and the underlying concepts of domain theory. Domain theory provides the mathematical foundation for representing and reasoning about program states in abstract form. We then present in detail our JAVA implementation, which serves as a comprehensive library for static analysis, featuring pre-implemented domains and abstractions that can be readily used by developers while also allowing users to define custom analyses by specifying new domains or extending existing ones. This flexibility is particularly valuable in specialized applications, where the default abstractions might not be sufficient for capturing the nuances of a particular system.

Furthermore, our implementation supports generic domain refinement, an advanced technique that improves the precision of the analysis by extending an abstract domain with a collection of logical predicates. These predicates allow the analysis to differentiate between elements within the domain based on their specific properties, thereby refining the granularity of the analysis. By incorporating these logical distinctions, we can enhance the precision of our analysis results, reducing the occurrence of false positives and making the tool more reliable for practical use.

In particular, the domain refinement in our implementation leverages several advanced features of the JAVA programming language. By utilizing Generics and Invariance, we have defined a generic class structure that naturally encapsulates both domains and predicates. This design allows domain operations to be performed in a modular and reusable manner, without requiring external code to handle domain-specific details. Moreover, by employing the functional interface Predicate and structuring domain elements as superclasses and subclasses, we make use of dynamic dispatch to define predicates that can be applied uniformly across both concrete and abstract domains. This feature eliminates the need for predicate redefinition when switching between different levels of abstraction, further improving the efficiency and flexibility of the analysis.

Finally, after a brief discussion on how the library was tested, we showcase our approach’s effectiveness by highlighting how simple is for the end user to repair articulate underlying domains.