Translating Xd-C programs to MSVL programs

DOI10.1016/j.tcs.2019.12.038zbMath1436.68077arXiv1809.00959MaRDI 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

verification; translation; model checking; C language; MSVL

Mathematics Subject Classification ID

68N15: Theory of programming languages

68N20: Theory of compilers and interpreters

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

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