From PUMA Graduiertenkolleg
One key application of program and model analysis is to exhibit programming errors or to certify that the program behaves according to a given specification. Specification can range from simply demanding the absence of typical errors like null pointers dereferences to providing precise qualitative and quantitative descriptions of the desired behaviour, like e.g. the allowed resource consumption.
The current four leading approaches to such analysis/certification problems are:
Program Verification through Theorem Proving
The logical view of programming as initiated by Hoare and Dijkstra is fundamental to Computer Science and the basis for program verification. Research in this area is dominated by the development of logical systems for various programming language constructs, e.g., for concurrency or object-orientation.
In the early 80s model-checking was developed for automatically verifying temporal properties of concurrent systems, like absence of deadlock. Model-checking is based on the exhaustive exploration of the state space of the system. A major break-through for the verification of hardware compondents was achieved by means of symbolic algorithms based on binary decision diagrams.
Static Analysis and Abstract Interpretation
In contrast to theorem provers and model-checkers, the first static analyses were not developed for verification purposes, but as a way to automatically infer semantic information about programs for later use in an optimizing compiler. However, the approximative methods developed in this context have proved to be extremely useful for proving the absence of certain programming errors or computing program invariants.
Type systems approximate the program semantics by suitable inductive definitions. Types can be automatically inferred, often using algorithms originally developed in one of the other areas. Semantic correctness of the analysis and inference thus are de-coupled. This makes type systems particularly suitable for situations where semantic correctness is non-obvious.
Each of the four approaches above is supported by a strong international community and by a large number of success stories. In the last years the approaches have started to interact, leading to significant progress in their realization into algorithms and tools. A good example is "predicate abstraction", a technique used by tools for the verification of C programs like Slam, Blast or Magic. Originally developed for the theorem prover PVS, predicate abstraction now allows to apply classical ideas from abstract interpretation in model-checking-based tools. It is an excellent example of the large potential of hybrid methods combining the results from different areas.
We consider the interface between approaches as one of the most exciting research areas in the field of formal methods, and the right place for PUMA's programme.
Application: Software-Intensive Systems
Software increasingly becomes a central component of applications, products and services in all areas of industry, business and administration. Systems where software interacts, controls, or communicates with devices, sensors, and humans are called software-intensive. Examples include systems from the automotive industries, avionics, tele-comunication, wireless adhoc networks, e-business applications based on web services, robotics and many more.
Since software-intensive systems more and more occupy our private and professional lives, their quality and reliability are substantial for technological progress, economic success and convenience of our private activities.
Today, despite their immense importance, software-intensive systems are not well understood. Mobile phones, e.g., can catch viruses, the introduction of large administration applications is delayed due to modelling errors, and many business transactions over the internet fail for technical reasons.
The methods and tools for modelling and analysis currently used in practice are not strong enough for the development of increasingly distributed, heterogeneous, and de-centralized software-intensive systems which have to be deployed in dynamic, rapidly changing environments. Analysis techniques with a solid theoretical foundation and adequate pragmatic methods are badly needed to link models with formal analysis and verification tools.