Keynote Speakers

TITLE: FormalISE: Reflections on Formal and Informal Methods in Software Engineering

ABSTRACT: In this talk, I reflect on formal and informal methods that are, or are becoming available to software engineers, ranging from manual testing to static analysis, fuzzing, symbolic execution and formal verification. These reflections are shaped by my experiences designing and applying different forms of program analysis techniques (with a focus on the middle ground between formal and informal methods) to a wide range of software systems and software engineering problems.

TITLE: Two-way collaboration between flow and proof in SPARK

ABSTRACT: There are various kinds of static (and dynamic) verification frameworks and tools, all with weaknesses and strengths. Combining them manually or automatically is common by making different tools interoperate or integrating various analyses in the same tool. In SPARK, two analyses work on different paths: deductive verification and data and information flow analysis. This talk presents how these analyses collaborate to improve the efficiency and precision of the SPARK tool while retaining soundness.