Model Checking MSVL Programs Based on Dynamic Symbolic Execution

DOI10.1007/978-3-319-21398-9_41zbMath1465.68176OpenAlexW2295344041MaRDI QIDQ3196412

Nan Zhang, Zhenhua Duan, Cong Tian, Kangkang Bu

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

model checkingtemporal logicconstraintsMSVLDSE

Mathematics Subject Classification ID

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

Uses Software

• CUTE
• DART
• VeriFast
• MSV

Cites Work

• A practical decision procedure for propositional projection temporal logic with infinite models
• Verification of distributed systems with the axiomatic system of MSVL
• Symbolic execution and program testing
• Program analysis via satisfiability modulo path programs
• Unnamed Item
• Unnamed Item