ODIN affronta la sfida di garantire l'affidabilità del codice sviluppando un'analisi dei programmi scalabile ed efficace. Gi approcci attuali combinano il codice con un'analisi della sua correttezza, spesso utilizzando un interprete astratto. Tuttavia, questo ha alcuni inconvenienti: l'analisi statica può generare falsi allarmi e questo diminuisce la credibilità dell'analisi. Inoltre, la precisione dell'analisi dipende da come il codice è scritto, rendendo complesso e costoso adattare l'analizzatore al codice. ODIN propone un approccio inverso: selezionare prima l'analisi e poi strutturare il codice in modo che sia conforme a tale analisi, minimizzando i falsi allarmi. Questo approccio comporta l'esplorazione della conformità del codice all'analisi del programma, un'area relativamente inesplorata, e mira a rendere l'analisi dei programmi più ampiamente utilizzata assicurando che il codice sia scritto in modo da facilitare la verifica.
Aree di ricerca coinvolte dal progetto | |
---|---|
Ingegneria del Software e verifica formale
Semantics and reasoning |
Strada le Grazie 15
37134 Verona
Partita IVA01541040232
Codice Fiscale93009870234
© 2024 | Università degli studi di Verona
******** CSS e script comuni siti DOL - frase 9957 ********p>