Techniques and tools for verification and certification of program completion

Abstract

One of the most interesting practical problems from a scientific and technological point of view is the termination of computer programs and systems. When a program is not terminating, this circumstance manifests itself in the software system that executes it (usually without the user being aware that its origin lies in this type of error) in the form of system crashes that require a total or partial restart. In this sense, the automatic verification of termination properties is of clear industrial interest. The use of concepts, methods and techniques from rule-based programming in the construction, analysis and verification of software and computer systems has a long history, although it continues to enjoy considerable popularity and in recent years has received renewed interest from different areas of computer engineering. In this field, we have developed new techniques that are applicable to the verification and certification of termination properties of computer programs and systems: commands, algebraic methods, use of logics and associated algorithms, arithmetic constraint solving, transformations, etc. This technology has been implemented in various tools that can be used through interfaces based on web services.

Scientific officer

Lucas Alba Salvador

Stakeholders

Applications

  • Verification and certification of the completion of different variants of rule-based systems.
  • Verification and certification of the termination of Maude programs.
  • Verification and certification of termination of different kinds of rule-based systems.
  • Verification and certification of termination of Maude programs.
  • Efficient resolution of arithmetic constraints.

Technical advantages

Techniques and tools developed on a solid formal basis.

Benefits it provides

  • Automatic verification and certification of termination properties of programs and computational systems.
  • Automatic verification and certification of termination properties of programs and computational systems.
  • Efficient resolution of arithmetic constraints.

Relevant experience

The ELP group, created in 1989, is identified in the registry of consolidated research groups of the Generalitat Valenciana since October 2000 (key GR-00143). The group’s activity has been mainly related to multi-paradigm programming languages and rigorous methods for software development, focusing on rule-based programming and the use of abstract interpretation techniques and transformation techniques for the optimization of program execution. Rule-based languages have also been the basis for inductive programming and for the representation of complex but understandable models resulting from the extraction of knowledge from data (data mining). The ELP group has participated in more than 30 competitive projects financed with European, national and community funds. Its research activity has often been developed in connection with related groups based in foreign universities, including Germany (RWTH Aachen, U. of Kiel), Australia (Monash U.), Austria (Technische Universitat Wien), United States (U. of Illinois at Urbana-Champaign, National Research Laboratory, Portland State U., Washington, Stanford), France (- U. of Illinois at Urbana-Champaign, National Research Laboratory, Portland State U., Stanford University), France (- U. of Illinois at Urbana-Champaign, National Research Laboratory, Portland State U, Washington, Stanford), France (-‘Ecole Polytechnique, U. Grenoble, U. Nice, U. de Paris Sud), Italy (U. di Pisa, U. di Siena, U. di Udine) and United Kingdom (U. Bristol). The group has participated in several projects with companies where the group’s knowledge has been transferred or specific technology has been developed. The range of sectors in which the group has worked includes, logically, IT and consulting companies, but also companies ranging from distribution to hospital management. // The group ELP, created in 1989, was recognized as a consolidated group of the Valencian Government in October 2000 (reference GR-00143). The group’s activities have mainly focused on multi-paradigm programming languages and rigurous methods for software development, with particular focus on rule–based programming, and the use of abstract interpretation and program transformation techniques for the optimization of program execution. Rule-based languages have been also used for inductive programming and complex model representation that are also comprehensible as a result of knowledge discovering (data mining). The ELP group has participated in more than 30 competitive research projects funded by the EU, the Spanish Research Funding Agency, and other European foundations. The group keeps a good record of international collaborations. Including Germany (RWTH Aachen, U. Kiel), Australia (Monash U.), Austria (Technische Universit-“at Wien), USA (U. of Illinois at Urbana-Champaign, National Research Laboratory, Portland State U., Washington, Stanford), France (-‘Ecole Polytechnique, U. Grenoble, U. Nice, U. Paris Sud), Italy (U. di Pisa, U. di Siena, U. di Udine) and UK (U. Bristol). The Group also keeps a good record of collaboration with industry, including IT companies as well as hospital management and distribution companies.