<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta />
    <article-meta>
      <title-group>
        <article-title>Language Workbenches: Opportunities and Challenges for V&amp;V</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>Markus Völter</string-name>
        </contrib>
      </contrib-group>
      <abstract>
        <p>of keynote speech at MoDeVVa 2014 Voelter ingenieurbüro für softwaretechnologie http://www.voelter.de/ Language workbenches (LWBs) are tools that support the efficient construction of languages. Several LWBs support modular extension and composition of languages, as well as flexibly mixing diverse notational styles in a single model. This has obvious advantages for V&amp;V: languages of different levels of abstraction and levels of formality can be integrated, verification-specific extensions can be modularly introduced and validation is more efficient because programs can be much more readable as a consequence of domainspecific notations. But there are also challenges: - How can verification tools deal with (potentially unknown) extensions to the subject languages? - Can the semantics implied by language extensions be exploited to speed up the verification? - Can the semantics of extensions be proven to be equivalent to their lower-level representation? In this talk I illustrate the opportunities an challenges based on mbeddr1, an extensible set of integrated languages for embedded software development built with the JetBrains MPS language workbench. My hope is that the opportunities help establish LWBs as a tool in the V&amp;V community, and the challenges inspire discussions in the workshop and research after the conference.</p>
      </abstract>
    </article-meta>
  </front>
  <body />
  <back>
    <ref-list />
  </back>
</article>