2 papers
cs.LO2017
Modulo Counting on Words and Trees
Bartosz Bednarczyk, Witold Charatonik
We consider the satisfiability problem for the two-variable fragment of the first-order logic extended with modulo counting quantifiers and interpreted over finite words or trees.…
cs.LO2016
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…