32 citations · 40 across the 6 of their papers we have counts for
3 papers · 1 filter
Extending Two-Variable Logic on Trees
Bartosz Bednarczyk, Witold Charatonik, Emanuel Kieroński
The finite satisfiability problem for the two-variable fragment of first-order logic interpreted over trees was recently shown to be ExpSpace-complete. We consider two extensions o…
Two-variable Logic with Counting and a Linear Order
Witold Charatonik, Piotr Witkowski
We study the finite satisfiability problem for the two-variable fragment of first-order logic extended with counting quantifiers (C2) and interpreted over linearly ordered structur…
Bounded Model Checking of Pointer Programs Revisited
Witold Charatonik, Piotr Witkowski
Bounded model checking of pointer programs is a debugging technique for programs that manipulate dynamically allocated pointer structures on the heap. It is based on the following…