3 papers
cs.CR2025
A Formally Verified Lightning Network
Grzegorz Fabiański, Rafał Stefański, Orfeas Stefanos Thyfronitis Litos
In this work we use formal verification to prove that the Lightning Network (LN), the most prominent scaling technique for Bitcoin, always safeguards the funds of honest users. We…
cs.FL2025
Polyregular Model Checking
Aliaume Lopez, Rafał Stefański
We introduce a high-level language with Python-like syntax for string-to-string, polyregular, first-order definable transductions. This language features function calls, boolean va…
cs.FL2020
Extensions of -Regular Languages
Mikołaj Bojańczyk, Edon Kelmendi, Rafał Stefański +1
We consider extensions of monadic second order logic over -words, which are obtained by adding one language that is not -regular. We show that if the added language has a…