Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Tue 19 Jan 2021 16:00 - 17:00 at VMCAI - Invited talk

In this paper we position Linear Time Temporal Logic (LTL), structural operational semantics (SOS), and a graphical generalization of BNF as central DSLs for program analysis and verification tasks in order to illustrate the impact of language to the mindset: (1) Specifying program analyses in LTL changes the classical algorithmic ‘HOW’ thinking into a property-oriented ‘WHAT’ thinking that allows one to logically combine analysis goals and eases proofs. (2) Playing with the original store component in SOS configurations allows one to elegantly realize variants of abstract program interpretations, and to align different aspects, like e.g., the symbolic values of variables and path conditions. (3) Specializing languages by refining their BNF-like meta models has the power to lift certain verification tasks from the program to the programming language level. We will illustrate the advantages of the change of mindset imposed by these three DSLs, as well as the fact that these advantages come at low price due to available adequate generator technology.

Tue 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:00: Invited talkVMCAI at VMCAI
16:00 - 17:00
Generative Program Analysis and Beyond: The Power of Domain-Specific Languages
I: Bernhard SteffenTU Dortmund, Alnis MurtoviTU Dortmund, David SchmidtKansas State University
Media Attached