Nella vita di un programma possiamo distinguere tre aspetti: sviluppo, rilascio e manutenzione. La fase di sviluppo comporta l'analisi delle specifiche del problema dato e la sintesi di un codice (scritto in uno specifico linguaggio di programmazione) che soddisfi alle richieste del problema e possibilmente non contenga errori. Una volta che ottenuto il codice finale "accettabile" si potrà procedere al suo rilascio. Nel caso si evidenzino errori non individuati nello sviluppo si dovrà procedere alla fase di manutenenzione del software prodotto, ovvero alla correzione degli errori, per poi arrivare ad un nuovo rilascio! Già in questa banale schematizzazione possiamo evidenziare uno degli aspetti più delicati della produzione del software: la produzione di codice (il più possibile) corretto, in modo da ridurre il più possibile i costi di manutenzione. Purtroppo lo studio approfondito (con metodi della logica-matematica) della questione della correttezza porta ad un importante risultato negativo: non è possibile in generale decidere a posteriori se il codice prodotto soddisfa alle specifiche del problema dato; in altre parole, non si può in generale verificare la correttezza di un programma, anche se ovviamente questo è possibile per casi speciali o particolarmente semplici. Di qui l'importanza di individuare strumenti e metodi che cerchino di evitare a priori i problemi legati alla verifica ed alla analisi del codice. Questo obbiettivo viene perseguito sostanzialmente per mezzo di due tecniche fondate su una rigorosa definizione della semantica dei linguaggi di programmazione: (1) Sviluppo di metodi per la sintesi di programmi il più possibile corretti; (2) Analisi del comportamento dei programmi prima della loro esecuzione o implementazione su di una macchina reale.
Scopo del profilo è quello di fornire il laureato in informatica di una avanzata "attrezzatura" logico-matematica che gli consenta una maggiore profondità nell'analisi, nella comprensione e nella soluzione dei problemi legati all'utilizzo dei linguaggi di programmazione e caratteristici della sua attività informatica, indipendentemente da specifiche applicazioni o linguaggi di programmazione scelti. La conoscenza di queste metodologie permette di affrontare problemi complessi in aree di ricerca avanzate, quali ad esempio: la progettazione di sistemi per la verifica formale di programmi, la progettazione di linguaggi di programmazione di nuova concezione, e la realizzazione di analizzatori statici per l'ottimizzazione automatica del codice, la trasformazione e la parallelizzazione/vettorizzazione automatica di programmi, e per l'analisi di sicurezza in sistemi distribuiti e su rete.