CfPBoK
by
Vadim Zaytsev
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.