~/talk

Solving Conditional Linear Recurrences for Program Verification: The Periodic C...

on YouTube 15m
Talkat OOPSLA 2023 · 2023-10-23..10-27· [compilers-and-language-design]

speakers

name:Chenglin Wang
links:none on file
name:Fangzhen Lin
links:none on file

resources

video:https://youtu.be/I4rjBjQEBso
slides:none on file

summary

Shows that a conditional linear recurrence has a computable closed form whenever its ultimately periodic index sequence holds, proves checking that property is undecidable, and gives a practical generate-and-verify algorithm that guesses a periodic block from a few iterations, computes symbolic matrix powers (Jordan form), then validates the guess. A prototype solver produces closed forms, plugs into Z3-based verification, handles many benchmarks (including unknown initial values with a separate technique), and compares favorably to IC and ViP.

AI-written summary · about

chapters (12)

  1. 0:00Introduction
  2. 0:23Recurrence analysis in verification
  3. 1:49Conditional recurrences in SMT
  4. 3:15Periodic linear solver contributions
  5. 3:36Conditional linear recurrences
  6. 4:38Matrix power for periodic recurrences
  7. 6:45Generalizing periodic index sequences
  8. 7:27Index sequences concept
  9. 8:11Guessing periodic segments
  10. 11:01Unknown initial values in recurrences
  11. 11:44Benchmark results
  12. 13:09Q&A

related talks

~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.