• bytecode
• verifica
• subroutine
• java

Java è un linguaggio di programmazione interpretato: i sorgenti vengono compilati in file binari che contengono istruzioni codificate in un formato binario indipendente, il bytecode, ed interpretate dalla Java Virtual Machine. La verifica del bytecode Java consiste nell'analizzare la correttezza del codice, questa analisi su sistemi embedded richiede l'utilizzo ottimizzato delle risorse del sistema. In questa tesi è stato affrontato il problema della verifica delle subroutine per lo sviluppo di un verificatore di bytecode ottimizzato. In particolare è stato progettato e sviluppato un componente che effettua una verifica polivariante delle subroutine e minimizza l'occupazione di memoria durante la verifica. Nella tesi vengono riportati i risultati sperimentali ottenuti.