Practical Formal
Verification Using Automated Reasoning and Model Checking
INTAS
Project |
|
Duration
September 2006 - February 2009
Partners
RISC-Linz (Coordinator)
Sponsored by
INTAS (INTAS Ref. Nr 05-1000008-8144)
Summary of the project
Main objective. The main objective
of the project is to advance the state-of-the-art in proving and checking
techniques for information systems, and to apply them to concrete industrial
problems. In more detail, by using practical problems for testing the different
methods for proving and model checking, we will compare the effectiveness of
different techniques, and we will identify the most appropriate ones, as well
as the necessary adaptations, improvements, and combinations of methods which
are more appropriate for solving industrial problems. In particular, we will
put a special emphasis on combining automated reasoning with model checking,
especially infinite-state model checking. As we want to test these methods in
the context of their usage, a central task of the project is the testing and
improvement of the techniques for program verification and synthesis, as well
as the corresponding methods for finitary problems: circuit synthesis and
verification, and reactive algorithms.
An
important task is the practical demonstration of the various methods in an
industrial context. For this we will develop appropriate standards and tools
for the integration of the methods into a coherent library, supported by an
intelligent user interface in natural language. By direct interaction with
applications, new and interesting theoretical and algorithmic developments will
be initiated.
Economic and impact. By using a comprehensive
dissemination strategy, an important result of the project will be the
increased awareness and acceptance of formal methods in industry, which in turn
will have a benefic impact on the reliability of software and hardware systems,
and information systems in general. The partners will be able to use the
experience from the project, both theoretical and practical, for realizing more
efficient tools, including possible commercial ones, and for performing formal
verification tasks for industrial users.
Research plan. Overall, the
research approach consists in improving formal methods by testing them against
practical problems from industry. For this, the research will follow three main
directions, each having several subtasks:
1.
Proving and checking engines: clausal proving, proving in finite models,
special calculi, natural style, proving for infinite-state systems.
2.
Verification and synthesis: logic aspects of program verification, verification
and synthesis in finite contexts, verification of specifications, model
checking of infinite state systems.
3.
Tools and evaluation: integration, mathematical knowledge bases,
parallelization, user interface, evaluation and dissemination.
Activities
First
meeting, December 10 – 11, 2006
Second
meeting, August 27 – 29, 2007
Third
meeting, May 28 – 30, 2008
Fourth
meeting, February 27 – 28, 2009
Fifth
meeting, May 26 – 27, 2009
Last Modification: July, 2009
[Up] [RISC-Linz] [University] [Search]