Scientific projects

COST (European Cooperation in Science and Technology) CA20111
11. October 2021 to 10. October 2025

If testing can reveal errors in computer programs, only formal verification can guarantee their absence. The highest Evaluation Assurance Levels of the Common Criteria for Information Technology Security Evaluation require automatically checked mathematical proofs of correctness. Proofs are also the basis of mathematics and many sciences, and thus are very important in education and research.

In many computer technologies, developers and users rely on standard languages and protocols for exchanging data and enabling tool interoperability: TCP/IP for network communication, HTML for web pages, etc. This is however not the case for formal proofs, which is a major bottleneck for their adoption by the industry. The main reason is that, currently, proof systems use mutually incompatible logical foundations. Fortunately, only small parts of the proofs developed in a system use features that are incompatible with other systems.

Europe is a leading actor in the area of formal proofs: about 65% of the proof systems of the world are developed in Europe, including the two most used proof assistants, Coq and Isabelle.

This Action aims at boosting the interoperability and usability of proof systems and making formal proofs enter a new era. For the first time, it gathers all the developers and users of proof systems in Europe. To make the proofs exchangeable, they will express, in a common logical framework, the logical foundations of their systems and develop tools for inter-translation of the proofs developed in individual systems to and from this common logical framework.

Principal Investigator:
Ing. Ján Perháč PhD.
VEGA 1/0762/19
1. January 2019 to 11. December 2021

The goal of this project is to explore novel approaches to formal language design and implementation. They should be based on synthesis of methods from the fields of formal languages, human-computer interaction and data analysis.
Language design and implementation process should be interactive and explorative activity, where language designer is able to experiment with design of the language notation and associated tools and immediately adjust language definition based on the results. To achieve this it would be required to design new methods for automated inference of language specification based on abstract syntax, example sentences and interaction with language designer.

Principal Investigator:
prof. Ing. Jaroslav Porubän PhD.

Educational projects

ERASMUS+ KA203 - Strategic partnership for higher education 2020-1-PT01-KA203-078646
1. September 2020 to 31. August 2023

Project Coordinator of KPI:
doc. Ing. Csaba Szabó PhD.