Word Equations with Two Variables. - Witold Charatonik; Leszek Pacholski (IWWERT, 1991)

Set constraints with projections are in NEXPTIME - Witold Charatonik; Leszek Pacholski (FOCS, 1994)

Negative Set Constraints with Equality - Witold Charatonik; Leszek Pacholski (LICS, 1994)

The Independence Property of a Class of Set Constraints. - Witold Charatonik; Andreas Podelski (CP, 1996)

The Horn Mu-calculus. - Witold Charatonik; David A. McAllester; Damian Niwinski; Andreas Podelski; Igor Walukiewicz (LICS, 1998)

Co-definite Set Constraints. - Witold Charatonik; Andreas Podelski (RTA, 1998)

Directional Type Inference for Logic Programs. - Witold Charatonik; Andreas Podelski (SAS, 1998)

Set-Based Analysis of Reactive Infinite-State Systems. - Witold Charatonik; Andreas Podelski (TACAS, 1998)

Set Constraints in Some Equational Theories. - Witold Charatonik (Inf. Comput., 1998)

An Undecidable Fragment of the Theory of Set Constraints. - Witold Charatonik (Inf. Process. Lett., 1998)

Set-Based Failure Analysis for Logic Programs and Concurrent Constraint Programs. - Andreas Podelski; Witold Charatonik; Martin Müller 001 (ESOP, 1999)

Directional Type Checking for Logic Programs: Beyond Discriminative Types. - Witold Charatonik (ESOP, 2000)

Paths vs. Trees in Set-Based Program Analysis. - Witold Charatonik; Andreas Podelski; Jean-Marc Talbot (POPL, 2000)

The Decidability of Model Checking Mobile Ambients. - Witold Charatonik; Jean-Marc Talbot (CSL, 2001)

The Complexity of Model Checking Mobile Ambients. - Witold Charatonik; Silvano Dal-Zilio; Andrew D. Gordon 001; Supratik Mukhopadhyay; Jean-Marc Talbot (FoSSaCS, 2001)

On Name Generation and Set-Based Analysis in the Dolev-Yao Model. - Roberto M. Amadio; Witold Charatonik (CONCUR, 2002)

Finite-Control Mobile Ambients. - Witold Charatonik; Andrew D. Gordon 001; Jean-Marc Talbot (ESOP, 2002)

Constraint-Based Infinite Model Checking and Tabulation for Stratified CLP. - Witold Charatonik; Supratik Mukhopadhyay; Andreas Podelski (ICLP, 2002)

Atomic Set Constraints with Projection. - Witold Charatonik; Jean-Marc Talbot (RTA, 2002)

Compositional Termination Analysis of Symbolic Forward Analysis. - Witold Charatonik; Supratik Mukhopadhyay; Andreas Podelski (VMCAI, 2002)

Set Constraints with Intersection. - Witold Charatonik; Andreas Podelski (Inf. Comput., 2002)

Model checking mobile ambients. - Witold Charatonik; Silvano Dal-Zilio; Andrew D. Gordon 001; Supratik Mukhopadhyay; Jean-Marc Talbot (Theor. Comput. Sci., 2003)

Bounded Model Checking of Pointer Programs. - Witold Charatonik; Lilia Georgieva; Patrick Maier 001 (CSL, 2005)

2-SAT Problems in Some Multi-Valued Logics Based on Finite Lattices. - Witold Charatonik; Michal Wrona (ISMVL, 2007)

Regular directional types for logic programs. - Witold Charatonik (PPDP, 2007)

Quantified Positive Temporal Constraints. - Witold Charatonik; Michal Wrona (CSL, 2008)

Tractable Quantified Constraint Satisfaction Problems over Positive Temporal Templates. - Witold Charatonik; Michal Wrona (LPAR, 2008)

On the Complexity of the Bernays-Schönfinkel Class with Datalog. - Witold Charatonik; Piotr Witkowski 001 (LPAR (Yogyakarta), 2010)

Set constraints with projections. - Witold Charatonik; Leszek Pacholski (J. ACM, 2010)

The Parameterized Complexity of Chosen Problems for Finite Automata on Trees. - Agata Barecka; Witold Charatonik (LATA, 2011)

Satisfiability of the Two-Variable Fragment of First-Order Logic over Trees - Witold Charatonik; Emanuel Kieronski; Filip Mazowiecki (CoRR, 2013)

Parameterized complexity of basic decision problems for tree automata. - Witold Charatonik; Agata Chorowska (Int. J. Comput. Math., 2013)

Decidability of weak logics with deterministic transitive closure. - Witold Charatonik; Emanuel Kieronski; Filip Mazowiecki (CSL-LICS, 2014)

Bounded Model Checking of Pointer Programs Revisited. - Witold Charatonik; Piotr Witkowski 001 (CoRR, 2016)

Two-variable Logic with Counting and a Linear Order. - Witold Charatonik; Piotr Witkowski 001 (Log. Methods Comput. Sci., 2016)

Complexity of Two-Variable Logic on Finite Trees. - Saguy Benaim; Michael Benedikt; Witold Charatonik; Emanuel Kieronski; Rastislav Lenhardt; Filip Mazowiecki; James Worrell 001 (ACM Trans. Comput. Log., 2016)

Two-Variable Logic with Counting and Trees. - Witold Charatonik; Piotr Witkowski 001 (ACM Trans. Comput. Log., 2016)

Extending Two-Variable Logic on Trees. - Bartosz Bednarczyk; Witold Charatonik; Emanuel Kieronski (CSL, 2017)

Modulo Counting on Words and Trees. - Bartosz Bednarczyk; Witold Charatonik (FSTTCS, 2017)

Generalized Refocusing: From Hybrid Strategies to Abstract Machines. - Malgorzata Biernacka; Witold Charatonik; Klara Zielinska (FSCD, 2017)

Two-variable First-Order Logic with Counting in Forests. - Witold Charatonik; Yegor Guskov; Ian Pratt-Hartmann; Piotr Witkowski 001 (LPAR, 2018)

Deriving an Abstract Machine for Strong Call by Need. - Malgorzata Biernacka; Witold Charatonik (FSCD, 2019)

An Abstract Machine for Strong Call by Value. - Malgorzata Biernacka; Dariusz Biernacki; Witold Charatonik; Tomasz Drab (APLAS, 2020)

A Derived Reasonable Abstract Machine for Strong Call by Value. - Malgorzata Biernacka; Witold Charatonik; Tomasz Drab (PPDP, 2021)

Strong Call by Value is Reasonable for Time. - Malgorzata Biernacka; Witold Charatonik; Tomasz Drab (CoRR, 2021)

The Zoo of Lambda-Calculus Reduction Strategies, And Coq. - Malgorzata Biernacka; Witold Charatonik; Tomasz Drab (ITP, 2022)

A simple and efficient implementation of strong call by need by an abstract machine. - Malgorzata Biernacka; Witold Charatonik; Tomasz Drab (Proc. ACM Program. Lang., 2022)