Gesellschaft für Informatik e.V.

Die Hauptredner...

• Bernd Finkbeiner , Universität des Saarlandes:

  Slicing Abstractions

  
  

  Abstraction and slicing are both techniques for reducing the size of the state space to be inspected during verification. In this talk, I will present a new model checking procedure for infinite-state concurrent systems that interleaves automatic abstraction refinement, which splits states according to new predicates obtained by Craig interpolation, with slicing, which removes irrelevant states and transitions from the abstraction. The effects of abstraction and slicing complement each other. As the refinement progresses, the increasing accuracy of the abstract model allows for a more precise slice; the resulting smaller representation gives room for additional predicates in the abstraction. The procedure terminates when an error path in the abstraction can be concretized, which proves that the system is erroneous, or when the slice becomes empty, which proves that the system is correct. The talk is based on joint work with Ingo Brückner, Klaus Dräger, and Heike Wehrheim.

  
  
• Christoph Weidenbach , Max Planck Institut für Informatik

  Automatic Analysis of LAN Infrastructures

  
  

  Important guarantees for LAN infrastructures include connectivity, error detection/recovery, robust changes and security. In the talk I will develop a LAN infrastructure model in first-order logic enabling automatic analysis of such properties. The model starts at the ethernet layer of the TCP/IP stack and ranges up to application protocols such as DHCP.