| Topic | People | Description | |
|---|---|---|---|
| Software creation and management standard compliant ACM 2012 | |||
| Blockchain and smart contracts |
Sara Migliorini Nicola Fausto Spoto |
Blockchain and smart contracts | |
| Code synthesis |
Roberto Giacobazzi |
Study and development of techniques for the synthesis of code (or code transformers) from the specification of semantic code properties. | |
| 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 standard compliant ACM 2012 | |||
| Static Analysis |
Mila Dalla Preda Roberto Giacobazzi Isabella Mastroeni Nicola Fausto Spoto |
Study of techniques for the static analysis of programming languages. Inference of properties of the heap memory used by programs. Inference of security properties for information manipulated by computer programs. | |
| Quantitative static analysis |
Alessandra Di Pierro |
Study of formal methods for quantitative analysis of programs. Extension of classical program analysis techniques (data-flow, control-flow, abstract interpretation,type systems)to probabilistic and speculative analysis for program optimisation and transformation. | |
| Verification of wireless network protocols |
Massimo Merro |
Semantics-based and model-checking techniques for the verification of wireless network protocols | |
| Design and analysis of algorithms standard compliant ACM 2012 | |||
| String algorithms |
Zsuzsanna Liptak |
Algorithms and data structures for strings; indexing for string problems; exact pattern matching, approximate pattern matching, string distance measures, storage, compression; problems arising in applications of strings such as computational biology, web data, textual data, big data, musical analysis; string combinatorics,combinatorics on words. | |
| Design and analysis of algorithms for graphs |
Roberto Posenato Romeo Rizzi |
Design and analysis of algorithms for constraint analysis in graphs. | |
| Formal languages and automata theory standard compliant 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 standard compliant 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. | |
| Software Verification |
Maria Paola Bonacina |
Decision procedures for satisfiability modulo theories and assignments and their application to reasoning about programs; invariant generation, interpolation, and abstraction refinement (for either model checking or static analysis) via theorem proving | |
| Models of computation standard compliant ACM 2012 | |||
| Computability |
Margherita Zorzi |
Quantum and probabilistic computability. Implicit Complexity Theory. | |
| Lambda Calculus |
Alessandra Di Pierro Margherita Zorzi |
Study of extended versions of the typed lambda calculus, in particular of probabilistic typing systems and their expressivity. | |
| 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 |
Process calculi for concurrent, distributed, and mobile systems. More recently, process calculi for cyber-physical systems and IoT systems | |
| 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 |
Re-writing systems for Topological Quantum Computation (TQC) and study of new algorithmic techniques based on the mathematical model of TQC. | |
| Semantics and reasoning standard compliant ACM 2012 | |||
| Program semantics |
Mila Dalla Preda Roberto Giacobazzi Isabella Mastroeni Ugo Solitro Nicola Fausto Spoto |
Development of semantic models for characterizing security and analysis problems of programming languages | |
| Semantics of concurrent, distributed, and mobile systems |
Massimo Merro |
Semantics of concurrent, distributed, and mobile computations. Associated with these semantic theories come specification techniques and verification technologies for assuring the behaviour of systems | |
| Semantics of Probabilistic Languages |
Alessandra Di Pierro Margherita Zorzi |
Construction of operational and denotational semantics via linear and abstract algebras. | |
| Name | Description | 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
******** CSS e script comuni siti DOL - frase 9957 ********p>
