Brochure di presentazione dell'area
(pdf,
it, 240 KB)
Presentazione Research Day 2017
(pdf,
it, 2429 KB)
| 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. | |
| 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/ |
| INdAM - Unità di Ricerca dell'Università di Verona | Questa pagina è dedicata all'unità di ricerca INdAM dell'Università di Verona. | |
| Logica | Logica in matematica ed informatica. | https://www.logicverona.it/ |
| 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 | https://amasini58.wixsite.com/quilab |
| Robotica | Il gruppo di ricerca si occupa di robotica non convenzionale | |
| SPY |
| Titolo | Responsabili | Fonte finanziamento | Data inizio | Durata (mesi) |
|---|---|---|---|---|
| Sistema Software di Pianoforte Virtuale su Tablet PC | Nicola Fausto Spoto | Viscount International S.p.A. | 05/02/15 | 11 |
| 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 |
