A framework for formal verification of robot kinematics

DOI10.1016/J.JLAMP.2024.100972MaRDI QIDQ6561341zbMATH OpenFDO

Authors Guojun Xie, Huanhuan Yang, Gang Chen

Publication date 25 June 2024

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.JLAMP.2024.100972

zbMATH Keywords

coordinate conversionCoq proof assistantformal methods in robotics and automationformal verificationkinematics

Mathematics Subject Classification ID

Computer science (68-XX)

Cites work

• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
• Coquelicot: a user-friendly library of real analysis for Coq
• Formal analysis of the kinematic Jacobian in screw theory
• Formalization of camera pose estimation algorithm based on Rodrigues formula
• Formalization of Euler-Lagrange equation set based on variational calculus in HOL light
• Formalization of operations of block matrix based on Coq
• Formalization of the inverse kinematics of three-fingered dexterous hand
• Parameterized verification of algorithms for oblivious robots on a ring
• Untyping typed algebras and colouring cyclic linear logic
• Verification of the ROS NavFn planner using executable specification languages

Cited in

(1)

• Vector polynomial based analytical inverse kinematics and configuration design of 6R robotic arms

This page was built for publication: A framework for formal verification of robot kinematics

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