A formally verified interpreter for a shell-like programming language

DOI10.1007/978-3-319-72308-2_1MaRDI QIDQ1630019zbMATH OpenOpenAlexFDO

Authors Nicolas Jeannerod, Claude Marché, Ralf Treinen

Publication date 7 December 2018

Full work available at URL https://doi.org/10.1007/978-3-319-72308-2_1

zbMATH Keywords

programming languagedeductive program verificationPOSIX shell

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20)

Recommendations

• Verified functional programming of an abstract interpreter
• TRX: a formally verified parser interpreter
• Structural Abstract Interpretation: A Formal Study Using Coq
• A formally verified compiler back-end
• Formal verification of language-based concurrent noninterference

Cited in

(3)

• Constructing infinitary quotient-inductive types
• A formally proved, complete algorithm for path resolution with symbolic links
• CoLiS

Describes a project that uses

Uses Software

• checkbashisms
• Shellcheck
• E Theorem Prover
• WhyML
• CVC4
• Alt-Ergo
• z3
• cvc3
• Why3
• SPASS

This page was built for publication: A formally verified interpreter for a shell-like programming language

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1630019)