Efficient Verification of Lingua Franca Programs

Welcome to the artifact page for our TACAS 2026 submission, titled “Efficient Verification of Lingua Franca Models”.

This page provides the technical report and accompanying artifact prepared to support the paper’s evaluation. It contains:

  1. A longer technical report that provides additional details.
  2. Manually generated Maude models and analysis commands for all 22 LF-Verifier benchmarks, and other case studies, such as the ADAS system and the train door example.
  3. All LF programs, with LF-MC annotations corresponding to the LF-Verifier analysis annotations, which are commented out.
  4. Maude files defining the semantics of the targeted subset of LF.
  5. LF-MC source code.
  6. All Maude models and analysis commands generated by the LF-MC tool.

All references to the authors have been removed to ensure anonymity during the review process.

Technical Report

Efficient Verification tech rep (pdf)

Artifact

Instructions

See the Artifact README for details on building and running the software, including Docker environments.

Last updated: 2025-10-24