Extracting and exploiting invariants for solving PBESs ------------------------------------------------------ Invariants play an important role in the verification of programs. In the setting of parameterised Boolean equation systems (PBESs) [1], invariants have received relatively little attention, but the investigations in [2] suggest that invariants have the potential to speed up solving several classes of PBESs in practice. However, several challenges remain before invariants can be exploited in practice. These include: 1. investigations into efficient techniques for generating and extracting invariants from arbitrary PBESs; these include techniques described in the program verification literature but also developing new techniques tailored to the domain of PBESs. 2. integrate extracted invariants in a suitable way in existing tools for solving PBESs; these include explicit solving techniques which rely on extracting and solving parity games from a PBES, but also symbolic techniques which rely on symbolic bisimulation minimisation to deal with infinite data types, or symbolic techniques to efficiently store very large graph structures. [1] Jan Friso Groote, Tim A. C. Willemse: Parameterised boolean equation systems. Theor. Comput. Sci. 343(3): 332-369 (2005) [2] Simona Orzan, Tim A. C. Willemse: Invariants for Parameterised Boolean Equation Systems. Theor. Comput. Sci. 411(11-13): 1338-1371 (2010)