Witold Charatonik

Welcome to my home page. It contains:

• About me (includes short CV)
• Research interests
• My addresses
• Publications
• Teaching

About me

• Logic in computer science

Conference involvements

• MFCS 2010 35th International Symposium on Mathematical Foundations of Computer Science
• FCT 2009 17th International Symposium on Fundamentals of Computation Theory
• TALE 2007 Workshop on Theory and Applications of Language Equations
• PPDP'07 9th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming
• SofSem'06 32nd International Conference on Current Trends in Theory and Practice of Computer Science
• FoSSaCS'05 8th International Conference on Foundations of Software Science and Computation Structures
• TACAS'04 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
• Concur'03 14th International Conference on Concurrency Theory
• LICS'03 18th Annual IEEE Symposium on Logic in Computer Science
• FoSSaCS'03 6th International Conference on Foundations of Software Science and Computation Structures
• ELICS'02 Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi

My addresses

• CSL'05 Bounded Model Checking of Pointer Programs, Proceedings of the 19th Annual Conference of the European Association for Computer Science Logic, Springer LNCS 3634, pp 397-412, Springer-Verlag, 2001, co-authors: Lilia Georgieva, Patrick Maier
• CONCUR'02 On name generation and set-based analysis in the Dolev-Yao model, Proceedings of the 13th International Conference on Concurrency Theory, LNCS, 2421, pp 499-514, Springer-Verlag, 2002, co-author: Roberto Amadio
• ICLP'02 Constraint-Based Infinite Model Checking and Tabulation for Stratified CLP, Proceedings of the 19th International Conference on Logic Programming LNCS, 2401, pp 115-129, Springer-Verlag, 2002, co-authors: Supratik Mukhopadhyay and Andreas Podelski
• RTA'02 Atomic Set Constraints with Projection Proceedings of the 13th Conference on Rewriting Techniques and Applications, Springer LNCS, 2378, pp 311-325, Springer-Verlag, 2002, co-author: Jean-Marc Talbot. Full version in a technical report
• ESOP'02 Finite-Control Mobile Ambients Proceedings of the European Symposium on Programming, Springer LNCS, 2305, pp 295-313, Springer-Verlag, 2002, co-authors: Andrew D. Gordon, Jean-Marc Talbot.
• VMCAI'02 Compositional Termination Analysis of Symbolic Forward AnalysisVerification, Model Checking, and Abstract Interpretation, Third International Workshop, Revised Papers. Springer LNCS 2294, pp 109-125, Springer-Verlag, 2002, co-authors: Supratik Mukhopadhyay and Andreas Podelski
• CSL'01 The Decidability of Model Checking Mobile Ambients Proceedings of the 15th Annual Conference of the European Association for Computer Science Logic, Springer LNCS 2142, pp 339-354, Springer-Verlag, 2001, co-author: Jean-Marc Talbot.
• FOSSACS'01 The Complexity of Model Checking Mobile Ambients, Proceedings of of the 4th International Conference on Foundations of Software Science and Computation Structures, Springer LNCS 2030, pp 152-167, Springer-Verlag, 2001, co-authors: Silvano Dal Zilio, Andrew D. Gordon, Supratik Mukhopadhyay, Jean-Marc Talbot. Full version in a technical report
• ESOP'00 Directional Type Checking: Beyond Discriminative Types, Proceedings of the European Symposium on Programming, Springer LNCS 1782, pp 72-87, Springer-Verlag, 2000.
• POPL'00 Paths vs. Trees in Set-based Program Analysis, Proceedings of the 27th Annual ACM Symposium on Principles of Programming Languages, pp 330-338, January 2000, ACM Press, co-authors: Andreas Podelski and Jean-Marc Talbot.
  Definitive copy in ACM's Digital Library
• ESOP'99 Set-based Failure Analysis for Logic Programs and Concurrent Constraint Programs, Proceedings of the European Symposium on Programming, Springer LNCS 1576, pp 177-192, co-authors: Andreas Podelski and Martin Müller
• SAS'98 Directional Type Inference for Logic Programs, Proceedings of the Fifth International Static Analysis Symposium, Pisa, Italy, September 1998, Springer LNCS 1503, pp 278-294, co-author: Andreas Podelski
• LICS'98 The Horn Mu-calculus, Proceedings of the 13th IEEE Symposium on Logic in Computer Science, Indianapolis 1998, pp 58-69, co-authors: David McAllester, Damian Niwinski, Andreas Podelski , Igor Walukiewicz
• RTA'98 Co-definite Set Constraints, Proceedings of the 9th Conference on Rewriting Techniques and Applications, Tsukuba, Japan, March/April 1998, LNCS 1379, pp 211-225, co-author: Andreas Podelski
• TACAS'98 Set-based Analysis of Reactive Infinite-state Systems, Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Lisbon, Portugal, March 28 - April 4, 1998, LNCS 1384, pp 358-375, Springer-Verlag, 2000. co-author: Andreas Podelski
• LICS'97 Set Constraints with Intersection, Proceedings of the 12th IEEE Symposium on Logic in Computer Science, Warsaw 1997, pp 362 -- 372, co-author: Andreas Podelski
• CP'96 The Independence property of a Class of Set Constraints, Proceedings of the Conference on Principles and Practice of Constraint Programming (CP), LNCS 1118, pp 76-90. Springer-Verlag, 1996. abstract, postscript file (250K), dvi file (81K), or compressed postscript file (115K), co-author: Andreas Podelski
• FOCS'94 Set constraints with projections are in NEXPTIME, Proceedings of the 35th Annual Symposium on Foundations of Computer Science (FOCS), Santa Fe 1994, pp 642 -- 653 abstract, postscript file (184K), dvi file (88K), or compressed postscript file (82K), co-author: Leszek Pacholski
• CCL'94 Set constraints in some equational theories, Proceedings of the 1st International Conference Constraints in Computational Logics, Munich 1994, LNCS 845 (1994), pp 304 -- 319. Springer-Verlag, 1994. abstract,
• LICS'94 Negative set constraints with equality, Proceedings of the 9th IEEE Symposium on Logic in Computer Science, Paris 1994, pp 128 -- 136 abstract, postscript file (138K), dvi file (59K), or compressed postscript file (66K), co-author: Leszek Pacholski
• IWWERT'91 Word Equations with Two Variables, Proceedings of 2nd Workshop on Word Equations and Related Topics, IWWERT'91, Springer LNCS 677 (1993), pp 43 -- 56, co-author: Leszek Pacholski

• Witold Charatonik, Silvano Dal Zilio, Andrew D. Gordon, Supratik Mukhopadhyay, and Jean-Marc Talbot, Model checking mobile ambients. Theoretical Computer Science 308/1-3:277-331, Elsevier, 2003.
• Witold Charatonik and Andreas Podelski, Set constraints with intersection Information and Computation (Special Issue of selected LICS'97 papers) 179(2):213--229, Elsevier, December 2002.
• Witold Charatonik, An Undecidable Fragment of the Theory of Set Constraints, Information Processing Letters 68(3):147-151, November 1998.
• Witold Charatonik, Set constraints in some equational theories, Information and Computation (Special Issue of selected CCL'94 papers) 142(1):40-75, April 1998.

• Witold Charatonik, Lilia Georgieva, Patrick Maier, Bounded Model Checking of Pointer Programs, Technical Report, Max-Planck-Institut für Informatik, MPI-I-2005-2-002. Extended version of the CSL'05 paper.
• Witold Charatonik, Jean-Marc Talbot, Atomic Set Constraints with Projection, Technical Report, Max-Planck-Institut für Informatik, MPI-I-2002-2-008, May 2002
• Witold Charatonik and Harald Ganzinger (Eds.) Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi Technical report MPI-I-2002-2-007, Max-Planck-Institut für Informatik, March 2002
• Roberto Amadio, Witold Charatonik, On name generation and set-based analysis in Dolev-Yao model, INRIA Research Report 4379, January 2002.
• Witold Charatonik, Silvano Dal Zilio, Andrew D. Gordon, Supratik Mukhopadhyay, Jean-Marc Talbot, The Complexity of Model Checking Mobile Ambients, Technical Report MSR-TR-2001-03, Microsoft Research, May 2001
• Witold Charatonik, Automata on DAG Representations of Finite Trees, Technical Report , Max-Planck-Institut für Informatik, MPI-I-1999-2-001, March 1999
• Witold Charatonik, Andreas Podelski, Set constraints for greatest models, Technical Report , Max-Planck-Institut für Informatik, MPI-I-97-2-004, April 1997
• Witold Charatonik, Set constraints in some equational theories, Phd thesis, Polish Academy of Sciences, 1995 abstract, postscript file (401K), dvi file (208K), or compressed postscript file (164K)
• Witold Charatonik, Leszek Pacholski, Set constraints with projections are in NEXPTIME, Raport de Recherche No 930, 08/1994, LRI, Universite de Paris--Sud
• Witold Charatonik, Leszek Pacholski, Negative set constraints: an easy proof of decidability, Technical Report, Max-Planck-Institut für Informatik, MPI-I-93-265, December 1993