BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//pretalx//cfp.riscv-europe.org//eu-summit-2026//speaker//XHATSH
BEGIN:VTIMEZONE
TZID:CET
BEGIN:STANDARD
DTSTART:20001029T040000
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=10
TZNAME:CET
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
BEGIN:DAYLIGHT
DTSTART:20000326T030000
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=3
TZNAME:CEST
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:pretalx-eu-summit-2026-RP8QNP@cfp.riscv-europe.org
DTSTART;TZID=CET:20260610T160000
DTEND;TZID=CET:20260610T161000
DESCRIPTION:Symbolic Quick Error Detection (SQED) streamlines processor ver
 ification by checking a microarchitecture-agnostic self-consistency proper
 ty using bounded model checking (BMC). While effective in detecting bugs w
 ithout manual property specification\, SQED suffers from severe scalabilit
 y limitations due to state explosion in complex designs. This paper introd
 uces RDM-SQED to mitigate this bottleneck by reducing the resource-intensi
 ve duplicate mode with a lightweight Processor-Level Abstraction (PLA). Th
 e PLA captures software-visible behaviors through a concise set of Element
 ary Instructions (EIs). To further constrain the verification logic\, we p
 ropose a recursive refinement algorithm that generates a minimal EI set. E
 xperimental evaluation on an out-of-order RISC-V processor demonstrates th
 at RDM-SQED significantly outperforms existing variants in both scalabilit
 y and bug\ndetection efficiency\, successfully identifying bugs that cause
  timeouts in other methods.
DTSTAMP:20260522T162352Z
LOCATION:Poster Island A
SUMMARY:Scalable Symbolic Quick Error Detection using Lightweight Processor
 -Level Abstraction - Yufeng Li
URL:https://cfp.riscv-europe.org/eu-summit-2026/talk/RP8QNP/
END:VEVENT
END:VCALENDAR