Speaker: Laura Kovács

Abstract: Despite the substantial progress in the computer-aided verification of computer systems, ensuring the correctness of programs implementing algebraic operations is still an open problem. This problem remains unsolved even when we restrict consideration to loops that are non-nested, without exit conditions, and/or only use limited (polynomial) arithmetic.Such programs naturally arise in compiler optimization, cryptography, cybersecurity, control theory, and probabilistic reasoning. This talk will present classes of computer systems for which we automatically can solve the challenge of proving programs error-free. Key to our setting is the combination of algebraic techniques with static code analysis, allowing us to even turn some unsolvable verification challenges into solvable ones.