BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Date iCal//NONSGML kigkonsult.se iCalcreator 2.20.2//
METHOD:PUBLISH
X-WR-CALNAME;VALUE=TEXT:Eventi DIAG
BEGIN:VTIMEZONE
TZID:Europe/Paris
BEGIN:STANDARD
DTSTART:20261025T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
BEGIN:DAYLIGHT
DTSTART:20260329T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20270328T020000
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:calendar.31566.field_data.0@www.diag.uniroma1.it
DTSTAMP:20261019T152459Z
CREATED:20261005T103410Z
DESCRIPTION:Abstract: The deployment of large language models in high-stake
 s domains demands infrastructure for trusting AI-generated outputs whose r
 easoning is opaque and possibly beyond human comprehension. This talk intr
 oduces Proof-Carrying Output (PCO)\, a framework in which an AI system ret
 urns an answer accompanied by a machine-checkable proof of compliance with
  a published\, decidable specification. The proofs rely on established pro
 of assistants such as Rocq (Coq) for symbolic reasoning and on temporal lo
 gics (LTL\, STL) for time-dependent properties. On top of proof checking\,
  PCO adds a cryptographic accountability layer that binds the output\, its
  proof\, the validator version\, and a trusted timestamp into a non-repudi
 able commitment on an append-only ledger before the output is acted upon\,
  yielding binding\, hiding\, temporal ordering\, and audit correctness. We
  demonstrate PCO through three case studies with working Rocq/STL implemen
 tations—tax computation\, autonomous-vehicle compliance\, and recommendati
 on transparency—extending proof-carrying code from static programs to dyna
 mic AI outputs\, and we discuss specification-coupled small language model
 s published by regulators as an enabling substrate for proof generation. A
 dditional recent results from my group will be described too. Short bio:Sh
 lomi Dolev holds the Rita Altura Trust Chair in Computer Sciences at Ben-G
 urion University of the Negev\, where he was the founding chair of the Com
 puter Science Department and served as Dean of the Faculty of Natural Scie
 nces. He is an IEEE Fellow and an EAI Fellow\, served as the chairman of t
 he Israeli Inter-University Computation Center (IUCC)\, and the computer s
 cience committee of the Israeli ministry of education\, currently head of 
 the Negev Hi-Tech Faculty Startup Accelerator. Co-founder of Secret Double
  Octopus LTD and SecretSkyDB LTD. His research spans distributed computing
 \, cryptography\, self-stabilization\, and post-quantum systems\; he is th
 e author of the book Self-Stabilization (MIT Press).
DTSTART;TZID=Europe/Paris:20261008T100000
DTEND;TZID=Europe/Paris:20261008T100000
LAST-MODIFIED:20261005T120119Z
LOCATION:Aula Magna DIAG
SUMMARY:Super-intelligence Survival Guide: Verification via Proof-Carrying 
 Output - Shlomi Dolev
URL;TYPE=URI:https://www.diag.uniroma1.it/node/31566
END:VEVENT
END:VCALENDAR