Witold Charatonik

Welcome to my home page. It contains:

• About me (includes short CV)
• Teaching
• Research interests
• My address
• List of publications
• My pgp public key
• Private info

About me

Conference involvements

• ELICS'02 Symposium on the Effectiveness of Logic in Computer Science in Honour of Moshe Vardi
• FoSSaCS'03 6th International Conference on Foundations of Software Science and Computation Structures
• LICS'03 18th Annual IEEE Symposium on Logic in Computer Science
• Concur'03 14th International Conference on Concurrency Theory

• set constraints and set-based analysis
• verification, in particular model checking for infinite-state systems
• logic programming
• tree automata
• mobile ambients

• 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 and Andreas Podelski, Set constraints with intersection, Accepted for publication in Information and Computation (Special Issue of selected LICS'97 papers) as of June 14, 2000. Electronic version in Ideal First
• 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, 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

 
-----BEGIN PGP PUBLIC KEY BLOCK-----
Version: 2.6.3i

mQCNAzFbz74AAAEEAKg4vmh7iIHEe/O+lJ47H1WL5zDpIah390hL3xuDotGRUD/n
F9pT67m7sCHhT26CYDtKODeXQJmWeVlpzuHA9u7V/vc41CyPHW9PSjtClYCz0pM7
1cbSGpxWoZUAWaPTXwKeRVa0HFK8ndXf2tr1Z3bwxubk57gJOrSWSQPTnvVVAAUR
tChXaXRvbGQgQ2hhcmF0b25payA8d2l0b2xkQG1waS1zYi5tcGcuZGU+iQCVAwUQ
MVvPv7SWSQPTnvVVAQFilwP/f88rht6AuJW34BX/w8HOsfDLGg7wj4sYUxMedj2h
PCgOy9LbpKWPLM1pnXyXN4SrJPMwmITsx4pGBn4XrX5GZPv4+o54Y+K/W4hYtzi/
kd6DqGZeDRsQole0xbkreHGOX513lrJ8oYZJe/UbvdaJXQK/bUcfqUSneXHBDKQd
IUY=
=ymuy
-----END PGP PUBLIC KEY BLOCK-----