LMU

Verification of Non-regular Properties (VeriNonReg)




Project description:

The verification of non-regular program properties involves the investigation of program models which are structurally more complex than usually assumed in this context. Non-regularity is here to be understood in the sense of formal language theory, i.e. regarding the more expressive segments of the Chomsky hierarchy such as the context-free or context-sensitive languages. In order to capture these languages, a similarly increasing expressivity is needed on the specification side.

Several different logics capable of expressing context-free and context-sensitive properties have been proposed in the literature (follow the links to see a list of publications/ information):

  • Fixed Point Logic with Chop (FLC)
  • Higher Order Fixpoint Logic (HFL)
  • Propositional Dynamic Logic of non-regular grammars (PDL[CFG], PDL[IG])
  • Modal Iteration Calculus (MIC)

Example properties are unlimited counting, absence of buffer underflows (for unlimited buffer sizes) or bisimilarity to a balanced tree, just to name a few. The project aims at comparing these logics regarding expressivity and to develop model checking algorithms for them. As expressivity increases, the meaning of "model checking" is less restricted to "method used in program verification" but must be viewed as a general logic problem in which various important and general problems can be encoded. It is for example possible to solve universality of nondeterministic finite automata, satisfiability of modal logic K and evaluation of quantified boolean formulas as instances of the model checking problem for the first-order fragment of HFL (HFL1).

Taking a model checking algorithm as a template to analyze problem structures bears a high potential for optimizations, in particular, if we take into account that the formulas for these logics are typically fixed regardless of the input size.

Formulas of the above logics tend to be difficult to read. Simplifications of the logical syntax (maybe at the cost of lesser expressivity) are desirable with regard to the development of verification tools that can be used by engineers without a formal background. The goal here is to extract fragments of these logics for which intuitive specification languages can be provided.


Software:

The following implementations of model checkers are available for download:


Literature:

A list of publications about the above logics is being kept up to date.
If we missed a paper, please let us know: to make mail visible: move mouse over

Involved People:


Funding:

The project is funded by the DFG.




Last modified: Thu Jun 26 17:29:07 2008