Translating Xd-C programs to MSVL programs

DOI10.1016/j.tcs.2019.12.038zbMath1436.68077arXiv1809.00959OpenAlexW2998781949WikidataQ126398570 ScholiaQ126398570MaRDI QIDQ2290648

Nan Zhang, Meng Wang, Zhenhua Duan, Cong Tian, Chenguang Yao

Publication date: 29 January 2020

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1809.00959

zbMATH Keywords

verificationtranslationmodel checkingC languageMSVL

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

C2M

Uses Software

• BLAST
• SPIN
• NuSMV
• CPAchecker
• CBMC
• RiTHM
• LTLAutomizer
• MinGW
• UMC4M
• MSVL

Cites Work

• Unnamed Item
• Unnamed Item
• A mechanism of function calls in MSVL
• A practical decision procedure for propositional projection temporal logic with infinite models
• A compiler for MSVL and its applications
• Fairness modulo theory: a new approach to LTL software model checking
• Efficient abstraction algorithms for predicate detection
• Operational semantics of Framed Tempura
• Kernel P systems: from modelling to verification and testing
• Tools and algorithms for the construction and analysis of systems. 20th international conference, TACAS 2014, held as part of the European joint conferences on theory and practice of software, ETAPS 2014, Grenoble, France, April 5--13, 2014. Proceedings
• Framed temporal logic programming
• A decision procedure for propositional projection temporal logic with infinite models
• Mechanized semantics for the clight subset of the C language
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Lazy abstraction