Informatica teorica

La ricerca dipartimentale in informatica teorica si svolge su una panoplia di argomenti che testimonia della ricchezza e varietà di temi dell'area: ragionamento automatico, computabilità, concorrenza, protocolli crittografici, progetto ed analisi di algoritmi, logica equazionale e riscrittura, logica e verifica, logiche modali e temporali, pattern matching, computazione probabilistica, analisi di programmi, semantica, teoria della prova, teoria della computazione quantistica, sistemi di riscrittura, verifica mediante model checking.

Documenti

pdf Brochure di presentazione dell'area  (pdf,  it, 240 KB)
pdf Presentazione Research Day 2017  (pdf,  it, 2429 KB)
Maria Paola Bonacina
Professore ordinario
Mila Dalla Preda
Professore associato
Alessandra Di Pierro
Professore associato
Roberto Giacobazzi
Professore ordinario
Zsuzsanna Liptak
Professore associato
Andrea Masini
Professore ordinario
Isabella Mastroeni
Professore associato
Massimo Merro
Professore ordinario
Roberto Posenato
Professore associato
Romeo Rizzi
Professore ordinario
Roberto Segala
Professore ordinario
Ugo Solitro
Ricercatore
Nicola Fausto Spoto
Professore associato
Margherita Zorzi
Ricercatore a tempo determinato
Competenze
Argomento Persone Descrizione
Design and analysis of algorithms aderente allo standard  ACM 2012
Algoritmi su stringhe Zsuzsanna Liptak
Algoritmi e strutture dati per stringhe e sequenze; strutture dati di indicizzazione per stringhe e sequenze; pattern matching esatto, pattern matching approssimato, misure di distanza tra stringhe, compressione dati; problemi computazionali in biologia, web data, dati testuali, dati musicali; combinatoria delle stringhe, combinatoria delle parole.
Progettazione e analisi algoritmi per grafi Roberto Posenato
Romeo Rizzi
Studio di algoritmi per analisi di vincoli su grafi.
Formal languages and automata theory aderente allo standard  ACM 2012
Teoria della dimostrazione e teoria dei tipi Ugo Solitro
Margherita Zorzi
Sistemi deduttivi e di tipo basati su logiche costruttive e sulla logica lineare
Logic aderente allo standard  ACM 2012
Lambda Calculus Andrea Masini
Margherita Zorzi
Quantum and Probabilistic lambda calculi. Lambda calculus for Continuation Passing Style. Computational interpretation of modal proofs.
modal and temporal logics Andrea Masini
Margherita Zorzi
Proof theoretical analysis of modal and temporal logics. Modal and temporal logics for security. Distribute logics. Branching a linear temporal logics.
proof theory, Linear logic, Type theory Andrea Masini
Margherita Zorzi
Sequent calculi for modal, linear and temporal logics. Natural deduction systems for modal, linear and temporal logics. Labelled deductive systems. Type systems for CPS. Proof nets for linear and classical logics. Deductive systems for quantum computability.
Verifica del software Maria Paola Bonacina
Procedure di decisione per la soddisfacibilità modulo teorie e loro applicazione alla verifica di proprietà di programmi; generazione di invarianti mediante dimostrazione di teoremi; generazione di interpolanti mediante dimostrazione di teoremi; raffinamento di astrazioni per model checking o analisi statica mediante dimostrazione di teoremi
Models of computation aderente allo standard  ACM 2012
Computability Andrea Masini
Margherita Zorzi
Quantum and probabilistic computability. Implicit Complexity Theory.
Lambda Calculus Alessandra Di Pierro
Margherita Zorzi
Studio di versioni estese del lambda calcolo tipato, in particolare di sistemi di tipaggio probabilistici e della loro espressività.
Modelli per sistemi ibridi Roberto Segala
Studio di modelli per la rappresentazione di sistemi concorrenti che esibiscono comportamenti sia discreti che continui. Uso dei modelli per l'analisi di sistemi distribuiti di controllo.
Modelli stocastici concorrenti Roberto Segala
Studio di modelli di concorrenza che includono comportamenti stocastici. Uso di tali modelli per l'analisi di sistemi distribuiti e di protocolli che fanno uso di primitive crittografiche.
Models for concurrent, distributed, and mobile systems Massimo Merro
Calcoli di processo per sistemi concorrenti, distribuiti e con mobilita' di codice e/o agenti. Piu' di recente, calcoli di processo per sistemi ciberfisici e sistemi IoT.
Quantum computation theory Andrea Masini
Margherita Zorzi
Quantum lambda calculi. Topological quantum computing. Quantum computational complexity. Theory of quantum computable functions. Quantum theory of interaction.
Topological Quantum Computation Alessandra Di Pierro
Modelli di calcolo basati su sistemi di riscrittura per il Topological Quantum Computing (TQC). Studio di nuove tecniche algoritmiche basate sul modello matematico alla base di TQC.
Semantics and reasoning aderente allo standard  ACM 2012
Semantica di programmi Mila Dalla Preda
Roberto Giacobazzi
Isabella Mastroeni
Ugo Solitro
Nicola Fausto Spoto
Studio di tecniche di modelli semantici per la caratterizzazione di problemi di analisi e di sicurezza nei linguaggi di programmazione.
Semantics of concurrent, distributed, and mobile systems Massimo Merro
Semantica operazionali per linguaggi concorrenti, distribuiti e con mobilita' di codice e/o agenti. Tecniche di specifica di verifica del buon comportamento di tali sistemi.
Semantics of Probabilistic Languages Alessandra Di Pierro
Margherita Zorzi
Costruzione di semantiche operazionali e denotazionali per linguaggi probabilistici mediante algebre lineari e astratte.
Gruppi di ricerca
Nome Descrizione URL
Algoritmi Il gruppo persegue lo studio degli aspetti strutturali di problemi fondamentali in informatica e dei loro modelli. Lo scopo è porre le basi per la progettazione di algoritmi protocolli e sistemi migliori e comprenderne i limiti computazionali. Aree specifiche di interesse includono: progettazione di algoritimi, strutture dati, algoritmi su stringhe, complessità, ottimizzazione combinatoriale, codici e teoria dell’informazione, machine learning. I problemi investigati hanno forti connessioni con le aree della bioinformatica, delle reti di comunicazione, della ricerca operativa e dell’intelligenza artificiale.
Algoritmi in Bioinformatica e Calcolo Naturale Applicazione di metodi teorici e di analisi dati per modellare l’informazione sottostante ai processi biologici: algoritmi su grafi e stringhe per la biologia dei sistemi; strutture dati avanzate per sequenze di dati; misure di distanza tra sequenze biologiche; calcolo naturale (biotecnologico, e a membrane), riconoscimento di pattern, e apprendimento automatico da dati biomedicali.
ARLette - Laboratorio di Ragionamento Automatico Il gruppo svolge ricerche in Ragionamento Automatico: dimostrazione di teoremi, procedure di decisione, soddisfacibilità modulo assegnamenti, costruzione di modelli, riscrittura, e applicazioni.
Basi di dati e Sistemi Informativi Questo gruppo di ricercatori si occupa di varie tematiche nell'ambito dei sistemi informativi http://stars.di.univr.it
Blockchain L'attività del gruppo di ricerca riguarda diverse tematiche relative allo sviluppo e all'applicazione della tecnologia blockchain e dell'infrastruttura degli smart contracts.
ForME - Metodi Formali per la Progettazione di Sistemi Ingegneristici Obiettivo del gruppo di ricerca è applicare metodi formali alla modellazione, verifica e sintesi di sistemi ingegneristici. I domini spaziano dai sistemi temporizzati per andare fino ai sistemi ciberfisici non lineari.
INdAM - Unità di Ricerca dell'Università di Verona Raccogliamo qui le attività scientifiche dell'Unità di Ricerca dell'Istituto Nazionale di alta Matematica INdAM presso l'Università di Verona
Intelligenza Artificiale (IA) Il gruppo svolge ricerche in Intelligenza Artificiale: Ragionamento Automatico, Algoritmi di Ricerca, Rappresentazione della Conoscenza, Apprendimento Automatico, Sistemi Multi-Agenti e applicazioni.
Logica Logica in matematica ed informatica. https://www.logicverona.it/
NeST Progettazione e verifica delle tecnologie di comunicazione in grado di portare efficienza e sostenibilità in applicazioni chiave come industria, agricoltura, domotica, trasporti e gestione del territorio.
Quantum Informatics Laboratory - QUILAB Laboratorio di Informatica Quantistica https://quilab.github.io
SPY
Progetti
Titolo Responsabili Fonte finanziamento Data inizio Durata (mesi) 
JP2016 - Determinazione anticipata di minacce mediante analisi approssimata di similarità in big-code Mila Dalla Preda Joint Projects - assegnato e gestito dal Dipartimento 01/03/17 24
JP2016 - Interpretazione astratta di COBOL Isabella Mastroeni Joint Projects - assegnato e gestito dal Dipartimento 01/03/17 24
Sistema Software di Pianoforte Virtuale su Tablet PC Nicola Fausto Spoto Viscount International S.p.A. 05/02/15 11
JP2014 - Progettazione basata sull'interpretazione e misurazione delle trasformazioni del codice di protezione Roberto Giacobazzi Joint Projects - assegnato e gestito dal Dipartimento 01/11/14 24
Theorem proving algorithms for program analysis: interpolants, models, and termination (PRIN 2012 non finanziato) Maria Paola Bonacina 18/02/13 36
Generalizing Truth-Functionality: GeTFun Luca Vigano' Unione Europea 01/01/13 48
Static Analysis for Multithreading - Joint Project 2011 Massimo Merro Julia s.r.l. 01/01/13 30
MoreGAIN - Mismatch smoothing by smart recordering - Joint Projects 2011 Roberto Giacobazzi Energycamente s.r.l. 01/01/12 24

Attività

Strutture

Condividi