| [1] |
Ayub MS, Hasan O (2017) Formal probabilistic analysis of a virtual fixture control algorithm for a surgical robot. In: Verification and evaluation of computer and communication systems, volume 10466 of LNCS, pp 1-16. Springer |
| [2] |
Bianco A, De Alfaro L (1995) Model checking of probabilistic and nondeterministic systems. I:n Foundations of software technology and theoretical computer science, volume 1026 of LNCS, pp 499-513. Springer · Zbl 1354.68167 |
| [3] |
Bresolin, D.; Geretti, L.; Muradore, R.; Fiorini, P.; Villa, T., Formal verification of robotic surgery tasks by reachability analysis, Microprocess Microsyst, 39, 8, 836-842 (2015) · doi:10.1016/j.micpro.2015.10.006 |
| [4] |
Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press (1999) · Zbl 1423.68002 |
| [5] |
Clarke EM, Klieber W, Nováček M, Zuliani P (2012) Model checking and the state explosion problem. In: Tools for practical software verification, volume 7682 of LNCS, pp 1-30. Springer |
| [6] |
Dawood H (2011) Theories of interval arithmetic: mathematical foundations and applications. LAP Lambert Academic Publishing |
| [7] |
Durán AJ, Pérez M, Varona JL (2013) The misfortunes of a mathematicians’ Trio using computer algebra systems: can we trust? CoRR. arXiv:1312.3270 · Zbl 1338.68299 |
| [8] |
Faroque M, Nizam S (2016) Virtual reality training for micro-robotic cell injection. Technical report, Deakin University, Australia |
| [9] |
Gordon Michael JC (1988) HOL: a proof generating system for higher-order logic. In: VLSI specification, verification and synthesis, volume 35 of SECS, pp 73-128. Springer |
| [10] |
Harrison J (1996) HOL light: a tutorial introduction. In: Srivas M, Camilleri A (eds) Proceedings of the first international conference on formal methods in computer-aided design (FMCAD’96), volume 1166 of LNCS, pp 265-269. Springer-Verlag |
| [11] |
Harrison J (1996) HOL light: a tutorial introduction. In: Formal methods in computer-aided design, volume 1166 of LNCS, pp 265-269. Springer |
| [12] |
Harrison, J.: Handbook of practical logic and automated reasoning. Cambridge University Press (2009) · Zbl 1178.03001 |
| [13] |
Harrison J(2013) The HOL light theory of euclidean space. J Autom Reason 1-18 · Zbl 1260.68373 |
| [14] |
HOL Light Multivariate Calculus (2020) https://github.com/jrh13/hol-light/blob/master/Multivariate |
| [15] |
HOL Light Real Calculus (2020) https://github.com/jrh13/hol-light/blob/master/Multivariate/realanalysis.ml |
| [16] |
HOL Light Transcendentals (2020) https://github.com/jrh13/hol-light/blob/master/Multivariate/transcendentals.ml |
| [17] |
HOL Light Vectors and Matrices (2020) https://github.com/jrh13/hol-light/blob/master/Multivariate/vectors.ml |
| [18] |
Huang, H.; Sun, D.; Mills, JK; Li, WJ; Cheng, SH, Visual-based impedance control of out-of-plane cell injection systems, Trans Autom Sci Eng, 6, 3, 565-571 (2009) · doi:10.1109/TASE.2008.2010013 |
| [19] |
Huang H, Sun D, Mills JK, Li Wen J (2006) A visual impedance force control of a robotic cell injection system. In: Robotics and biomimetics, pp 233-238. IEEE |
| [20] |
Hasan O, Tahar S (2015) Formal verification methods. In: Encyclopedia of information science and technology, pp 7162-7170. IGI Global Pub |
| [21] |
Kuncova J, Kallio Pasi (2004) Challenges in capillary pressure microinjection. In: Engineering in Medicine and Biology Society, volume 2, pp 4998-5001. IEEE |
| [22] |
Kouskoulas Y, Renshaw D, Platzer A, Kazanzides P (2013) Certifying the safe design of a virtual fixture control algorithm for a surgical robot. In: Hybrid systems: computation and control, pp 263-272. ACM |
| [23] |
Maple (2020) https://www.maplesoft.com/ |
| [24] |
Mathematica (2020) https://www.wolfram.com/mathematica/ |
| [25] |
Nakayama, T.; Fujiwara, H.; Tastumi, K.; Fujita, K.; Higuchi, T.; Mori, T., A new assisted hatching technique using a piezo-micromanipulator, Fertil Steril, 69, 4, 784-788 (1998) · doi:10.1016/S0015-0282(98)00017-X |
| [26] |
Nethery, JF; Spong, MW, Robotica: a mathematica package for robot analysis, IEEE Robot Autom Mag, 1, 1, 13-20 (1994) · doi:10.1109/100.296449 |
| [27] |
Paulson, L.C.: ML for the working programmer. Cambridge University Press (1996) · Zbl 0863.68032 |
| [28] |
Rashid A (2020) Formal verification of robotic cell injection systems upto \(4\)-DOF using HOL Light. http://save.seecs.nust.edu.pk/fvrcis/ |
| [29] |
Rashid A, Hasan O (2017) Formal analysis of robotic cell injection systems using theorem proving. In: Design, modeling, and evaluation of cyber physical systems, volume 11267 of LNCS, pp 127-141. Springer |
| [30] |
Rashid A, Hasan O (2018) Formal modeling of robotic cell injection systems in higher-order logic. In: Formal verification of physical systems, volume 2307, pp 1-9. CEUR-WS |
| [31] |
Sardar MU, Hasan O (2017) Towards probabilistic formal modeling of robotic cell injection systems. In: Models for formal analysis of real systems, pp 271-282 |
| [32] |
Sun D, Liu Y (1997) Modeling and impedance control of a two-manipulator system handling a flexible beam. In: Proceedings of 1997 IEEE International Conference on Robotics and automation, volume 2, pp 1787-1792. IEEE |
| [33] |
Sun, Y.; Nelson, BJ, Biological cell injection using an autonomous microrobotic system, Robot Res, 21, 10-11, 861-868 (2002) · doi:10.1177/0278364902021010833 |
| [34] |
Yanagida, K.; Katayose, H.; Yazawa, H.; Kimura, Y.; Konnai, K.; Sato, A., The usefulness of a piezo-micromanipulator in intracytoplasmic sperm injection in humans, Hum Reprod, 14, 2, 448-453 (1999) · doi:10.1093/humrep/14.2.448 |
