A compiler for MSVL and its applications

DOI10.1016/J.TCS.2017.07.032MaRDI QIDQ1630985zbMATH OpenOpenAlexWikidataFDO

Authors Kai Yang, Zhenhua Duan, Cong Tian, 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

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

Recommendations

• scientific article; zbMATH DE number 4013996
• A compiler for an algebraic specification language
• A Compiler for an Array and Vector Processing Language
• A practical approach to compiler construction
• scientific article; zbMATH DE number 192911
• scientific article; zbMATH DE number 49476
• An action compiler targeting standard ML

Cites work

• scientific article; zbMATH DE number 1982210 (Why is no real title available?)
• scientific article; zbMATH DE number 2038904 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• scientific article; zbMATH DE number 3421895 (Why is no real title available?)
• A cylinder computation model for many-core parallel computing
• A decision procedure for propositional projection temporal logic with infinite models
• A mechanism of function calls in MSVL
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Fairness modulo theory: a new approach to LTL software model checking
• Linear temporal logic as an executable semantics for planning languages
• Static Analysis
• TALplanner: A temporal logic based forward chaining planner
• Tools and Algorithms for the Construction and Analysis of Systems
• Using temporal logics to express search control knowledge for planning

Cited in

(8)

• Translating Xd-C programs to MSVL programs
• scientific article; zbMATH DE number 1951543 (Why is no real title available?)
• A mechanism of function calls in MSVL
• Generating Java code pairing with ChatGPT
• A novel approach to verifying context free properties of programs
• A temporal logic programming approach to planning
• Efficient decision procedure for propositional projection temporal logic
• Verifying a scheduling protocol of safety-critical systems

Describes a project that uses

Uses Software

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

This page was built for publication: A compiler for MSVL and its applications

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