We are a group of mainly professors and students interested in applying formal methods to various domains. We typically meet on Wednesdays, at 6 PM, in 045 C, at UVT main building.
By formal methods we understand applying symbolic computation methods, in particular computational logic, to rigorously reasoning about properties of computer programs. Relevant program property is correctness with respect to a specification.The term formal methods refers to both modeling the system/software as mathematical entities and to the (automated) verification process of system properties in a throughout fashion.
Hence, formal methods comprise of at least two aspects. Specification means to describe the conditions on the input program variables (precondition) and the expected behavior of a program (output condition) in a mathematically precise way.
(Complete) verification means to demonstrate using mathematical rigor that every possible execution of the program does not crash and indeed satisfies its specification, preferably with computer support (automated reasoners, SAT/SMT solving).Many times, the complete verification of a program may is not feasible, hence a loose approach is used to increase the confidence in the correctness of a program:
Also the loose approach is supported by automatic tools like static program analyzers, model checkers, etc.
In the Winter Semester 2019/2020, we will focus on the verification of binarized neural networks.
Contact: Mădălina ERAŞCU.