Zum einen überprüft der Verifier die in der JVM-Spezifikation aufgeführten Anforderungen. Diese betreffen im wesentlichen die Typsicherheit, sowie die Einhaltung von Zugriffsbeschränkungen bei Zugriffen auf Felder und Methoden.
Neben diesen ,,Standard-Anforderungen'' werden weitere, JX-spezifische Anforderungen geprüft. Zum Beispiel darf eine Interrupt Behandlungsroutine nur dann installiert werden, wenn sichergestellt ist, dass sie innerhalb einer gewissen Zeit terminiert. Zu diesem Zweck wurde eine Analyse entwickelt, die es für viele Methoden erlaubt, eine Abschätzung der maximalen Ausführungsdauer statisch zu bestimmen. Da dieses Problem jedoch im Allgemeinen unentscheidbar ist, können nicht alle Methoden analysiert werden. Die nicht analysierbaren Methoden werden durch neue ersetzt, die Laufzeitüberprüfungen enthalten, welche eine Terminierung innerhalb der Zeitvorgabe sicherstellen.
Außerdem hat der Verifier die Aufgabe, Analysen durchzuführen, die der Optimierung dienen. Beispielsweise wird eine ,,Null-Pointer Analys" durchgeführt, um statisch zu überprüfen ob eine Referenz den Wert null hat oder nicht. Kann zur Verifikationszeit festgestellt werden, dass die Referenz ungleich null ist, so kann eine entsprechende Laufzeitüberprüfung entfallen.
Um die verschiedenen Verifikationsschritte zu vereinheitlichen wurde
eine allgemeine Vorgehensweise für die Bytecodeanalyse implementiert.
First of all, standard Java Bytecode verification was implemented. It guarantees that the constraints described by the JVM-Specification are met. Most of these are concerned with type-safety and the restrictions on field and method access imposed by access-flags.
Besides those Java rules, there are additional constraints the verifier
ensures in JX. For example, an interrupt handler can only be installed
after verifying that the handler terminates within a certain time
bound. To this end, a worst case execution time analysis was developed,
which allows to statically estimate the execution time for a wide range
of methods. However, as this problem is in general undecidable, not all
methods can be analyzed. Those methods that cannot be analyzed are replaced
with new ones, which contain runtime-checks to ensure termination within
a time limit.
Another aim of the verifier is to analyse the code to find optimisation possibilities. For example, a 'null-pointer analysis' can be performed, which checks whether a reference is valid or not. If the reference is valid, the compiler can omit runtime checking this reference.
To even the different verification processes, a framework for bytecode
analysis was implemented.