CHC-COMP 2023: Valutazione dei risolutori di Clausi Horn con vincoli

CHC-COMP 2023 ha segnato la sesta edizione della Competizione per Solutori di Constrained Horn Clauses (CHCs). Questa competizione si è svolta ad aprile 2023, con i risultati condivisi al 10° Workshop su Horn Clauses per Verifica e Sintesi a Parigi, Francia. L'evento ha presentato sette solutori, con sei partecipanti e uno presentato fuori concorso. I partecipanti hanno lavorato su sei diversi percorsi, ognuno focalizzato su un tipo specifico di CHC.

#Cosa sono le Constrained Horn Clauses?

Le Constrained Horn Clauses sono un tipo speciale di formula logica. Si basano sul formato tradizionale delle Horn clause aggiungendo vincoli. Questi vincoli possono provenire da varie teorie di base come aritmetica intera, array o tipi di dati. Le CHC sono ora ampiamente usate per la verifica automatica dei programmi, il che significa che aiutano a garantire che i programmi funzionino correttamente.

Negli ultimi dieci anni, sono stati fatti progressi significativi nello sviluppo di strumenti, noti come solutori CHC, che possono gestire queste clausole in modo efficiente. Questi solutori possono affrontare problemi di Soddisfacibilità, il che significa che possono determinare se esiste una soluzione per una certa affermazione logica.

#Scopo di CHC-COMP

L'obiettivo principale di CHC-COMP è valutare i migliori solutori CHC basati su Benchmark realistici che chiunque può accedere. La competizione incoraggia i contributi di sviluppatori, ricercatori e utenti interessati ai metodi di risoluzione delle CHC e alle loro applicazioni pratiche.

CHC-COMP 2023 si è svolta in connessione con il workshop menzionato prima. La scadenza per inviare i benchmark candidati era il 24 marzo 2023. I partecipanti avevano un breve periodo per inviare i loro strumenti e competere. Dopo due settimane di competizione, i risultati sono stati condivisi al workshop.

#Struttura della Competizione

La competizione ha permesso ai solutori partecipanti di competere in sei diversi percorsi. Ogni percorso trattava un diverso tipo di CHC. I percorsi erano progettati per valutare i solutori in base a vari criteri:

1. Teoria di Base: I diversi percorsi hanno utilizzato varie teorie sottostanti per valutare i solutori.
2. Numero di Atomi Non Interpretati: I percorsi erano categorizzati in base a quanti atomi (intesi come variabili o simboli) non erano interpretati nel contesto della teoria.

I tipi di clausole inclusi in questi percorsi erano CHC lineari e non lineari con vincoli applicati all'aritmetica intera, agli array e altri.

#Dettagli Tecnici

CHC-COMP 2023 ha utilizzato la piattaforma StarExec per condurre la competizione. StarExec ha fornito una coda dedicata di nodi equipaggiati con processori potenti per eseguire i solutori. Questo ha garantito che la competizione potesse elaborare un numero significativo di compiti contemporaneamente.

Prima della competizione, i team hanno partecipato a una prova per familiarizzare con la piattaforma e assicurarsi che i loro strumenti funzionassero correttamente. Questa fase di test ha permesso agli organizzatori di comunicare con i partecipanti su eventuali problemi emersi prima dell'inizio ufficiale della competizione.

La competizione principale è consistita in invii finali valutati rispetto a vari benchmark. Ogni lavoro aveva limiti specifici sul tempo CPU e sull'uso della memoria per garantire una competizione equa.

#Valutazione dei Solutori

I solutori sono stati giudicati in base a quanto bene hanno performato sui benchmark assegnati. Hanno ricevuto punteggi in base al numero di risultati che hanno identificato accuratamente come soddisfacenti o insoddisfacenti. Se i solutori restituivano risultati sconosciuti, questi erano meno favorevoli.

Nei casi in cui due solutori non concordavano sul risultato di un benchmark, gli organizzatori hanno preso nota dell'incoerenza e hanno informato i rispettivi team. I team hanno avuto l'opportunità di affrontare questi problemi se il tempo lo permetteva.

#Processo di Selezione dei Benchmark

La selezione dei benchmark per la competizione ha comportato diversi passaggi. Prima, i benchmark sono stati elaborati per assicurarsi che si conformassero al formato richiesto. Dopo la formattazione, i benchmark sono stati categorizzati nei sei percorsi in base alla loro complessità e ad altre caratteristiche.

Il processo di selezione mirava a creare un mix di benchmark "facili" e "difficili". I benchmark "facili" erano quelli che sia il solutore vincente che il secondo classificato hanno risolto velocemente. Ogni benchmark è stato valutato in base a quanto bene ha performato nelle competizioni precedenti per garantire una rappresentazione equa dei test disponibili.

#Invii dei Solutori

Sette solutori hanno partecipato a CHC-COMP 2023, con dettagli sulle loro configurazioni registrati dagli organizzatori della competizione. I solutori hanno utilizzato varie configurazioni adatte ai tipi specifici di clausole nei percorsi della competizione.

Inoltre, ci si aspettava che le performance di questi solutori variassero in base alle loro capacità e alla natura dei benchmark che affrontavano. La competizione ha offerto opportunità sia ai nuovi che ai solutori affermati di mostrare i loro punti di forza.

#Problemi Osservati e Soluzioni

Durante la competizione, sono stati identificati alcuni problemi riguardanti le prestazioni di certi solutori. Ad esempio, incoerenze nei risultati hanno portato a contattare i team e dare loro la possibilità di inviare correzioni. Gli organizzatori hanno lavorato a stretto contatto con questi team per garantire che le configurazioni difettose fossero corrette, mantenendo l'integrità competitiva.

Mantenendo la comunicazione aperta, molte discrepanze sono state risolte, portando a risultati più accurati.

#Risultati Finali

Alla conclusione della competizione, i vincitori sono stati annunciati in base alle loro performance complessive nei vari percorsi. Quest'anno, la competizione ha riconosciuto più vincitori in diverse categorie basate sulle loro specifiche capacità nel gestire le clausole presentate.

#Considerazioni Future

Guardando al futuro, gli organizzatori di CHC-COMP stanno considerando potenziali miglioramenti e cambiamenti per le edizioni future. Tra queste considerazioni ci sono:

1. Validazione dei Risultati: Assicurarsi che ogni solutore possa generare testimonianze o prove accurate a supporto dei propri risultati rimane una priorità.
2. Stato dei Benchmark: C'è bisogno che i benchmark dichiarino esplicitamente i risultati attesi. Questo aiuterà a valutare la correttezza dei risultati forniti dai solutori.
3. Percorsi Paralleli: Un'idea di consentire l'elaborazione parallela per specifici percorsi potrebbe migliorare la dinamica della competizione e offrire nuove sfide per i partecipanti.
4. Contributi ai Benchmark Migliorati: Gli organizzatori incoraggiano i contributi della comunità per espandere i set di benchmark disponibili per le future competizioni.

#Conclusione

CHC-COMP 2023 ha valutato con successo e messo in mostra i progressi nel campo della risoluzione delle CHC. L'evento ha evidenziato l'importanza della collaborazione tra ricercatori e sviluppatori, fornendo una piattaforma per lo sviluppo continuo nell'area della verifica dei programmi. Con feedback preziosi dai partecipanti e le lezioni apprese durante questa edizione, le future competizioni possono costruire su questa base per un successo ancora maggiore.

Man mano che la competizione continua a crescere, il coinvolgimento dei membri della comunità e il contributo di nuovi benchmark saranno essenziali per guidare l'innovazione e migliorare le tecnologie dei solutori. La comunità CHC guarda con attesa alla prossima edizione, ansiosa di vedere come il campo si evolverà ulteriormente.