Link for the site to declare intent to present in the seminar (do not hesitate to register even if there is already aregistered intent)

Past seminars (with slides when provided)

29/03/2022 — 2 Presentations

Who : Dr. Mattias Ulbric’s (https://formal.kastel.kit.edu/~ulbrich/)
Title: Regression Verification

Abstract:
The standard technique to identify flaws in implementations is regression testing. However, testing can only find those errors that covered by the supplied test cases. Alternatively, formal approaches can used to verify code, but that usually requires a formal specification of the procedures to be analysed.
I’d like to tell you about regression verification where an old version of a programme serves as specification for the new version – thus combining the benefits of testing and formal verification.
I’ll present how we applied this to C programmes and programmable logic controlelrs.

Who : Dr. Soumyadip Bandyopadhyay

Title : Equivalence checking of Petri net based models of programs

Abstract :

Programs are often subjected to significant optimizing and parallelizing transformations based on extensive dependence analysis. Formal validation of such transformations needs modelling paradigms which can capture both control and data dependences in the program vividly.
Being value-based with an inherent scope of capturing parallelism, the untimed coloured Petri net (CPN) models, reported in the literature, fit the bill well; accordingly, they are likely to be more convenient as the intermediate representations (IRs) of both the source and the transformed codes for translation validation than strictly sequential
variable-based IRs like sequential control flow graphs (CFGs). In this talk , several path-based equivalence checking methods 
for CPN models of programs on integers are presented.