Abstraction and model checking of core Erlang programs in Maude

DOI10.1016/J.ENTCS.2007.06.013MaRDI QIDQ2873779zbMATH OpenOpenAlexFDO

Authors Martin Neuhäußer, Thomas Noll

Publication date 24 January 2014

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2007.06.013

zbMATH Keywords

Erlangformal verificationfunctional programmingMauderewriting logic

Mathematics Subject Classification ID

Logic programming (68N17) Functional programming and lambda calculus (68N18) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Equational abstractions for model checking Erlang programs
• Verification of Erlang programs using abstract interpretation and model checking
• Towards Erlang verification by term rewriting
• Model checking Erlang programs -- abstracting recursive function calls
• scientific article; zbMATH DE number 2090137

Cites work

• Conditional rewriting logic as a unified model of concurrency
• Rewriting logic: Roadmap and bibliography
• Specification and proof in membership equational logic
• The revised report on the syntactic theories of sequential control and state

Cited in

(17)

• A proof assistant based formalisation of a subset of sequential core Erlang
• Strategies, model checking and branching-time properties in Maude
• Program equivalence in an untyped, call-by-value functional language with uncurried functions
• scientific article; zbMATH DE number 1691455 (Why is no real title available?)
• Verification of Erlang programs using abstract interpretation and model checking
• Model checking Erlang programs -- abstracting recursive function calls
• Equational abstractions for model checking Erlang programs
• Towards Erlang verification by term rewriting
• Towards symbolic execution in Erlang
• scientific article; zbMATH DE number 1942462 (Why is no real title available?)
• scientific article; zbMATH DE number 2090137 (Why is no real title available?)
• Model checking strategy-controlled rewriting systems
• Equational abstractions for reducing the state space of rewrite theories
• Computer Aided Systems Theory – EUROCAST 2005
• Verification of Erlang processes by dependency pairs
• Playing with bisimulation in Erlang
• A formalisation of Core Erlang, a concurrent actor language

Describes a project that uses

Uses Software

• Maude
• Erlang

This page was built for publication: Abstraction and model checking of core Erlang programs in Maude

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