A project of SQIG at IT partially supported by FCT and EU FEDER, namely via projects KLog PTDC/MAT/68723/2006, QSec PTDC/EIA/67661/2006 and AMDSC UTAustin/MAT/0057/2008.
The problem addressed by the initiative is the verification of non-deterministic, probabilistic and quantum programs and protocols. In many applications it is critical to ensure that the program/protocol works as intended. Tests are widely used but they can only detect errors, never prove their absence. When correctness is essential, formal proof techniques or model checking techniques are used instead. The former usually adopt specific logics and require skill not common among practitioners. The latter has found wider acceptance by the industry because of its high degree of automation and less requirements from the practitioner. Recent interest in the verification of probabilistic and quantum systems posed challenging problems to these approaches.
Inspired by our experience in quantum logic, our key idea is to adopt linear algebra as the lingua franca of software verification. Indeed, we can look at a program (even a classical one) as a linear transformation over a suitable vector space, whose vectors represent the states of our system. Additionally, we can also look at valuation-dependent terms as scalar transformations, valuation-dependent properties as projectors and parallel composition of programs as tensor product. Hence, linear algebra can and should be used for reasoning about programs, which include the particular case of ping-pong protocols, that is, protocols without true paralelism. We propose to adopt general reasoning techniques of linear algebra to the particular case of programs. In addition, we also aim at developing algorithms for reasoning about such programs by adapting numerical methods in finite dimensional linear algebra to the case at hand. This adaptation is feasible only in the case of programs with finite space resources, but not necessarily time bounded. Later on we will also consider the infinite dimension case.
AMS-MSC 68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)