| 2022 | ITP | The Zoo of Lambda-Calculus Reduction Strategies, And Coq. | Malgorzata Biernacka, Witold Charatonik, Tomasz Drab |
| 2021 | PPDP | A Derived Reasonable Abstract Machine for Strong Call by Value. | Malgorzata Biernacka, Witold Charatonik, Tomasz Drab |
| 2020 | APLAS | An Abstract Machine for Strong Call by Value. | Malgorzata Biernacka, Dariusz Biernacki, Witold Charatonik, Tomasz Drab |
| 2018 | LPAR | Two-variable First-Order Logic with Counting in Forests. | Witold Charatonik, Yegor Guskov, Ian Pratt-Hartmann, Piotr Witkowski |
| 2017 | CSL | Extending Two-Variable Logic on Trees. | Bartosz Bednarczyk, Witold Charatonik, Emanuel Kieronski |
| 2015 | CSL | Two-variable Logic with Counting and a Linear Order. | Witold Charatonik, Piotr Witkowski |
| 2014 | CSL | Decidability of weak logics with deterministic transitive closure. | Witold Charatonik, Emanuel Kieronski, Filip Mazowiecki |
| 2013 | ICALP | Complexity of Two-Variable Logic on Finite Trees. | Saguy Benaim, Michael Benedikt, Witold Charatonik, Emanuel Kieronski, Rastislav Lenhardt, Filip Mazowiecki, James Worrell |
| 2013 | LICS | Two-Variable Logic with Counting and Trees. | Witold Charatonik, Piotr Witkowski |
| 2011 | LATA | The Parameterized Complexity of Chosen Problems for Finite Automata on Trees. | Agata Barecka, Witold Charatonik |
| 2010 | LPAR | On the Complexity of the Bernays-Schnfinkel Class with Datalog. | Witold Charatonik, Piotr Witkowski |
| 2008 | CSL | Quantified Positive Temporal Constraints. | Witold Charatonik, Michal Wrona |
| 2008 | LPAR | Tractable Quantified Constraint Satisfaction Problems over Positive Temporal Templates. | Witold Charatonik, Michal Wrona |
| 2007 | PPDP | Regular directional types for logic programs. | Witold Charatonik |
| 2005 | CSL | Bounded Model Checking of Pointer Programs. | Witold Charatonik, Lilia Georgieva, Patrick Maier |
| 2002 | CONCUR | On Name Generation and Set-Based Analysis in the Dolev-Yao Model. | Roberto M. Amadio, Witold Charatonik |
| 2002 | ESOP | Finite-Control Mobile Ambients. | Witold Charatonik, Andrew D. Gordon, Jean-Marc Talbot |
| 2002 | ICLP | Constraint-Based Infinite Model Checking and Tabulation for Stratified CLP. | Witold Charatonik, Supratik Mukhopadhyay, Andreas Podelski |
| 2002 | VMCAI | Compositional Termination Analysis of Symbolic Forward Analysis. | Witold Charatonik, Supratik Mukhopadhyay, Andreas Podelski |
| 2001 | CSL | The Decidability of Model Checking Mobile Ambients. | Witold Charatonik, Jean-Marc Talbot |
| 2001 | FOSSACS | The Complexity of Model Checking Mobile Ambients. | Witold Charatonik, Silvano Dal-Zilio, Andrew D. Gordon, Supratik Mukhopadhyay, Jean-Marc Talbot |
| 2000 | ESOP | Directional Type Checking for Logic Programs: Beyond Discriminative Types. | Witold Charatonik |
| 2000 | POPL | Paths vs. Trees in Set-Based Program Analysis. | Witold Charatonik, Andreas Podelski, Jean-Marc Talbot |
| 1999 | ESOP | Set-Based Failure Analysis for Logic Programs and Concurrent Constraint Programs. | Andreas Podelski, Witold Charatonik, Martin Mller |
| 1998 | LICS | The Horn Mu-calculus. | Witold Charatonik, David A. McAllester, Damian Niwinski, Andreas Podelski, Igor Walukiewicz |
| 1998 | SAS | Directional Type Inference for Logic Programs. | Witold Charatonik, Andreas Podelski |
| 1998 | TACAS | Set-Based Analysis of Reactive Infinite-State Systems. | Witold Charatonik, Andreas Podelski |
| 1997 | LICS | Set Constraints with Intersection. | Witold Charatonik, Andreas Podelski |
| 1996 | CP | The Independence Property of a Class of Set Constraints. | Witold Charatonik, Andreas Podelski |
| 1994 | FOCS | Set constraints with projections are in NEXPTIME | Witold Charatonik, Leszek Pacholski |
| 1994 | LICS | Negative Set Constraints with Equality | Witold Charatonik, Leszek Pacholski |