Progetti di Ricerca

Di seguito sono elencati i progetti di ricerca che sono stati finora segnalati all’associazione nei quali il contributo della programmazione logica è stato di primaria importanza.

E’ possibile segnalare ulteriori progetti scrivendo a  Fabio Fioravanti.

I progetti sono ordinati per anno di inizio progetto.

 

Titolo Progetto Il riconoscimento molecolare nelle interazioni proteina-ligando, proteina-proteina e proteina superficie: sviluppo di approcci sperimentali e computazionali integrati per lo studio di sistemi di interesse farmaceutico.
Tipo di Progetto FIRB 2003
Anno di Inizio Progetto 2003
Anno di Fine Progetto 2010
Sito Web http://clp.dimi.uniud.it/projects/
Contributo della Programmazione Logica L’unità udinese del progetto si è occupata del problema della predizione della struttura terziaria della proteina con tecniche di logic programming. I principali contributi sono:1.A. Dal Palù, A. Dovier, and F. Fogolari.

Constraint Logic Programming approach to protein structure prediction.

BMC Bioinformatics 2004, 5:186, 30 November 2004

A. Dal Palu’, A. Dovier, and E. Pontelli.

A constraint solver for discrete lattices, its parallelization, and application to protein structure prediction.

SOFTWARE-PRACTICE AND EXPERIENCE, Volume 37, Issue 13, Pages 1405-1449, 2007

A. Dal Palù, A. Dovier, F. Fogolari, and E. Pontelli. CLP-based protein fragment assembly.

Theory and Practice of Logic Programming, special issue dedicated to ICLP 2010.

Consorzio (affiliati GULP) Università di Udine, DIMI
Referente GULP Agostino Dovier

 

Titolo Progetto Tecniche innovative per la programmazione con vincoli in applicazioni strategiche
Anno di Inizio Progetto 2010
Anno di Fine Progetto 2010
Sito Web http://clp.dimi.uniud.it/projects/
Abstract Obiettivo di questo progetto e’ lo sviluppo di strumenti e tecniche che consentano di ovviare ad alcuni dei limiti esistenti all’impiego su larga scala di solver CLP e ASP, in particolar modo connessi al trattamento di problemi di dimensioni e complessita’ reali, ove vengano imposti pressanti requisiti di efficienza nella ricerca della soluzione.Il focus viene posto sullo studio di metodologie miste che prevedano l’integrazione di CP con la ricerca locale e con tecniche provenienti da discipline quali la ricerca operativa, l’analisi numerica, ecc. Il tutto per trattare efficientemente vincoli esprimibili su domini eterogenei, complessi e strutturati. Al contempo si studieranno approcci alla integrazione tra tecniche CP e programmazione logica non-monotona, con l’obiettivo di dimostrare come CP possa fungere da motore inferenziale per il formalismo dell’Answer Set Programming.

Le soluzioni cosi’ progettate saranno validate tramite l’applicazione concreta a problemi tratti da contesti reali e di interesse strategico, quali la predizione della struttura di proteine, la pianificazione e scheduling, la configurazione di prodotto.

Contributo della Programmazione Logica Constraint logic programming,Constraint programming,

Answer set programming,

Action description languages,

Multi-agent systems.

Consorzio (affiliati GULP) Federico BergentiDario Campagna

Raffaele Cipriano

Alessandro Dal Palu’

Agostino Dovier

Andrea Formisano

Raffaella Gentilini

Gianfranco Rossi

Referente GULP Andrea Formisano
Budget 5000

 

Titolo Progetto Sistema automatico ed intelligente di tracciamento delle siviere in uno stabilimento siderurgico
Tipo di Progetto Progetto Regione FVG
Anno di Inizio Progetto 2011
Anno di Fine Progetto 2013
Sito Web http://clp.dimi.uniud.it/projects/
Contributo della Programmazione Logica E’ stato utilizzato il constraint logic programming per definire un generatore di codici correttori da realizzarsi su tabelle quadrate da apporre su siviere mobili in un ambiente industriale estremo (acciaieria). Il tutto inserito e validato con un sistema di tracciamento basato su telecamere site piuttosto lontane a causa delle temperature.
Consorzio (affiliati GULP) Univ. di UDINE, DIMI
Consorzio (altri) QUALIBIT SRL
Referente GULP Agostino Dovier

 

Titolo Progetto MAS-DALI per applicazioni di risparmio energetico
Tipo di Progetto Interno
Anno di Inizio Progetto 2011
Anno di Fine Progetto
Sito Web http://www.disim.univaq.it
Abstract Il progetto vuole esplorare l’utilizzo di sistemi multi agente ibridi per l’azionamento e controllo di sistemi di climatizzazione al fine del risparmio energetico, sfruttando l’inerzia termica degli edifici, le preferenze dell’utente e i sensori ambientali connessi tramite una rete domotica.
Contributo della Programmazione Logica Gestione delle preferenze tramite answer set programmingLogic Agent programming

Induzione

Comples Event Processing

Consorzio (affiliati GULP) Dott. Ing. Giovanni De Gasperis, DISIM, UnivAQProf. Stefania Costantini, DISIM, UnivAQ
Consorzio (altri) Dott. Pasquale Carianiello, DISIM, UnivAQ, ITDott. Subhasis Thakur, DISIM. UnivAQ, IN

Dott. Ing. Mario Gimenez De Lorenzo, dottorando DIIE, UnivAQ, IT

Referente GULP Giovanni De Gasperis

 

Titolo Progetto Engineering the POlicy-making LIfe CYcle
Acronimo ePolicy
Tipo di Progetto FP7 STREP
Anno di Inizio Progetto 2011
Anno di Fine Progetto 2014
Sito Web http://www.epolicy-project.eu
Abstract The e-Policy ProjectThe e-POLICY project is a FP7 STREP project funded under the Information and Communication Technologies (ICT) theme, Objective 5.6 ICT solutions for Governance and Policy Modeling.

Its main aim is to support policy makers in their decision process across a multi-disciplinary effort aimed at engineering the policy making life-cycle. For the first time, global and individual perspectives on the decision process are merged and integrated. The project focuses on regional planning and promotes the assessment of economic, social and environmental impacts during the policy making process (at both the global and individual levels). For the individual aspects, e-POLICY aims at deriving social impacts through opinion mining on e-participation data extracted from the web. To aid policy makers, citizens and stakeholders, e-POLICY heavily relies on visualization tools providing an easy access to data, impacts and political choices.

The ePolicy case study is the Emilia Romagna Regional Energy plan. ePolicy will provide a tool for supporting regional planners to create an energy plan that is in line with strategic EU and national objectives, consistent with financial and territorial constraints, partecipated including opinion mining results, well assessed from an environmental perspective and optimal with respect to one or more metrics. In addition to the regional plan, ePolicy will provide a portfolio of implementation instruments (namely fiscal incentives, tax exemption, investment grants) for pushing the society and the energy market to go in the direction envisaged by the plan.

Contributo della Programmazione Logica Programmazione Logica a Vincoli
Consorzio (affiliati GULP) Università di BolognaUniversità di Ferrara
Consorzio (altri) University College Cork (Ireland)The University of Surrey (UK)

INESC Porto Instituto De Engenharia De Sistemas E Computadores Do Porto (Portugal)

Fraunhofer Institute for Computer Graphics Research (Germany)

Regione Emilia Romagna (Italy)

PPA Energy (UK)

ASTER (Italy)

Referente GULP Marco Gavanelli
Budget 3,27M

 

Titolo Progetto Nuova architettura parallela per l’esecuzione di Programmi Logici mediante General Purpose Graphic Processing Unit (GPGPU)
Tipo di Progetto INDAM-GNCS
Anno di Inizio Progetto 2011
Anno di Fine Progetto 2011
Sito Web http://clp.dimi.uniud.it/projects/
Abstract Scopo del progetto e’ studiare le potenzialita delle architetture dicalcolo parallelo offrte dalle moderne GPGPU e di identificare parti dei motori Prolog e risolutori CLP(FD) e ASP che si prestano ad una parallelizzazione su tali architetture. Si pongono tre obiettivi principali:

1) offrire una versione di Prolog o ASP che utilizzi in modo trasparente e

nativo le caratteristiche parallele di schede grafiche

2) studiare e re-implementare gli algoritmi alla base dei sistemi Prolog,

CLP e ASP, basando il modello di calcolo sulla presenza di una architettura di tipo CUDA o OpenCL

3) studio di scenari applicativi concreti e di dimensioni realistiche: la predizione di struttura tridimensionale di proteine mediante CLP(FD), linguaggi per il planning riconducibili ad ASP e CLP.

Contributo della Programmazione Logica CLPCLP(FD)

ASP

SLD-risoluzione

Consorzio (affiliati GULP) Alessandro Dal Palu’Gianfranco Rossi

Andrea Formisano

Agostino Dovier

Consorzio (altri) Enrico Pontelli – USA
Referente GULP Alessandro Dal Palu’

 

Titolo Progetto Business Innovation in Virtual Enterprise Environments
Acronimo BIVEE
Tipo di Progetto Seventh Framework Programme (FP7) FoF-ICT-2011.7.3 (Virtual Factories and enterprises)
Anno di Inizio Progetto 2011
Anno di Fine Progetto 2015
Sito Web http://bivee.eu/
Abstract European industry, particularly the manufacturing industry, needs a boost in order to compete with the challenge presented by the globalised markets. Continuous production improvement and innovation need to become a ?natural? attitude of European enterprises.European industrial system is characterized by a large majority of SMEs (small and medium enterprises), to innovate and compete they need to rally in business ecosystems and operate as networked, virtual enterprises. Rallying the forces is a must when SMEs address innovation, since individually they lack the necessary critical mass.

The Bivee project ? Business Innovation in Virtual Enterprise Environments ? proposes an integrated Software Environment aimed at promoting and supporting production improvement and enterprise innovation for networked SMEs and virtual enterprises.

The Bivee Environment includes advanced methods for boosting creativity and innovation with an open approach, for supporting their lean implementation, for monitoring the concrete outcomes, managing the innovation ventures in a collaborative networked industrial setting, for creating shared knowledge repositories, leveraging on the collective intelligence of the communities.

Tools being developed by Bivee will model the existing environment, create a playground where ideas creation is encouraged, nurtured, and validated, providing also a testing ground to prove new ideas.

Contributo della Programmazione Logica Logic-based modeling and verification of Business Processes;Rule-based ontological reasoning
Consorzio (affiliati GULP) CNR-IASI – Institute for Systems Analysis and Computer Science
Consorzio (altri) Engineering (Italy, Coordinator)BIBA ? Bremer Institut Für Produktion und Logistik (Germany)

BOC Asset Management (Austria)

ATOS (Spain)

SRDC ? Yazilim Arastirma ve Gelistirme ve Danismanlik Ticaret (Turkey)

UNIVPM ? Università Politecnica delle Marche (Italy)

CNR-IASI – Institute for Systems Analysis and Computer Science (Italy)

AIDIMA ? Asociación de Investigación y Desarrollo de La Industria del Mueble y Afines (Spain)

Loccioni (Italy)

Referente GULP Maurizio Proietti

 

Titolo Progetto MAS-DALI per la robotica virtuale
Tipo di Progetto Interno
Anno di Inizio Progetto 2012
Anno di Fine Progetto
Sito Web http://www.disim.univaq.it
Abstract Il progetto vuole esplorare le applicazioni nel campo della robotica cognitiva del framework ad agenti DALI, interfacciando via rete i sistemi multi agente con ambienti di simulazione di robotica virtuale e/o mondi virtuali, intregrando moduli di elaborazione sub-simbolici.
Contributo della Programmazione Logica Complex Event ProcessingFIPA message passing tramite lo spazio di tuple

Controllo distribuito

Metainterpreti

Generazione e verifica di regole tramite metodi induttivi.

Consorzio (affiliati GULP) Dott. Ing. Giovanni De Gasperis, DISIM, UnivAQProf. Stefania Costantini, DISIM, UnivAQ
Consorzio (altri) Dott. Pasquale Caianiello, DISIM, UnivAQ, ITDott. Subhasis Thakur, DISIM, UnivAQ, IN

Dott. Giulio Nazzicone, dottorando DISIM. UnivAQ, IT

Referente GULP Giovanni De Gasperis

 

Titolo Progetto Scalable End User Access to Big Data
Acronimo Optique
Tipo di Progetto FP7, IP, ICT Call 3
Anno di Inizio Progetto 2012
Anno di Fine Progetto 2016
Sito Web http://www.optique-project.eu
Abstract Scalable end-user access to Big Data is critical for effective data analysis and value creation. Optique will bring about a paradigm shift for data access by* providing a semantic end-to-end connection between users and data sources;

* enabling users to rapidly formulate intuitive queries using familiar vocabularies and conceptualizations;

* seamlessly integrating data spread across multiple distributed data sources, including streaming sources;

* exploiting massive parallelism for scalability far beyond traditional RDBMSs

and thus reducing the turnaround time for information requests to minutes rather than days.

These objectives will be achieved by bringing together leading experts and cutting edge technology from diverse communities to develop an extensible platform that will provide a complete and generic solution to the data access challenges posed by Big Data.

The platform will: (i) Use an ontology and declarative mappings to capture user conceptualisations and to transform user queries into complete, correct and highly optimised queries over the data sources; (ii) Integrate distributed heterogeneous sources, including streams; (iii) Exploit massively parallel technologies and holistic optimisations to maximise performance; (iv) Include tools to support query formulation and ontology and mapping management; (v) Use semi-automatic bootstrapping of ontologies and mappings and query driven ontology construction to minimise installation overhead.

Development of the platform will be informed by and continuously evaluated against the requirements of complex real-world challenges, with two large European companies providing the project with comprehensive use cases, and access to user groups and TB scale data sets.

Experience from the use case deployments will be used to develop high quality tutoring and training resources, and to engage in an aggressive dissemination and exploitation program aimed at achieving the widest possible uptake of Optique technology.

Contributo della Programmazione Logica Tecniche di riscrittura di query congiuntive rispetto ad ontologie OWL 2 QL, usando rappresentazioni intermedie in Datalog.Riscrittura di query congiuntive rispetto a mapping, usando tecniche ispirate alla valutazione parziale di programmi logici.

Estensione del framework per gestire regole con con ritorsione lineare.

Consorzio (affiliati GULP) Free University of Bozen-BolzanoSapienza Università di Roma
Consorzio (altri) University of Oslo – NorvegiaSiemens AG – Germania

Statoil ASA – Norvegia

fluid Operations AG – Germania

Det Norske Veritas – Norvegia

University of Oxford – Regno Unito

Technische Universität Hamburg-Harburg – Germania

National and Kapodistrian University of Athens – Grecia

Referente GULP Diego Calvanese
Budget 14M

 

Titolo Progetto Dimostratore MAS-DALI nel Sistema Informativo Aerospaziale di CIRA
Acronimo MAS-SIA
Tipo di Progetto Consulenza
Anno di Inizio Progetto 2013
Anno di Fine Progetto 2014
Sito Web http://sia.cira.it
Abstract Il dimostratore MAS-DALI-SIA, nell’ambito del progetto CIRA-SIA, vuole dimostrare la fattibilità dello sviluppo di un sistema multi agente dedicato all’information retrieval sviluppato tramite il framework ad agenti DALI. Il codice degli agenti dell’implementazione finale e una versione ingegnerizzata ed estesa del framework DALI sono forniti dal gruppo di ricerca AAAI del Dipartimento di Ingegneria e Scienze dell’Informazione e Matematica dell’Università degli Studi dell’Aquila nell’ambito del rapporto di consulenza al Centro di Ricerche Aerospaziali di Capua (CE).IL MAS-SIA è composto da una comunità di agenti DALI cooperativi, ciascuno dedicato ad un compito in un contesto convenzionale di information retrieval (file indexer, tokenizer, query manager, document manager, etc…) che scambiano messaggi asincroni per tenere continuamente indicizzato una base testuale non strutturata sulla base di eventi di aggiunta e cancellazione di file. Il sistema finale si presenta come una applicazione web client/server, corredato di una interfaccia utente HTML5/Javascript che permette alll’utente finale di attivare/disattivare il MAS, l’invio di query interrogazione e la visualizzazione dei risultati, oltre che monitorare i messaggi FIPA che gli agenti scambiano durante il funzionamento.

Un server Python/twisted è stato sviluppato lato server per la meta-gestione del MAS e la traduzione dei messaggi FIPA/JSON direttamente visualizzabili sull’interfaccia web.

Contributo della Programmazione Logica Logic Agent Programming through the DALI Prolog-based frameworkComplex Event Processing

FIPA message passing through tuple space

Consorzio (affiliati GULP) Prof. Stefania Costantini, DISIM, UnivAQDott. Ing. Giovanni De Gasperis, DISIM, UnivAQ
Consorzio (altri) CIRA, ITDott. Suhasis Thakur, DISIM, UnivAQ, IN

Dott. Giulio Nazzicone, dottorando DISIM, UnivAQ, IT

Referente GULP Stefania Costantini

 

Titolo Progetto Progetto regionale FVG 2013: Sviluppo di un simulatore per la modellizzazione e il dimensionamento di sistemi energetici
Tipo di Progetto Progetto Regione FVG
Anno di Inizio Progetto 2013
Anno di Fine Progetto 2014
Sito Web http://clp.dimi.uniud.it/projects/
Contributo della Programmazione Logica Realizzazione di un prototipo in CLP per il calcolo del risparmio energetico ottenuto in seguito ad installazione di pannelli fotovoltaici, pompe di calore, e accumulatori, che include un suggerimento d’uso razionale degli elettrodomestici.
Consorzio (affiliati GULP) Università di Udine, DIMI
Referente GULP Agostino Dovier

 

Titolo Progetto Verifica di Programmi Imperativi mediante Trasformazione di Programmi Logici con Vincoli
Tipo di Progetto INDAM-GNCS Progetto Giovani Ricercatori
Anno di Inizio Progetto 2013
Anno di Fine Progetto 2014
Sito Web https://www.altamatematica.it/gncs/sites/www.altamatematica.it.gncs/files/ProgettiGR.pdf
Abstract La programmazione logica con vincoli, grazie alla sua potenza espressiva, è stata largamente impiegata come formalismo per codificare programmi e specificarne le proprietà da provare. Inoltre, come ampiamente illustrato in letteratura, la trasformazione dei programmi, cioè la manipolazione sintattica del codice sorgente del programma che ne preserva la semantica, può essere utilizzata come strumento per condurre deduzioni formali nell?ambito di teorie logiche e quindi può essere convenientemente utilizzata per l?analisi dei programmi imperativi. Per tali motivi la trasformazione di programmi logici con vincoli è stata utilizzata per definire un framework per la verifica automatica di programmi imperativi.
Contributo della Programmazione Logica Programmazione logica con vincoliTrasformazione di programmi logici con vincoli
Referente GULP Emanuele De Angelis
Budget 1200

 

Titolo Progetto CUD@ASP: sfruttare la potenza di calcolo delle GPU per il ragionamento automatico
Acronimo CUD@ASP
Tipo di Progetto INDAM-GNCS
Anno di Inizio Progetto 2014
Anno di Fine Progetto 2014
Sito Web http://clp.dimi.uniud.it/projects/
Abstract Il paradigma di programmazione dell’Answer Set Programming si e` fatto strada tra i paradigmi adatti a rappresentare conoscenza in domini complessi e al ragionamento su di essa. Tale paradigma contempla sia regole di senso comune sia la gestione di aspetti non monotoni del ragionamento. Parte del successo dell’ASP deriva dalla estrema efficienza dimostrata da alcuni dei risolutori disponibili, quale ad esempio clasp, sviluppato all’Universita` di Potsdam.Nel progetto vogliamo portare l’esperienza maturata dai membri del gruppo nell’impiego di GPU nel SAT solving e nel CSP solving, nel contesto dell’Answer Set Programming al fine di realizzare una versione GPU-based di un solver ASP. La disponibilita` di un tale solver, parallelo e ad alta efficienza, avrebbe notevoli ricadute in tutti gli ambiti in cui ASP rappresenta il motore inferenziale alla base del ragionamento automatico. Gli esempi sono numerosi, ci limitiamo a menzionare le applicazioni esistenti a planning, scheduling, problem solving, configurazione di prodotto, phylogenetic tree reconstruction, haplotype inference, biological networks inference e modeling, ragionamento su ontologie, semantic web, ecc…
Contributo della Programmazione Logica Answer set programmingConstraint logic programming

Constraint programming,

Conflict-driven learning

SAT-solving techniques

Consorzio (affiliati GULP) Università di PerugiaUniversità di Udine

Università di Parma

Alessandro Dal Palu’

Agostino Dovier

Andrea Formisano

Raffaella Gentilini

Flavio Vella

Referente GULP Andrea Formisano
Budget 3500

 

Titolo Progetto Metodi di verifica formale del software basati su trasformazioni di programmi logici con vincoli
Tipo di Progetto INDAM-GNCS
Anno di Inizio Progetto 2014
Anno di Fine Progetto 2015
Abstract Il progetto si propone di estendere il metodo di verifica trasformazionale basato su programmazione logica con vincoli che è stato applicato con successo ai programmi imperativi con interi ed array.L’obiettivo è di estendere la classe di programmi imperativi trattati permettendo, ad esempio, l’uso di strutture dati dinamiche, quali liste o puntatori. A tal proposito si intende usare il linguaggio CHR (Constraint Handling Rules) per codificare ed implementare gli assiomi della teoria dei vincoli considerata.
Contributo della Programmazione Logica Trasformazione di programmi logici con vincoliCHR (Constraint Handling Rules)

Verifica di programmi

Consorzio (affiliati GULP) CNR-IASI – Institute for Systems Analysis and Computer ScienceUniversità “G. d’Annunzio” di Chieti-Pescara

Università di Roma “Tor Vergata”

Referente GULP Fabio Fioravanti
Budget 4000

 

Titolo Progetto Constraint-Based Search using GPUs and applications to protein structure prediction
Tipo di Progetto INDAM-GNCS
Anno di Inizio Progetto 2015
Anno di Fine Progetto 2015
Sito Web http://clp.dimi.uniud.it/projects/
Abstract Negli ultimi anni la diffusione delle General-Purpose Graphics Processing Units (in breve, GPU) sia come supporto hardware presente nella stragrande maggioranza degli attuali calcolatori (fissi e portatili) che come scheda aggiuntiva capace di offrire un alto grado di parallelismo a basso costo, ha spinto ricercatori di varie discipline ad esplorarne le potenzialità per gli scopi di loro interesse. Dal 2012 il gruppo dei proponenti ha presentato, in lavori su atti di convegno e riviste, diversi contributi per sfruttare le GPU per la ricerca di soluzioni in problemi vincolati, dapprima affrontando la risoluzione del problema SAT, proseguendo nella direzione di sviluppare un, più generale, ASP solver, per arrivare alla definizione di un constraint solver. In questo contesto, la GPU si è mostrata estremamente efficiente per la ricerca approssimata di soluzioni con tecniche di Large Neighborhood Search (LNS) e promettente per la parallelizzazione degli algoritmi di propagazione di vincoli complessi (denominati vincoli globali). La generalità e la capacità di manipolazione numerica di un constraint solver permette una agevole codifica del problema della predizione di una proteina e la tecnica di LNS si è mostrata particolarmente adatta alla rapida predizione di strutture sub-ottime.Il presente progetto si articolerà principalmente ma non esclusivamente nelle seguenti tre direttive principali

1. studio ed implementazione parallela di algoritmi per la propagazione di vincoli globali complessi

2. testing delle implementazioni di cui al punto sopra sui benchmarks della Minizinc challenge, competizione annuale dei constraint solver

3. testing e tuning delle implementazioni di cui sopra in varianti del problema del protein structure prediction (loop modeling, protein insertion, docking, etc)

Contributo della Programmazione Logica Sviluppo di constraint solverModeling in Minizinc
Consorzio (affiliati GULP) Università di Udine, DIMI
Referente GULP Agostino Dovier

 

Titolo Progetto Generazione automatica delle asserzioni per la verifica di programmi da semantiche formali
Tipo di Progetto INDAM-GNCS
Anno di Inizio Progetto 2015
Anno di Fine Progetto 2016
Abstract Lo sviluppo di metodi formali per la verifica del software è una delle applicazioni più rilevanti della logica matematica, in quanto consente di ottenere in modo automatizzato garanzie che un sistema software sia aderente alle specifiche. Un passo preliminare nelle tecniche di verifica di un programma consiste nella generazione di formule logiche la cui soddisfacibilità implica la correttezza del programma. Nelle tecniche attualmente più diffuse questo passo preliminare viene realizzato per mezzo di algoritmi ad-hoc.Questo progetto si propone di sviluppare un metodo per generare automaticamente le condizioni che assicurano la correttezza di un programma a partire dalla specifica formale della semantica del linguaggio di programmazione e della logica in cui è espressa la proprietà da verificare. Tali condizioni di verifica possono poi essere fornite in input a sistemi che provano, in modo parzialmente automatizzato, la loro soddisfacibilità e, quindi, la correttezza del programma.

Il metodo proposto è basato su trasformazioni delle formule che rappresentano la semantica e la proprietà da verificare. Un vantaggio essenziale del metodo trasformazionale è che esso permette di generare condizioni di verifica in modo parametrico rispetto alla semantica, senza richiedere dimostrazioni ad-hoc di correttezza, che è assicurata dall’uso di opportune regole di trasformazione.

Verranno esplorati diversi aspetti del metodo proposto, prendendo in considerazione vari linguaggi e vari costrutti di programmazione, vari stili di specifica formale della semantica del linguaggio, varie classi di proprietà di correttezza dei programmi e varie strategie di trasformazione. Infine, verrà implementato un framework per la generazione delle condizioni di verifica basato sul metodo di trasformazione e verranno sviluppati diversi casi di studio per valutarne sperimentalmente l’efficacia.

Contributo della Programmazione Logica Trasformazione di programmi logici con vincoliMetaprogrammazione
Consorzio (affiliati GULP) CNR-IASI – Institute for Systems Analysis and Computer ScienceUniversità “G. d’Annunzio” di Chieti-Pescara

Università di Roma “Tor Vergata”

Referente GULP Maurizio Proietti
Budget 4800

 

Titolo Progetto Aplicacion de programacion logica de restricciones conjuntistas a la validacion y verificacion de software (Applicazione della programmazione logica con vincoli insiemistici alla validazione e verifica del software)
Tipo di Progetto Progetto finanziato da Fondo para la Investigación Científica y Tecnológica (FONCyT), Argentina.
Anno di Inizio Progetto 2015 (attualmente in fase di valutazione)
Anno di Fine Progetto 2018
Abstract Il progetto si pone i seguenti obiettivi: automatizzare la generazione di prototipi funzionali a partire da specifiche basate sulla teoria degli insiemi; utilizzare la programmazione logica con vincoli insiemistici come base per la generazione automatica di prototipi e per la generazione di casi di test; estendere la programmazione logica con vincoli insiemistici alle funzioni parziali, funzioni totali, relazioni binarie e sequenze; integrare la programmazione logica con vincoli insiemistici con CLP(Q,R); validare empiricamente le soluzioni proposte.
Contributo della Programmazione Logica Programmazione Logica a Vincoli (CLP)Vincoli insiemistici

Sviluppo di applicazioni grafiche in Prolog tramite XPCE

Consorzio (affiliati GULP) Gianfranco RossiDipartimento di Matematica e Informatica, Università di Parma
Consorzio (altri) Maximiliano Cristià (responsabile del progetto)Universidad Nacional de Rosario e Centro Internacional Franco-Argentino de

Ciencias de la Informacion y de Sistemas (CIFASIS)

Claudia Frydman

Aix-Marseille Universite’, Francia

Referente GULP Gianfranco Rossi