BEGIN:VCALENDAR
VERSION:2.0
PRODID:Linklings LLC
BEGIN:VTIMEZONE
TZID:America/Los_Angeles
X-LIC-LOCATION:America/Los_Angeles
BEGIN:DAYLIGHT
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
DTSTART:19700308T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=2SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
DTSTART:19701101T020000
RRULE:FREQ=YEARLY;BYMONTH=11;BYDAY=1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTAMP:20211208T164409Z
LOCATION:3016
DTSTART;TZID=America/Los_Angeles:20211208T105200
DTEND;TZID=America/Los_Angeles:20211208T111500
UID:dac_DAC 2021_sess132_RESEARCH479@linklings.com
SUMMARY:Theory-Specific Proof Steps Witnessing Correctness of SMT Executio
 ns
DESCRIPTION:Research Manuscript\n\nTheory-Specific Proof Steps Witnessing 
 Correctness of SMT Executions\n\nHyvärinen\n\nEnsuring hardware and softwa
 re correctness increasingly relies on the use of symbolic logic solvers, i
 n particular for satisfiability modulo theories (SMT).  However, building 
 efficient and correct SMT solvers is difficult: even state-of-the-art solv
 ers disagree on instance satisfiability.  This work presents a system for 
 witnessing unsatisfiability of instances of NP problems, commonly appearin
 g in verification, in a way that is natural to SMT solving. Our implementa
 tion of the system seems to often result in significantly smaller witnesse
 s, lower solving overhead, and faster checking time in comparison to exist
 ing proof formats that can serve a similar purpose.\n\nTopic: EDA\n\nKeywo
 rd: Design Verification and Validation\n\nVirtual Program: Presented In-Pe
 rson
END:VEVENT
END:VCALENDAR