Showing cs.FLShow all
3 papers · 1 filter
cs.FL2024
Invariants for One-Counter Automata with Disequality Tests
Dmitry Chistikov, Jérôme Leroux, Henry Sinclair-Banks +1
We study the reachability problem for one-counter automata in which transitions can carry disequality tests. A disequality test is a guard that prohibits a specified counter value.…
cs.FL2023
Checking Presence Reachability Properties on Parameterized Shared-Memory Systems
Nicolas Waldburger
We consider the verification of distributed systems composed of an arbitrary number of asynchronous processes. Processes are identical finite-state machines that communicate by rea…
cs.FL2022
Parameterized safety verification of round-based shared-memory systems
Nathalie Bertrand, Nicolas Markey, Ocan Sankur +1
We consider the parameterized verification problem for distributed algorithms where the goal is to develop techniques to prove the correctness of a given algorithm regardless of th…