| Argomento | Persone | Descrizione | |
|---|---|---|---|
| Software creation and management aderente allo standard ACM 2012 | |||
| Blockchain and smart contracts |
Sara Migliorini Nicola Fausto Spoto |
Blockchain and smart contracts | |
| Sintesi di codice |
Roberto Giacobazzi |
Studio e sviluppo di tecniche per la sintesi di codice (o la trasformazione di codice) dalla specifica di proprietà semantiche del codice. | |
| Software creation and management |
Federica Maria Francesca Paci |
Study and development of formal and semi-formal methodologies and technologies for the creation and management of software systems | |
| Software Testing |
Mariano Ceccato |
Software Testing | |
| Software organization and properties aderente allo standard ACM 2012 | |||
| Analisi statica |
Mila Dalla Preda Roberto Giacobazzi Isabella Mastroeni Nicola Fausto Spoto |
Studio di tecniche di analisi statica per linguaggi di programmazione. Inferenza di proprietà della memoria dinamica dei programmi. Inferenza di proprietà di sicurezza per le informazioni manipolate dai programmi. | |
| Quantitative Static Analysis |
Alessandra Di Pierro |
Studio di metodi formali per l'analisi quantitativa dei programmi. Estensione delle tecniche classiche di analisi statica (data-flow, control-flow, abstract interpretation, type systems) all'analisi probabilistica e speculativa. | |
| Verification of wireless networks protocols |
Massimo Merro |
Tecniche semantiche e di model checking, anche statistico, per la verifica della correttezza di protocolli di reti wireless | |
| 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 |
Margherita Zorzi |
Quantum and Probabilistic lambda calculi. Lambda calculus for Continuation Passing Style. Computational interpretation of modal proofs. | |
| Logiche non classiche (intuizionista, lineare, modale, temporale) |
Davide Bresolin |
||
| modal and temporal logics |
Margherita Zorzi |
Proof theoretical analysis of modal and temporal logics. Modal and temporal logics for security. Distribute logics. Branching a linear temporal logics. | |
| Verifica del software |
Maria Paola Bonacina |
Procedure di decisione per la soddisfacibilità modulo teorie e assegnamenti, e loro applicazione alla verifica di proprietà di programmi; generazione di invarianti, generazione di interpolanti, e raffinamento di astrazioni (per model checking o analisi statica) mediante dimostrazione di teoremi | |
| Models of computation aderente allo standard ACM 2012 | |||
| Computability |
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 |
Davide Bresolin 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 |
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 |
|---|---|---|
| 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: soddisfacibilità modulo teorie e assegnamenti, procedure di decisione per la soddisfacibilità, dimostrazione di teoremi, 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 |
| Big Data Analytics | Questo gruppo di ricerca si occupa di tematiche relative alla rappresentazione, gestione e analisi di grandi quantità di dati caratterizzate in particolare dalla dimensione spaziale e temporale. | |
| 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 |
© 2024 | Verona University
