VSTTE 2026

Esperienza

Troppa grazia Sant’Antonio

Prima di questo dottorato, non sono mai stato una persona che viaggia parecchio. Persino adesso, si contano su un paio di dita le volte che mi sono avventurato in qualcosa che sia definibile come tale di mia spontanea volontà. Il mio piano di obbligarmi ad esplorare luoghi a me ignoti dietro l’inattaccabile motivazione lavorativa sembra avere prodotto i frutti desiderati, e poiché la fame vien mangiando, adesso mi trovo molto più a mio agio a muovermi autonomamente, percorrendo anche distanze non banali. È anche grazie a questa maturata propensione che recentemente ho deciso di passare qualche giorno da mia sorella, a Trieste.
Peccato che ho scoperto troppo tardi, dopo che tutti i preparativi erano già stati ultimati, che il nostro paper ‘Verified Linear Programming through Tolerance-Aware Precision Boosting’ era stato accettato a VSTTE, motivo per cui mi sarei ritrovato a passare da quelle zone per una seconda volta in pochissimo tempo. Sarebbe stato molto piacevole organizzare un viaggio più lungo che riunisse entrambe queste escursioni (e che mi avrebbe risparmiato ben due voli), ma poco male. Una chance in più per esplorare una regione che mi aveva già lasciato un’ottima impressione.
Purtroppo la mia destinazione, Graz, non ha un aeroporto particolarmente connesso, per cui la mia unica opzione è stata arrivare a Edimburgo, atterrare a Vienna e infine raggiungere Graz tramite un Flixbus. A causa degli orari non proprio comodissimi, ho raggiungo il mio albergo alle 3 di notte, ma almeno nulla si è inceppato nel processo, per cui sono arrivato stanco, ma sano e salvo, e non ho passato la notte in aeroporto, opzione che avevo considerato. Inoltre, la passeggiata notturna, con una leggera pioggerellina ad arricchire lo scenario, mi ha regalato uno scorcio raro di una città addormentata e quieta, foderata con un silenzio tranquillo e lo-fi.

La conferenza

La mia esperienza relativa alla partecipazione a conferenze dal vivo è estremamente limitata. Il mio ricordo relativamente recente di AAAI26 messo a confronto con ciò che ho trovato all’università di Graz mi ha spiazzato. Invece delle centinaia, se non migliaia, di persone che popolano ogni angolo di una struttura per convegni sterminata, ci siamo trovati tutti in una piccola aula universitaria ad ascoltare raccolti le presentazione degli altri presenti. Dovrei precisare che VSTTE è una conferenza ospite di FMCAD, che probabilmente la supera in termini di partecipazione.
In compenso, avere a che fare con al più una cinquantina di persone ha l’enorme vantaggio di creare un ambiente molto più familiare e accogliente. Persino per me, non esattamente un individuo che definirei estroverso, non è stato difficile scambiare quattro chiacchiere con buona parte delle persone che ho incontrato.

Mi permetto anche una frecciatina evidenziando che, ai miei occhi, anche l’ambito di ricerca ha un ruolo piuttosto importante sull’atmosfera che si respira. A AAAI26 ho chiaramente percepito una forte pressione, quasi tensione, aleggiare nell’aria, probabilmente alimentata dalla fretta e competizione che caratterizza l’ambito AI, dove la velocità e quantità di pubblicazione ha sempre la precedenza su qualsiasi altra metrica. L’atmosfera a VSTTE, invece, mi è sembrata molto più rilassata, collaborativa, quasi familiare. Sicuramente mi trovo molto più a mio agio in quest’ultimo tipo di ambiente.

La prima giornata

La prima giornata è stata caratterizzata dalla presentazione dei paper che sono stati accettati alla conferenza. C’è stata una grande varietà di temi trattati, ma ho notato un grande focus sui dettagli implementativi, anche se spesso descritti solo ad alto livello. Questo approccio si contrappone alla mia tendenza di mostrare solo i risultati, sorvolando sui passaggi che li hanno prodotti, spendendo invece quel tempo a descrivere il contesto e i preliminari, nella speranza che ciò sia sufficiente a permettere ai miei spettatori di seguire agevolmente la spiegazione. Forse, però, dovrei prendere un po’ più di spunto.
In ogni caso, alle 16 in punto, con una precisione più svizzera che austriaca, è stato il mio turno. È filato tutto sorprendentemente liscio. Non mi sono impappinato, sono rientrato pienamente nei tempi previsti e, soprattutto, ho percepito un certo interesse generale nel pubblico. Anche le domande sono state relativamente tante (almeno per la media che avevo osservato) e molto mirate, nonostante l’ora piuttosto tarda. Sembra che, contrariamente alle mie aspettative, lo strumento che ho pubblicizzato sia qualcosa di appetibile nell’ambito della verifica formale, ma che poche persone conoscono, probabilmente perché i software di verifica che vengono usati sono spesso visti come black box, ignorando tutti i dettagli e miriade di componenti che, insieme, producono le funzionalità che il software offre.

Prima che potessi ritirarmi a vita privata nel mio hotel, sono stato intercettato e convinto ad andare a cena con un gruppo di colleghi conosciuti al volo. Abbiamo addirittura avuto la fortuna di scegliere il ristorante giusto in cui fermarci, e abbiamo passato una stupenda serata condividendo esperienze e aneddoti.

La seconda giornata

La seconda giornata è stata molto più leggera. Ho seguito i due tutorial sul programma. Il primo era relativo alla verifica formale di circuiti utilizzando una formulazione algebrica. Da persona più legata al mondo degli SMT, mi è sembrato un modo incredibilmente complicato per fare ciò che un SAT solver, anche se sono sicuro di non essere riuscito a cogliere tutte le sottili e complesse motivazioni che giustificano questa scelta per nulla banale. Il secondo era una sessione hands-on su Marabu, un tool per la verifica di Deep Neural Networks. Era il momento che aspettavo di più, poiché ho avuto a che fare con il loro software in passato, prendendone ispirazione nel tentativo di integrare qualcosa di simile nelle versioni più arcaiche di dLinear. Dopo la sua sessione, mi sono unito a lui e a un altro ricercatore particolarmente interessato all’argomento e abbiamo pranzato insieme, continuando a discutere i dettagli di ognuno dei nostri progetti. Suona molto strano detto da me, ma posso intravedere una possibile collaborazione in un futuro non troppo distante, ammesso che i progetti a cui sto lavorando al momento raggiungano un livello soddisfacente di completamento.

Una graziosa esplorazione

Adempiuti i miei doveri, ho sfruttato il poco tempo che mi rimaneva in città per esplorarla. Graz mi è piaciuta parecchio: mi sembra una città molto graziosa, con una lunga ed importante storia che è riuscita a conservare quasi intatta per tutto questo tempo. Un patrimonio culturale che ora restituisce ai suoi abitanti e a chi vi soggiorna. È molto piacevole passeggiare per le vie del centro, che rimane molto a misura d’uomo, fra i suoi meravigliosi edifici storici, le molte aree pedonali e i parchi verdi. Persino da un punto di vista commerciale, Graz è molto vivace, con tanti negozietti di grandi marche sparsi dovunque.
C’è una chiara attenzione nei confronti dell’arte che mi sembra ancora più integrata nel tessuto cittadino di quanto avevo già osservato a Lubiana. E poi Graz ha un fiume, la cui presenza, inizio a sospettare, è strettamente correlata con il mio apprezzamento della location.

Verso le 18:30 mi sono unito al tour della città incluso nella conferenza. Un’ottima occasione per scoprire i retroscena storici dietro i luoghi più caratteristici di Graz.

Conscio che il giorno dopo avrei abbandonato Graz nel giro di un’oretta, ho avuto la simpatica idea di salire fino alla torre dell’orologio che sovrasta la città alle 10 di notte. Ne è valsa la pena: ho esplorato le gallerie scavate nella roccia della collina su cui si erge e ho potuto ammirare le luci della città dal suo punto più alto.

Tirando le somme, i luoghi più significativi che ho visitato sono stati:

• L’università
• Il mausoleo di Federico II
• La cattedrale
• I parco cittadino
• Le scale a doppia elica
• La piazza dell’orologio
• Il fiume Mur
• La torre dell’orologio

In the sbrucs

Piuttosto che tornare a Vienna per poi dirigermi a Londra, ho deciso di sfruttare la mia presenza in Austria per pernottare un giorno a casa di amici, ad Innsbruck. Certo, sarebbe stato molto più semplice se le ore di treno che separano Graz dalla mia destinazione non fossero state quasi 6. Pazienza, un’occasione simile non mi ricapiterà facilmente, ed era già da un po’ che avevo in mente una gita del genere. In mattinata ho raggiunto la stazione centrale di Graz e ho preso il treno per Innsbruck. Anche se il viaggio è stato davvero lungo, non mi è pesato particolarmente: il treno è estremamente comodo, con un sacco di spazio fra i sedili, e la vista era a dir poco mozzafiato, con le montagne che seguono da lontano, inamovibili, con il loro sguardo, il nostro minuscolo convoglio sfrecciare fra le valli disegnate dalle loro imponenti figure.

Parecchi anni fa, il tempo in treno sarebbe apparso infinito, ma adesso, se non altro, anche 6 ore volano senza difficoltà. In men che non si dica ero alla stazione di Innsbruck, piuttosto asettica e minimale. Informato il mio contatto, inizio ad andargli incontro. Gli edifici intorno alla stazione le somigliano: non si tratta di strutture storiche e colorate, ma palazzoni squadrati e grigi. Dopo aver lasciato i miei averi a casa per non farmi appesantire durante la nostra esplorazione, ci siamo diretti verso il centro storico. Superato l’arco di trionfo con tutti i rilievi degli imperatori austriaci più importanti che si staglia in mezzo alla strada abbiamo raggiunto la zona più vecchia della città. Lo stile degli edifici è cambiato radicalmente e si è allineato a quanto visto a Graz: palazzi con una media di due o tre piani, intonacati di colori diversi e spesso decorati da piccoli ghirigori, colonne disegnate o piccoli mosaici, veri o dipinti. Gli edifici più importanti ed alti spesso sono sormontati da una cupola più o meno appuntita di rame, ormai reso verdognolo dall’esposizione alle intemperie e conseguente ossidazioni. Un colore che sembra volersi omologare a quello di sfondo. Camminando verso nord, infatti, la strada si dischiudeva a passo d’uomo, dando sempre più spazio alle montagne alle sue spalle. Mentre a Lubiana i rilievi sono lontani, come un dettaglio di sfondo appena abbozzato in un sogno lucido, a Innsbruck i monti compaiono all’improvviso ogni qualvolta lo sguardo non è bruscamente interrotto da qualcosa costruito dall’uomo. Sembra sufficiente tendere la mano per accarezzarne i pendii verdi e morbidi.

Ci siamo diretti verso uno dei simboli più importanti della città: un balconcino con le tegole dorate incastonato in uno degli edifici che formano la piazza nel cuore del paese. Il colpo d’occhio non è male, con tanto di decorazioni che impreziosiscono l’opera, ma condivido l’opinione che i locali sembrano avere: grazioso, ma non certo chissà quale capolavoro. Molto più di valore, invece, è l’area che lo circonda.

In quel cunicolo di vicoli e stradine si respira l’aria di un tempo ormai andato, e, vagabondando nel dedalo di possibilità, è possibile scoprire alcune gemme carine, da negozi di carte molto ben forniti a duomi che, pur avendo un’unica navata, la sfruttano al massimo per apparire imponenti come cattedrali.

Sorpresi da un principio di pioggia, ci siamo dedicati a saziare il nostro appetito con una porzione di Spätzle, una versione molto più raffinata e molto saporita dell’americano Mac & Cheese. Il nostro piano di attendere che il meteo divenisse più clemente ci si è presto ritorto contro. Dopo un iniziale miglioramento, che abbiamo sfruttato per raggiungere la biblioteca universitaria ed visitare brevemente la parte della città dall’altra parte del fiume Inn, la leggera pioggerellina a cui sono ormai abituato si è trasformata in un rovescio a tutti gli effetti. Il tragitto di ritorno è stato molto più bagnato del previsto.
Il giorno dopo, delle campane dal suono particolarmente intenso si sono assicurate che non perdessi l’aereo hanno contribuito, svegliandoci alle 7 di mattino. Abbiamo fatto colazione con uno dei dolci tipici del luogo, e poi via, verso l’aeroporto. La procedura di imbarco è stata ancora più veloce di quanto avessi preventivato: ero letteralmente l’unica persona in fila per i controlli della sicurezza, che sono stati molto manuali. E così, poco tempo dopo, ero già in volo per tornare nel Regno Unito.

Impressioni

• Bagno separato in stanza toilette e stanza da bagno
• Molte informazioni sono tradotte in Tedesco, Inglese, e Italiano, ma spesso la lingua Tedesca è l’unica presente

Graz

• Grande orgoglio nel passato storico (che causa qualche complesso a causa del contrasto con la situazione attuale)
• Piuttosto silenziosa
• Non troppo accomodante per chi non parla Tedesco
• Una Torrevarata con negozi e palazzoni
• Atmosfera rilassata
• Tram che rimpiazzano gli autobus
• Cattedrale estremamente opulente
• Mezzi gratuiti nel centro città
• Facile da visitare camminando
• Niente Wi-Fi sui treni
• Vagone ristorante piuttosto elegante
• Le montagne e i paesaggi sembrano un po’ l’interno siciliano, ma con valli più spaziose e picchi più alti
• La sede del parlamento è facilmente accessibile, posizionata nei pressi di un cortile di fattura italiana

Innsbruck

• Tetti di rame ossidato
• Topologia compatta
• Biblioteca seriosa e stranamente carente in materie scientifiche
• Pista per il salto con gli sci
• Negozio storico di campane
• Le nuvole nascondono le cime delle montagne, sembra di essere isolati dal mondo esterno
• Assenza di una fumetteria come si deve
• Catacombe piuttosto vuote, con altare nascosto
• Duomo con unica navata
• Il municipio è in una galleria commerciale
• Aeroporto minuscolo, persino più piccolo di Fontanarossa
• Controllo del boarding pass fatto a mano
• Molti aerei non di linea che utilizzano la pista

Note

Side channels attacks

Side channels attack use information leaked by the implementation of a system, rather than weaknesses in the implemented algorithm itself. The example being provided is a side channel attack that can measure the variation in magnetic field generated by a CPU when computing some data. The key insight is that correlation is what gives your secret away. If there is any correlation between the data bing measured and the secret, then the attacker will be able to recover the secret. For this reason, you always want to encrypt your data, usually via a one-time-pad procedure, and then perform operations on the encrypted data.
This works well in theory, but in practice, even a simple program needs to load data on the register, making them prime targets for this kind of attacks. Hence we need to harden the implementation of the asssembly instructions

How is inteweaving some cycles between loads help?

Optimizing compiler optimization

We want to verified the optimization phase of the GraalVM compiler using Isabelle/HOL. While it is possible to verify the theoretical model of the optimizer, the issue is that then we need to prove that the implementation follows the specification. Therefore, they instead op to generate the compiler code (java) from the specification. GraalVM is a just-in-time compiler, hence optimization passes must be as fast as possible. Interesting, although very specific. Maybe it can be generalized to other compilers, but it is not clear how.

Chartreaux: Towrads verified

Dataflow analysis in kotlin Applies to a toy set language

What about typescript? Slide 22 : could we divide by 0?

Proving Minmax algorithm

Tree based algorithm. Witness? Explore multiple algorithms in dafne, find that there are some tree combinations that invalidate the witness.

Verified QBF solving in isaelle-HOL

QBF: Qnatified Boolean Formulas Verifying and generating the code for a QBF solver in SML. Seems to be extremely underperforming when compared to state-of-the-art solvers. Certificates Vs. Building a verified solver. Different Languages (Standard ML, Haskell, OCaml) produce a different performing code, even when generated by the same specification.

Measuring and including sematic entropy in LTL Guardrail generation

Perplexity: measure of a probability distribution for a given sequence of token. Sematic entropy measures the fact that the same answer can be given with different sentences, all sharing the same rough meaning. AWS Dogwood is a governance language designed for AI agents and their tool, and supports guardrails and LTL support.

Cluster entropy: Shannon entropy over candidate behaviors. How many different behaviors Marginal entropy: how much do the candidates disagree?

As a first pruning step we ask

• if the LTL realizable (can the LLM follow it)
• if the LTL is vacuous (any trace satisfies it)

Towards a standard intermediate language for software verification

Real-world languages are complex to verify Verification techniques are largely language-agnostic Factor out an intermediate language, so that you just verify that, and let the translation from the real-world language to the intermediate language be handled by a compiler.

Kratos2

Loading diagram...

What is the workflow of using Kratos2? How do I annotate error, live and notlive properties in the source code?

Smoke tests

We want to check fast common verification problems, which usually means vacuous verifications, wasted effort an dead code. VerCors is a deductive verifier for concurrent software. Support Java, C, opencl, cuda. Supports invariants, preconditions, postconditions, and assertions.

Formal verification of circuits (multipliers)

Decision diagrams SAT solvers Algebraic approach

Using the latter, we create a graph of multipliers, that translate to polynomials, which can then be verified by existing solvers. The product of the input sum should be equal to the weighted product of the inputs. For some reasons you use rationals instead of integers, just because it is easier from the theory point of view, although we just compute integers.

Given a pair of inputs, there are only for kinds of nodes:

AND, AND with left negation, AND with right negation, AND with both negated.

Loading diagram...

Computer algebra

It is possible to generate the ideal from a basis of polynomial, taking into account all the linear combinations of the basis polynomials.

It is interesting to answer the question: given an arbitrary polynomial, does it belong to the ideal? A Grobner basis is a set of polynomials that generates the same ideal, but has some nice properties that make it easier to answer the question above.

How to sort polynomials? In the general case, when we have multilinear polynomials with are not linear, we can use the lexicographic order.

Marabu

Alethe proof format. Can be applied to robotics, to show the limitation via counterexamples.

Diario di viaggio

• 13/09/2026
  • 15:24 Partenza del treno da Newcastle
  • 17:20 Arrivo a Edimburgo
  • 18:02 Arrivo all’aeroporto di Edimburgo
  • 18:18 Arrivo al terminal
  • 19:20 Decollo da Edimburgo
  • 22:35 Atterraggio a Vienna
  • 00:15 Partenza dall’aeroporto di Vienna
  • 02:45 Arrivo a Graz
  • 03:05 Arrivo in hotel
• 14/09/2026
  • 07:30 Sveglia
  • 08:30 Uscita dall’hotel
  • 09:00 Arrivo in università
  • 12:30 Pausa pranzo
  • 16:00 La mia presentazione
  • 18:05 Fine della prima giornata di conferenza
  • 19:00 Cena con i colleghi
  • 22:00 Rientro in hotel
• 15/09/2026
  • 07:30 Sveglia
  • 08:30 Uscita dall’hotel
  • 09:00 Arrivo in università
  • 12:30 Pausa pranzo
  • 12:35 Pausa pranzo
  • 13:30 Esplorazione della città
  • 18:30 Visita guidata
  • 20:30 Rientro in hotel
  • 22:00 Visita alla torre dell’orologio
  • 23:30 Rientro in hotel
• 16/09/2026
  • 08:00 Sveglia
  • 09:48 Partenza dalla stazione centrale di Graz
  • 15:40 Arrivo a Innsbruck
  • 16:30 Arrivo a casa
  • 17:00 Giro per il centro storico
  • 18:30 Cena
  • 19:30 Continuazione dell’esplorazione
  • 20:15 Ritorno a casa
• 17/09/2026
  • 07:00 Sveglia campanara
  • 08:30 Sveglia
  • 09:15 Partenza verso il centro
  • 09:45 Colazione
  • 10:21 Partenza bus
  • 10:35 Arrivo in aeroporto
  • 11:50 Decollo da Innsbruck
  • 12:40 Atterraggio a Londra
  • 20:30 Partenza da King’s Cross
  • 23:10 Arrivo a Newcastle