Contact    Jobs
Search:
Bernd Finkbeiner

Reactive Systems Group
Universität des Saarlandes
Phone: +49 681 302 5632
eMail: finkbeiner at cs.uni-sb.de
Building: E 1 3 Room: 506
Coordinates: N 49.257833° E 7.045144°

I am a professor in computer science at Saarland University. I am currently the chairman of the examination board. If you have questions regarding the examination regulations please come to my office hours on Wednesdays 3-4pm.

Research

I am interested in computer systems and protocols that are reactive in nature: systems of concurrent processes that interact with each other and with their environment over a possibly infinite run. Parallelism and nondeterminism make it difficult to design such systems correctly. My research concerns computer-aided methods that derive implementations from formal specifications (synthesis) and that prove that a given implementation satisfies a logical property (verification).

Teaching

  • Wintersemester 2009/2010: Verification (Stammvorlesung) How can one ensure that computer programs actually do what they are intended to do? Simply running a program repeatedly with various inputs is inadequate, because one cannot tell which inputs might cause the program to fail. It is possible to tailor a tester to test a given program, but present-day programs are so complex that they cannot be adequately checked through conventional testing, which can leave significant bugs undetected. Program verification uses mathematical and logical methods to prove that a program is correct. This approach was pioneered by, among others, Dijkstra, Floyd, Gries, Hoare, Lamport, Manna, Owicki and Pnueli. Today, we have powerful decision procedures that can, completely automatically, answer basic questions about the data types typically used by programmers. Model Checking is a “push-button” technology that can analyze finite-state abstractions of programs with as many as 1020 states. This course takes an up-to-date look at the theory and practice of program verification.

Recent Professional Activities

  • PC member of SAASE 2009, October 14-17, 2009.
  • PC member of SGI 2009, September 28, 2009
  • PC member of TIME 2009, July 23-25, 2009.
  • PC member of PADTAD 2009", July 19-20, 2009. “:* PC member of RV 2009, June 26-28, 2009.
  • PC member of AFM 2009, June 27, 2009.
  • PC member of Haifa Verification Conference 2008, October 27-30, 2008.
  • PC member of AFM 2008, July 14, 2008.
  • PC member of PADTAD 2008, July 20-21, 2008.
  • Co-organizer of MBT 2008: Fourth Workshop on Model-Based Testing, March 30, 2008.
  • Invited speaker at Deduktionstreffen 2008, March 17-18, 2008.
  • Invited speaker at OMEGA 2007, October 26, 2007.
  • PC member of AFM07, November 6, 2007.
  • PC member of HVC 2007, October 23 – 25, 2007.
  • Invited speaker at FoMSESS 2007, June 4 – 5, 2007.
  • Co-organizer of MBT 2007: Third Workshop on Model-Based Testing, March 31 – April 1, 2007.
  • PC member of RV 2007: Workshop on Runtime Verification, 2007.
  • Co-organizer of Dagstuhl Seminar 07011 on Runtime Verification, January 2-6, 2007.
  • PC member of IBM Verification Conference 2006, October 23-26, 2006.
  • Co-organizer of MBT 2006: The Second Workshop on Model based Testing, March 25-26, 2006.
  • PC member of FATES/RV 2006: The first Joint International Workshop on Formal Aspects of Testing and Runtime Verification, August 15 – 16, 2006.
  • PC member of PADTAD 2006: Parallel and Distributed Systems: Testing and Debugging, July 17, 2006.
  • Co-organizer of RV 2005: Fifth Workshop on Runtime Verification, July 12, 2005.
  • PC member of VMSIS 2005: Workshop on Visual Modeling for Software Intensive Systems, September 24, 2005, Dallas, Texas, USA.
  • Invited speaker at IBM Verification Conference 2005, November 13 – 16, 2005, Haifa, Israel.