sle2024s/paper06

SLE 2024 SI paper:
Translating meaning representations to behavioural interface specifications

Iat Tou Leong, Raul Barbosa

• DOI: 10.1016/j.jss.2024.112009
• Extended version of Translating Natural Language Requirements to Formal Specifications: A Study on GPT and Symbolic NLP (DSN-W 2023)
• T5D: Formal Methods
  • The output artifacts are formal behavioural interface specifications (JML contracts) and they are checked with verification tooling/theorem proving.
• T4G: AI-for-SLE
  • The pipeline leverages NLP meaning representations and resolves ambiguities to translate natural language semantics into formal specs.
• T2E: Documentation
  • The source of specifications is developer documentation (method-level comments), turning documentation into machine-checkable contracts.
• T5A: Requirements
  • It operationalizes (textual) requirements/intended behaviour stated in natural language into precise formal pre/postconditions.

---

The page is maintained by Dr. Vadim Zaytsev a.k.a. @grammarware. Last updated: June 2026.