Jens Bendisposto


Heinrich-Heine-Universität Düsseldorf

Institut für Informatik
Universitätsstraße 1
D-40225 Düsseldorf


Tel.: +49 (211) 81-10714
Fax: +49 (211) 81-10712


Aktuelle Lehrveranstaltungen (Wintersemester 2017/2018)

  • Softwareentwickung im Team (Programmierpraktikum 2)
  • Datenverarbeitung für Nicht-Informatiker





  • 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.
    In 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.
Verantwortlich für den Inhalt: E-Mail sendenWE Informatik