Bounded symbolic execution for runtime error detection of Erlang programs

MaRDI QIDQ3384903zbMATH OpenFDO

Authors Emanuele De Angelis, Fabio Fioravanti, Adrián Palacios, Alberto Pettorossi, Maurizio Proietti

Publication date 17 December 2021

Full work available at URL https://arxiv.org/abs/1809.04770, http://eptcs.web.cse.unsw.edu.au/paper.cgi?HCVS2018.4

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Towards symbolic execution in Erlang
• Polymorphic success types for Erlang
• Polymorphic types in Erlang function specifications
• Verification of Erlang programs using abstract interpretation and model checking
• Preemptive Type Checking in Dynamically Typed Languages

Cites work

• A rule-based verification strategy for array manipulating programs
• An iterative approach to precondition inference using constrained Horn clauses
• scientific article; zbMATH DE number 997344 (Why is no real title available?)
• Optimal dynamic partial order reduction
• Predicate pairing for program verification
• Program Development in Computational Logic
• Program verification using constraint handling rules and array constraint generalizations
• Verifying Array Programs by Transforming Verification Conditions

This page was built for publication: Bounded symbolic execution for runtime error detection of Erlang programs

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