A compiler for MSVL and its applications

DOI10.1016/j.tcs.2017.07.032zbMath1407.68096OpenAlexW2742794271WikidataQ121774302 ScholiaQ121774302MaRDI QIDQ1630985

Kai Yang, Cong Tian, Zhenhua Duan, Nan Zhang

Publication date: 5 December 2018

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

Full work available at URL: https://doi.org/10.1016/j.tcs.2017.07.032

zbMATH Keywords

verificationmodel checkingAI planningcompilerMSVL

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items

Verifying a scheduling protocol of safety-critical systems ⋮ A temporal logic programming approach to planning ⋮ Efficient decision procedure for propositional projection temporal logic ⋮ Translating Xd-C programs to MSVL programs ⋮ A novel approach to verifying context free properties of programs

Uses Software

• BLAST
• SPIN
• NuSMV
• LLVM
• CBMC
• JPAX
• RiTHM
• SHOP2

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A mechanism of function calls in MSVL
• A cylinder computation model for many-core parallel computing
• Linear temporal logic as an executable semantics for planning languages
• TALplanner: A temporal logic based forward chaining planner
• Fairness modulo theory: a new approach to LTL software model checking
• Using temporal logics to express search control knowledge for planning
• A decision procedure for propositional projection temporal logic with infinite models
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Tools and Algorithms for the Construction and Analysis of Systems
• Static Analysis