Jump to contentJump to search

Jens Bendisposto

Contact Information

Heinrich-Heine-Universität Düsseldorf

Institut für Informatik

Universitätsstraße 1
D-40225 Düsseldorf



Phone: +49 (211) 81-10714
Fax: +49 (211) 81-10712


Current Courses (Winterterm 2016)

  • undefinedFunctional Programming

You can find proposed theses undefinedhere.







  • Janine Golov, Jens Bendisposto
    (Teil)-Invertierung der Programmierausbildung.
    In Inverted Classroom - The next Stage, Lernen und Lehren im 21. Jahrhundert, Sabrina Zeaiter and Jürgen Handke, Tectum, 29--37, 2017.


    • Jens Bendisposto, Philipp Körner, Michael Leuschel, Jeroen Meijer, van de Pol, Jaco, Helen Treharne, Jorden Whitefield
      Symbolic Reachability Analysis of B through ProB and LTSmin.
      In Proceedings iFM 2016, LNCS, 9681, Springer, 2016.
    • Joy Clark, Jens Bendisposto, Stefan Hallerstede, Dominik Hansen, Michael Leuschel
      Generating Event-B Specifications from Algorithm Descriptions.
      In Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings, Michael J. Butler and Klaus-Dieter Schewe and Atif Mashkoor and Miklós Biró, Lecture Notes in Computer Science, 9675, Springer, 183--197, 2016.


    • Ladenberger, Lukas, Hansen, Dominik, Wiegard, Harald, Bendisposto, Jens, Leuschel, Michael
      Validation of the ABZ landing gear system using ProB.
      In International Journal on Software Tools for Technology Transfer, Springer Berlin Heidelberg, 1-17, 2015.
    • From Failure to Proof: The ProB Disprover for B and Event-B.
      In Proceedings SEFM'2015, LNCS 9276, Springer, 2015.




    • Bendisposto, Jens, Fritz, Fabian, Jastram, Michael, Leuschel, Michael, Weigelt, Ingo
      Developing Camille, a text editor for Rodin.
      In Software: Practice and Experience, 41, 2, John Wiley & Sons, Ltd., 189--198, 2011.
    • Automatic Flow Analysis for Event-B.
      In Proceedings of Fundamental Approaches to Software Engineering (FASE) 2011, Dimitra Giannakopoulou and Fernando Orejas, Lecture Notes in Computer Science, 6603, Springer, 50--64, 2011.


    • Directed Model Checking for B: An Evaluation and New Techniques.
      In SBMF'2010, Jim Davies and Leila Silva and Adenilso da Silva Simão, Lecture Notes in Computer Science, 6527, Springer, 1--16, 2010.
    • GEPAVAS Gerichtete und parallele Validierung von abstrakten Spezifikationen - Projektreport.
      Technical Report, University of Düsseldorf, 2010.


    • Proof Assisted Model Checking for B.
      In Proceedings of ICFEM 2009, Karin Breitman and Ana Cavalcanti, Lecture Notes in Computer Science, 5885, Springer, 504-520, 2009.
    • Sebastian Wieczorek, Vitaly Kozyura, Andreas Roth, Michael Leuschel, Jens Bendisposto, Daniel Plagge, Ina Schieferdecker
      Applying Model Checking to Generate Model-based Integration Tests from Choreography Models.
      In Proceedings TESTCOM/FATES 2009, Lecture Notes in Computer Science, 5826, Springer-Verlag, 179--194, 2009.
    • Visualising Event-B Models with B-Motion Studio.
      In Proceedings of FMICS 2009, Marı́a Alpuente and Byron Cook and Christophe Joubert, Lecture Notes in Computer Science, 5825, Springer, 202-204, 2009.
    • Mireille Samia, Harald Wiegard, Jens Bendisposto, Michael Leuschel
      High-Level versus Low-Level Specifications: Comparing B with Promela and ProB with Spin.
      In Proceedings TFM-B 2009, Attiogbe and Mery, APCB, 2009.
    • Parallel Model Checking of Event-B Specification with ProB.
      In 2009.


      • Michael Leuschel, Mireille Samia, Jens Bendisposto, Li Luo
        Easy Graphical Animation and Formula Viewing for Teaching B.
        In The B Method: from Research to Teaching, C. Attiogbé and H. Habrias, Lina, 17--32, 2008.
      • A Semantics-Aware Editing Environment for Prolog in Eclipse.
        In Proceedings of the 18th Workshop on Logic-based methods in Programming Environments, WLPE, 2008.
      • Jens Bendisposto, Michael Leuschel, O. Ligot, Mireille Samia
        La validation de modèles Event-B avec le plug-in ProB pour RODIN.
        In Technique et Science Informatiques, 27, 8, 1065-1084, 2008.


        • BE4: The B Extensible Eclipse Editing Environment.
          In Proceedings of B 2007, Jacques Julliand and Olga Kouchnarenko, Lecture Notes in Computer Science, 4355, Springer, 270-273, 2007.
        • A Generic Flash-Based Animation Engine for ProB.
          In Proceedings of B 2007, Jacques Julliand and Olga Kouchnarenko, Lecture Notes in Computer Science, 4355, Springer, 266-269, 2007.
        • Debugging Event-B Models using the ProB Disprover Plug-in.
          In Proceedings AFADL'07, 2007.


        • Animating and Model Checking B Specifications with Higher-Order Recursive Functions.
          In Dagstuhl Seminar 06191 "Rigorous Methods for Software Construction and Analysis", J. Abrial, U. Glässer, 2006.
        Responsible for the content: