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
Davide Bresolin
Incaricato alla ricerca
Mila Dalla Preda
Ricercatore a tempo determinato
Alessandra Di Pierro
Professore associato
Roberto Giacobazzi
Professore ordinario
Zsuzsanna Liptak
Ricercatore
Andrea Masini
Professore ordinario
Isabella Mastroeni
Professore associato
Massimo Merro
Professore associato
Roberto Posenato
Ricercatore
Romeo Rizzi
Professore associato
Roberto Segala
Professore ordinario
Ugo Solitro
Ricercatore
Nicola Fausto Spoto
Professore associato
Competenze
Argomento Persone Descrizione ISI-CRUI
Theory of computation - 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. Computer Science & Engineering
Progettazione e analisi algoritmi per grafi Roberto Posenato
Romeo Rizzi
Studio di algoritmi per analisi di vincoli su grafi. Computer Science & Engineering
Theory of computation - Formal languages and automata theory aderente allo standard  ACM 2012
Teoria della dimostrazione e teoria dei tipi Gianluigi Bellin
Ugo Solitro
Sistemi deduttivi e di tipo basati su logiche costruttive e sulla logica lineare Computer Science & Engineering
Theory of computation - Logic aderente allo standard  ACM 2012
Lambda Calculus Andrea Masini
Quantum and Probabilistic lambda calculi. Lambda calculus for Continuation Passing Style. Computational interpretation of modal proofs. Computer Science & Engineering
Logiche non classiche (intuizionista, lineare, modale, temporale) Davide Bresolin
Computer Science & Engineering
modal and temporal logics Andrea Masini
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
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 Computer Science & Engineering
Theory of computation - Models of computation aderente allo standard  ACM 2012
Computability Andrea Masini
Quantum and probabilistic computability. Implicit Complexity Theory. Computer Science & Engineering
Lambda Calculus Alessandra Di Pierro
Studio di versioni estese del lambda calcolo tipato, in particolare di sistemi di tipaggio probabilistici e della loro espressività.
Modelli per sistemi ibridi Davide Bresolin
Marta Capiluppi
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. Computer Science & Engineering
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. Computer Science & Engineering
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. Computer Science & Engineering
Quantum computation theory Andrea Masini
Quantum lambda calculi. Topological quantum computing. Quantum computational complexity. Theory of quantum computable functions. Quantum theory of interaction. Computer Science & Engineering
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.
Theory of computation - Semantics and reasoning aderente allo standard  ACM 2012
Semantica di programmi Mila Dalla Preda
Roberto Giacobazzi
Isabella Mastroeni
Durica Nikolic
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. Computer Science & Engineering
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. Computer Science & Engineering
Semantics of Probabilistic Languages Alessandra Di Pierro
Costruzione di semantiche operazionali e denotazionali per linguaggi probabilistici mediante algebre lineari e astratte.
Gruppi di ricerca
Nome Descrizione URL
ARLette Ricerca in ragionamento automatico http://profs.sci.univr.it/~bonacina/ARLette.html
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
Bioinformatica e Calcolo Naturale Analisi algoritmica di processi biologici http://bioinformatics.di.univr.it/
Logica Logica in matematica ed informatica. https://logicseminarverona.wordpress.com/
Progettazione di sistemi elettronici (ESD - Electronic Systems Design) Tecniche per la progettazione automatica di sistemi elettronici, basate su linguaggi formali e metodologie corrette per costruzioni o formalmente verificate http://esd.scienze.univr.it/
QUILAB Quantum Informatics Laboratory
Robotica Il gruppo di ricerca si occupa di robotica non convenzionale
SPY
Progetti
Titolo Responsabili Fonte finanziamento Data inizio Durata (mesi) 
Generalizing Truth-Functionality: GeTFun Luca Vigano' Unione Europea 01/01/13 48
MoreGAIN - Mismatch smoothing by smart recordering - Joint Projects 2011 Roberto Giacobazzi Energycamente s.r.l. 01/01/12 24
Sistema Software di Pianoforte Virtuale su Tablet PC Nicola Fausto Spoto Viscount International S.p.A. 05/02/15 11
Static Analysis for Multithreading - Joint Project 2011 Massimo Merro Julia s.r.l. 01/01/13 30
Static Analysis for Multithreading - Joint Project 2011 Massimo Merro Julia s.r.l. 01/01/13 30
Theorem proving algorithms for program analysis: interpolants, models, and termination (PRIN 2012 non finanziato) Maria Paola Bonacina 18/02/13 36

Attività

Strutture