BEGIN:VCALENDAR
PRODID:-//Columba Systems Ltd//NONSGML CPNG/SpringViewer/ICal Output/3.3-
 M3//EN
VERSION:2.0
CALSCALE:GREGORIAN
METHOD:PUBLISH
BEGIN:VEVENT
DTSTAMP:20260611T085328Z
DTSTART:20260610T130000Z
DTEND:20260610T140000Z
SUMMARY:Departmental Seminar: “Formal Methods at Industrial Scale\, Befor
 e and After AI” by Dr Claudia Cauli\, Principal Research Engineer\, Huaw
 ei R&D
UID:{http://www.columbasystems.com/customers/uom/gpp/eventid/}p2az-mq99fz
 hl-702nqh
DESCRIPTION:Over the past two years\, my team at Huawei Cloud has applied
  formal methods to production cloud infrastructure. We deployed model ch
 ecking\, deductive verification\, and SMT encodings\, within model-based
  and code-level approaches\, to establish the correctness of a distribut
 ed key-value store\, a global server load balancer\, IAM security analys
 es\, and a BPF static validator. Across these projects\, we prevented cr
 itical bugs from reaching production\, improved the performance of a sec
 urity feature\, and discovered high-severity low-level bugs. In this tal
 k\, I'll walk through what worked and what didn't\, and share both perso
 nal experience and concrete data\, reflecting on what I think the AI rev
 olution means for FM engineering as a research agenda and where interest
 ing open problems now sit.
STATUS:TENTATIVE
TRANSP:TRANSPARENT
CLASS:PUBLIC
LOCATION:Kilburn_TH 1.3\, Kilburn Building\, Manchester
END:VEVENT
END:VCALENDAR
