Model Checking MSVL Programs Based on Dynamic Symbolic Execution

DOI10.1007/978-3-319-21398-9_41MaRDI QIDQ3196412zbMATH OpenOpenAlexFDO

Authors Zhenhua Duan, Kangkang Bu, Cong Tian, Nan Zhang

Publication date 29 October 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-21398-9_41

zbMATH Keywords

constraintsmodel checkingtemporal logicMSVLDSE

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1956607
• scientific article; zbMATH DE number 1507203
• Symbolic model checking of software
• Symbolic and structural model-checking
• Symbolic bounded conformance checking of model programs
• Symbolic model checking with rich assertional languages
• The automatic verification using symbolic model-checking

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 52331 (Why is no real title available?)
• A practical decision procedure for propositional projection temporal logic with infinite models
• Program analysis via satisfiability modulo path programs
• Symbolic execution and program testing
• Verification of distributed systems with the axiomatic system of MSVL

Cited in

(1)

• Translating Xd-C programs to MSVL programs

Describes a project that uses

Uses Software

• MSV
• VeriFast
• DART
• CUTE

This page was built for publication: Model Checking MSVL Programs Based on Dynamic Symbolic Execution

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