{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T16:40:02Z","timestamp":1746204002890,"version":"3.40.4"},"reference-count":81,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2014,3,1]],"date-time":"2014-03-01T00:00:00Z","timestamp":1393632000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Math.Comput.Sci."],"published-print":{"date-parts":[[2014,3]]},"DOI":"10.1007\/s11786-014-0175-z","type":"journal-article","created":{"date-parts":[[2014,4,30]],"date-time":"2014-04-30T05:22:17Z","timestamp":1398835337000},"page":"39-70","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Formal Analysis of Optical Systems"],"prefix":"10.1007","volume":"8","author":[{"given":"Sanaz","family":"Khan-Afshar","sequence":"first","affiliation":[]},{"given":"Umair","family":"Siddique","sequence":"additional","affiliation":[]},{"given":"Mohamed Yousri","family":"Mahmoud","sequence":"additional","affiliation":[]},{"given":"Vincent","family":"Aravantinos","sequence":"additional","affiliation":[]},{"given":"Ons","family":"Seddiki","sequence":"additional","affiliation":[]},{"given":"Osman","family":"Hasan","sequence":"additional","affiliation":[]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,5,1]]},"reference":[{"key":"175_CR1","unstructured":"Allen, L., Angel, R., Rodney, G.A., Mangus, J.D., Shannon, R.R. , Spoelhof, Ch.P.: The Hubble Space Telescope Optical System Failure Report. Technical Report, NASA TM-103443, Washington, DC, November 1990"},{"key":"175_CR2","unstructured":"Formal analysis of optical systems, Hardware Verification Group, Concordia University. http:\/\/hvg.ece.concordia.ca\/projects\/optics\/ (2014). Accessed 20 Mar 2014"},{"key":"175_CR3","unstructured":"Mathematica. http:\/\/www.wolfram.com\/ (2014). Accessed 20 Mar 2014"},{"key":"175_CR4","unstructured":"Mathlink Link. http:\/\/reference.wolfram.com\/mathematica\/guide\/MathLinkAPI.html (2014). Accessed 20 Mar 2014"},{"key":"175_CR5","unstructured":"Matlab\u2013codev toolkit. http:\/\/opensource.gsfc.nasa.gov\/projects\/Matlab_Code_V\/ (2014). Accessed 20 Mar 2014"},{"key":"175_CR6","unstructured":"Matlab\u2013zemax toolkit. http:\/\/opensource.gsfc.nasa.gov\/projects\/Matlab_Zemax\/ (2014). Accessed 20 Mar 2014"},{"key":"175_CR7","unstructured":"OpenMath Content Dictionaries. http:\/\/www.openmath.org\/cdnames.html (2014). Accessed 20 Mar 2014"},{"key":"175_CR8","unstructured":"OpenMath Content Dictionary: linalgeig1. http:\/\/www.win.tue.nl\/~amc\/oz\/om\/cds\/linalgeig1.xml (2014). Accessed 20 Mar 2014"},{"key":"175_CR9","unstructured":"Overview of OpenMath. http:\/\/www.openmath.org\/overview\/index.html (2014). Accessed 20 Mar 2014"},{"key":"175_CR10","unstructured":"Rezonator. http:\/\/www.rezonator.orion-project.org\/ (2014). Accessed 20 Mar 2014"},{"key":"175_CR11","unstructured":"Source Code of the Phrasebook Mathematica-OpenMath. http:\/\/mathdox.org\/new-web\/index.html (2014). Accessed 20 Mar 2014"},{"key":"175_CR12","unstructured":"Zemax. https:\/\/www.radiantzemax.com\/ (2014). Accessed 20 Mar 2014"},{"issue":"2","key":"175_CR13","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1002\/cphc.201100757","volume":"13","author":"M. Baaske","year":"2012","unstructured":"Baaske M., Vollmer F.: Optical resonator biosensors: molecular diagnostic and nanoparticle detection on an integrated platform. Chem. Phys. Chem. 13(2), 427\u2013436 (2012)","journal-title":"Chem. Phys. Chem."},{"key":"175_CR14","doi-asserted-by":"crossref","unstructured":"Ballarin, C., Homann, K., Calmet, J.: Theorems and algorithms: an interface between Isabelle and Maple. In: Levelt, A.H.M. (ed.) Proceedings of the 1995 International Symposium on Symbolic and Algebraic Computation, ISSAC \u201995, pp. 150\u2013157. ACM, New York, USA (1995)","DOI":"10.1145\/220346.220366"},{"key":"175_CR15","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139644181","volume-title":"Principles of Optics Electromagnetic: Theory of Propagation, Interference and Diffraction of Light","author":"M. Born","year":"1999","unstructured":"Born M., Wolf E.: Principles of Optics Electromagnetic: Theory of Propagation, Interference and Diffraction of Light. Cambridge University Press, Cambridge, UK (1999)"},{"issue":"4","key":"175_CR16","doi-asserted-by":"crossref","first-page":"470","DOI":"10.1016\/j.jal.2005.10.006","volume":"4","author":"B. Buchberger","year":"2006","unstructured":"Buchberger B., Craciun A., Jebelean T., Kovacs L., Kutsia T., Nakagawa K., Piroi F., Popov N., Robu J., Rosenkranz M., Windsteiger W.: Theorema: towards computer-aided mathematical theory exploration. J. Appl. Logic 4(4), 470\u2013504 (2006)","journal-title":"J. Appl. Logic"},{"key":"175_CR17","doi-asserted-by":"crossref","unstructured":"Caprotti, O., Cohen, A.M.: Connecting proof checkers and computer algebra using OpenMath. In: Bertot, Y., Dowek, G., Thery, L., Hirschowitz, A., Paulin, C. (eds.) Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 1690, pp. 109\u2013112. Springer, Berlin, Heidelberg (1999)","DOI":"10.1007\/3-540-48256-3_8"},{"key":"175_CR18","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1145\/362001.362019","volume":"34","author":"O. Caprotti","year":"2000","unstructured":"Caprotti O., Cohen A.M., Riem M.: JAVA phrasebooks for computer algebra and automated deduction. SIGSAM Bull. 34, 33\u201337 (2000)","journal-title":"SIGSAM Bull."},{"issue":"24","key":"175_CR19","doi-asserted-by":"crossref","first-page":"5137","DOI":"10.1002\/adfm.201290146","volume":"22","author":"K.J. Chen","year":"2012","unstructured":"Chen K.J., Chen H.C., Tsai K.A., et. al.: Light-emitting devices: resonant-enhanced full-color emission of quantum-dot-based display technology using a pulsed spray method. Adv. Funct. Mater. 22(24), 5137\u20135137 (2012)","journal-title":"Adv. Funct. Mater."},{"key":"175_CR20","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1016\/j.optcom.2007.04.053","volume":"274","author":"Q. Cheng","year":"2007","unstructured":"Cheng Q., Cui T.J., Zhang C.: Waves in planar waveguide containing chiral nihility metamaterial. Opt. Commun. 274, 317\u2013321 (2007)","journal-title":"Opt. Commun."},{"issue":"752","key":"175_CR21","doi-asserted-by":"crossref","first-page":"642","DOI":"10.1098\/rspa.1925.0150","volume":"109","author":"P.A.M. Dirac","year":"1925","unstructured":"Dirac P.A.M.: The fundamental equations of quantum mechanics. Proc. R. Soc. A: Math. Phys. Eng. Sci. 109(752), 642\u2013653 (1925)","journal-title":"Proc. R. Soc. A: Math. Phys. Eng. Sci."},{"key":"175_CR22","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1007\/BF02650179","volume":"21","author":"R. Feynman","year":"1982","unstructured":"Feynman R.: Simulating physics with computers. Int. J. Theor. Phys. 21, 467\u2013488 (1982)","journal-title":"Int. J. Theor. Phys."},{"key":"175_CR23","volume-title":"Analytical and Computational Methods in Electromagnetics","author":"R. Garg","year":"2008","unstructured":"Garg R.: Analytical and Computational Methods in Electromagnetics. Artech House, Norwood, MA, USA (2008)"},{"key":"175_CR24","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon M.J.C., Melham T.F.: Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge Press, Cambridge (1993)"},{"key":"175_CR25","volume-title":"Introduction to Electrodynamics","author":"D.J. Griffiths","year":"1999","unstructured":"Griffiths D.J.: Introduction to Electrodynamics. Pearson Prentice Hall, Upper Saddle River, NJ, USA (1999)"},{"key":"175_CR26","volume-title":"Introduction to Quantum Mechanics","author":"D.J. Griffiths","year":"2005","unstructured":"Griffiths D.J.: Introduction to Quantum Mechanics. Pearson Prentice Hall, Upper Saddle River, NJ, USA (2005)"},{"key":"175_CR27","doi-asserted-by":"crossref","first-page":"696","DOI":"10.1038\/nphoton.2009.230","volume":"3","author":"R.H. Hadfield","year":"2009","unstructured":"Hadfield R.H.: Single-Photon Detectors for Optical Quantum Information Applications. Nat. Photonics 3, 696\u2013705 (2009)","journal-title":"Nat. Photonics"},{"key":"175_CR28","unstructured":"Hales, T.C.: Introduction to the flyspeck project. In: Mathematics, Algorithms, Proofs, volume 05021 of Dagstuhl Seminar Proceedings (2005)"},{"key":"175_CR29","doi-asserted-by":"crossref","unstructured":"Harrison J.: HOL light: a tutorial introduction. In: Formal Methods in Computer-Aided Design, volume 1166 of LNCS, pp. 265\u2013269. Springer (1996)","DOI":"10.1007\/BFb0031814"},{"key":"175_CR30","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Theorem Proving with the Real Numbers (Distinguished dissertations). Springer, Verlag (1998)","DOI":"10.1007\/978-1-4471-1591-5"},{"key":"175_CR31","doi-asserted-by":"crossref","unstructured":"Harrison, J.: A HOL theory of Euclidean space. In: Theorem Proving in Higher Order Logics, volume 3603 of LNCS, pp. 114\u2013129. Springer (2005)","DOI":"10.1007\/11541868_8"},{"key":"175_CR32","unstructured":"Harrison, J.: Formalizing basic complex analysis. In: From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, volume 10(23) of Studies in Logic, Grammar and Rhetoric, pp. 151\u2013165. University of Bia\u0142ystok (2007)"},{"key":"175_CR33","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511576430","volume-title":"Handbook of Practical Logic and Automated Reasoning","author":"J. Harrison","year":"2009","unstructured":"Harrison J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Cambridge, UK (2009)"},{"key":"175_CR34","doi-asserted-by":"crossref","unstructured":"Harrison, J.: HOL light: an overview. In: Theorem Proving in Higher Order Logics, volume 5674 of Lecture Notes in Computer Science, pp. 60\u201366. Springer (2009)","DOI":"10.1007\/978-3-642-03359-9_4"},{"key":"175_CR35","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1023\/A:1006023127567","volume":"21","author":"J. Harrison","year":"1998","unstructured":"Harrison J., Th\u00e9ry L.: A skeptic\u2019s approach to combining HOL and maple. J. Autom. Reason. 21, 279\u2013294 (1998)","journal-title":"J. Autom. Reason."},{"key":"175_CR36","doi-asserted-by":"crossref","unstructured":"Hasan, O., Afshar, S.KH., Tahar, S.: Formal analysis of optical waveguides in Hol. In: Theorem Proving in Higher Order Logics, volume 5674 of LNCS, pp. 228\u2013243. Springer (2009)","DOI":"10.1007\/978-3-642-03359-9_17"},{"issue":"9-10","key":"175_CR37","doi-asserted-by":"crossref","first-page":"813","DOI":"10.1023\/A:1006998830374","volume":"31","author":"P.R. Hayes","year":"1999","unstructured":"Hayes P.R., O\u2019Keefe M.T., Woodward P.R., Gopinath A.: Higher-order-compact time domain numerical simulation of optical waveguides. Opt. Quantum Electron. 31(9-10), 813\u2013826 (1999)","journal-title":"Opt. Quantum Electron."},{"key":"175_CR38","volume-title":"Numerical Methods For Scientific Computing","author":"J.H. Heinbockel","year":"2004","unstructured":"Heinbockel J.H.: Numerical Methods For Scientific Computing. Trafford, Victoria, BC, Canada (2004)"},{"key":"175_CR39","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, Ch., Pichardie, D. (eds.) Interactive theorem proving. Lecture Notes in Computer Science, vol. 7998, pp. 279\u2013294. Springer, Berlin, Heidelberg (2013)","DOI":"10.1007\/978-3-642-39634-2_21"},{"issue":"3","key":"175_CR40","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1364\/OE.8.000173","volume":"8","author":"S.G. Johnson","year":"2001","unstructured":"Johnson S.G., Joannopoulos J.D.: Block-iterative frequency domain methods for Maxwell\u2019s equations in a planewave basis. Opt. Expr. 8(3), 173\u2013190 (2001)","journal-title":"Opt. Expr."},{"key":"175_CR41","volume-title":"Model Checking","author":"E.M. Clarke Jr.","year":"1999","unstructured":"Clarke E.M. Jr., Grumberg O., Peled D.A.: Model Checking. The MIT Press, Cambridge, MA, USA (1999)"},{"key":"175_CR42","unstructured":"Afshar S.K., Aravantinos V.: A HOL-Light library for vectors of complex numbers. http:\/\/hvg.ece.concordia.ca\/code\/hol-light\/complex-vectors (2014). Accessed 20 Mar 2014"},{"key":"175_CR43","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Wiedijk, F.: Certified computer algebra on top of an interactive theorem prover. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Towards Mechanized Mathematical Assistants. Lecture Notes in Computer Science, vol. 4573, pp. 94\u2013105. Springer, Berlin, Heidelberg (2007)","DOI":"10.1007\/978-3-540-73086-6_8"},{"issue":"12","key":"175_CR44","doi-asserted-by":"crossref","first-page":"1249","DOI":"10.1007\/s11082-013-9745-6","volume":"45","author":"M. Karimi","year":"2013","unstructured":"Karimi M., Abedi K., Zavvari M.: Resonant cavity enhanced quantum ring photodetector at 20\u00a0\u03bcm wavelength. Opt. Quantum Electron. 45(12), 1249\u20131258 (2013)","journal-title":"Opt. Quantum Electron."},{"issue":"10","key":"175_CR45","doi-asserted-by":"crossref","first-page":"1550","DOI":"10.1364\/AO.5.001550","volume":"5","author":"H. Kogelnik","year":"1966","unstructured":"Kogelnik H., Li T.: Laser beams and resonators. Appl. Opt. 5(10), 1550\u20131567 (1966)","journal-title":"Appl. Opt."},{"key":"175_CR46","doi-asserted-by":"crossref","unstructured":"LASCAD. http:\/\/www.las-cad.com\/ (2014). Accessed 20 Mar 2014","DOI":"10.18356\/06a3c3bd-es"},{"issue":"7","key":"175_CR47","doi-asserted-by":"crossref","first-page":"1207","DOI":"10.1088\/0034-4885\/66\/7\/203","volume":"66","author":"U. Leonhardt","year":"2003","unstructured":"Leonhardt U.: Quantum physics of simple optical instruments. Rep. Progr. Phys. 66(7), 1207 (2003)","journal-title":"Rep. Progr. Phys."},{"issue":"8","key":"175_CR48","doi-asserted-by":"crossref","first-page":"3235","DOI":"10.1109\/JLT.2006.876899","volume":"24","author":"Y. Liu","year":"2006","unstructured":"Liu Y., Sarris C.D.: Fast time-domain simulation of optical waveguide structures with a multilevel dynamically adaptive mesh refinement FDTD approach. J. Lightwave Technol. 24(8), 3235\u20133247 (2006)","journal-title":"J. Lightwave Technol."},{"issue":"5","key":"175_CR49","doi-asserted-by":"crossref","first-page":"1129","DOI":"10.1088\/0034-4885\/68\/5\/R04","volume":"68","author":"B. Lounis","year":"2005","unstructured":"Lounis B., Orrit M.: Single-photon sources. Rep. Progr. Phys. 68(5), 1129\u20131179 (2005)","journal-title":"Rep. Progr. Phys."},{"key":"175_CR50","doi-asserted-by":"crossref","unstructured":"Mahmoud, M.Y., Aravantinos, V., Tahar, S.: Formalization of infinite dimension linear spaces with application to quantum theory. In: NASA Formal Methods, volume 7871 of LNCS, pp. 413\u2013427. Springer (2013)","DOI":"10.1007\/978-3-642-38088-4_28"},{"key":"175_CR51","doi-asserted-by":"crossref","unstructured":"Malak, M., Pavy, N., Marty, F., Peter, Y., Liu, A.Q., Bourouina, T.: Stable, high-Q Fabry\u2013Perot resonators with long cavity based on curved, all-silicon, high reflectance mirrors. In: IEEE International Conference on Micro Electro Mechanical Systems, pp. 720\u2013723 (2011)","DOI":"10.1109\/MEMSYS.2011.5734526"},{"key":"175_CR52","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139644105","volume-title":"Optical Coherence and Quantum Optics","author":"L. Mandel","year":"1995","unstructured":"Mandel L., Wolf E.: Optical Coherence and Quantum Optics. Cambridge University Press, Cambridge, UK (1995)"},{"key":"175_CR53","unstructured":"Mathscheme. http:\/\/www.cas.mcmaster.ca\/research\/mathscheme\/ (2014). Accessed 20 Mar 2014"},{"key":"175_CR54","unstructured":"MATLAB. http:\/\/www.mathworks.com\/products\/matlab\/ (2014). Accessed 20 Mar 2014"},{"issue":"016611","key":"175_CR55","first-page":"1","volume":"64","author":"S. Mookherjea","year":"2001","unstructured":"Mookherjea S.: Analysis of optical pulse propagation with two-by-two (ABCD) matrices. Phys. Rev. E 64(016611), 1\u201310 (2001)","journal-title":"Phys. Rev. E"},{"key":"175_CR56","unstructured":"MuPAD. http:\/\/www.mathworks.com\/discovery\/mupad.html (2014). Accessed 20 Mar 2014"},{"issue":"7","key":"175_CR57","doi-asserted-by":"crossref","first-page":"1075","DOI":"10.1109\/3.687847","volume":"34","author":"M. Nakazawa","year":"1998","unstructured":"Nakazawa M., Kubota H., Sahara A., Tamura K.: Time-domain ABCD matrix formalism for laser mode-locking and optical pulse transmission. IEEE J. Quantum Electron. 34(7), 1075\u20131081 (1998)","journal-title":"IEEE J. Quantum Electron."},{"key":"175_CR58","doi-asserted-by":"crossref","unstructured":"Naqvi, A.: Comments on waves in planar waveguide containing chiral nihility metamaterial. Opt. Commun. 284:215\u2013216, Elsevier (2011)","DOI":"10.1016\/j.optcom.2010.08.017"},{"key":"175_CR59","unstructured":"Institute of Quantum Optics at Leibniz University of Hannover. General directives for safety in the institute of quantum optics. http:\/\/www.iqo.uni-hannover.de\/fileadmin\/institut\/pdf\/job%20security\/3._Sicherheitmerkblatt06012014_engl.pdf (2014). Accessed 20 Mar 2014"},{"issue":"3","key":"175_CR60","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1088\/0031-9120\/44\/3\/008","volume":"44","author":"A. Pereira","year":"2009","unstructured":"Pereira A., Ostermann F., Cavalcanti C.: On the use of a virtual Mach\u2013Zehnder interferometer in the teaching of quantum mechanics. Phys. Educ. 44(3), 281 (2009)","journal-title":"Phys. Educ."},{"key":"175_CR61","volume-title":"Fundamentals of Optoelectronics","author":"C.R. Pollock","year":"1995","unstructured":"Pollock C.R.: Fundamentals of Optoelectronics. Tom Casson, Chicago, USA (1995)"},{"key":"175_CR62","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1145\/362001.362016","volume":"34","author":"H. Prieto","year":"2000","unstructured":"Prieto H., Dalmas S., Papegay Y.: Mathematica as an OpenMath application. SIGSAM Bull. 34, 22\u201326 (2000)","journal-title":"SIGSAM Bull."},{"key":"175_CR63","doi-asserted-by":"crossref","first-page":"042319","DOI":"10.1103\/PhysRevA.68.042319","volume":"68","author":"T.C. Ralph","year":"2003","unstructured":"Ralph T.C., Gilchrist A., Milburn G.J., Munro W.J., Glancy S.: Quantum computation with optical coherent states. Phys. Rev. 68, 042319 (2003)","journal-title":"Phys. Rev."},{"issue":"6","key":"175_CR64","doi-asserted-by":"crossref","first-page":"1480","DOI":"10.1109\/JSTQE.2006.884082","volume":"12","author":"B. Saadany","year":"2006","unstructured":"Saadany B., Malak M., Kubota M., Marty F.M., Mita Y., Khalil D., Bourouina T.: Free-space tunable and drop optical filters using vertical Bragg mirrors on silicon. IEEE J. Sel. Topics Quantum Electron. 12(6), 1480\u20131488 (2006)","journal-title":"IEEE J. Sel. Topics Quantum Electron."},{"key":"175_CR65","doi-asserted-by":"crossref","DOI":"10.1002\/0471213748","volume-title":"Fundamentals of Photonics","author":"B.E.A. Saleh","year":"1991","unstructured":"Saleh B.E.A., Teich M.C.: Fundamentals of Photonics. John Wiley & Sons, Inc., New York, USA (1991)"},{"key":"175_CR66","doi-asserted-by":"crossref","unstructured":"Siddique, U., Aravantinos, V., Tahar, S.: A new approach for the verification of optical systems. In: Optical System Alignment, Tolerancing, and Verification VII, volume 8844 of SPIE, pp. 88440G\u201388440G\u201314 (2013)","DOI":"10.1117\/12.2024860"},{"key":"175_CR67","doi-asserted-by":"crossref","unstructured":"Siddique, U., Aravantinos, V., Tahar, S.: Formal stability analysis of optical resonators. In: NASA Formal Methods, volume 7871 of LNCS, pp. 368\u2013382 (2013)","DOI":"10.1007\/978-3-642-38088-4_25"},{"key":"175_CR68","doi-asserted-by":"crossref","unstructured":"Siddique, U., Aravantinos, V., Tahar, S.: On the formal analysis of geometrical optics in HOL. In: Automated Deduction in Geometry, volume 7993 of LNCS, pp. 161\u2013180 (2013)","DOI":"10.1007\/978-3-642-40672-0_11"},{"key":"175_CR69","volume-title":"Lasers","author":"A.E. Siegman","year":"1986","unstructured":"Siegman A.E.: Lasers. University Science Books, Sausalito, CA, USA (1986)"},{"key":"175_CR70","unstructured":"Optica Software. http:\/\/www.opticasoftware.com\/ (2014). Accessed 20 Mar 2014"},{"issue":"20","key":"175_CR71","doi-asserted-by":"crossref","first-page":"203901","DOI":"10.1063\/1.2387965","volume":"89","author":"W.Z. Song","year":"2006","unstructured":"Song W.Z., Zhang X.M., Liu A.Q., Lim C.S., Yap P.H., Hosseini Habib M.M.: Refractive index measurement of single living cells using on-chip Fabry\u2013Perot cavity. Appl. Phys. Lett. 89(20), 203901 (2006)","journal-title":"Appl. Phys. Lett."},{"issue":"7","key":"175_CR72","doi-asserted-by":"crossref","first-page":"1318","DOI":"10.1016\/j.optlastec.2011.03.031","volume":"43","author":"B. Su","year":"2011","unstructured":"Su B., Xue J., Sun L., Zhao H., Pei X.: Generalised ABCD matrix treatment for laser resonators and beam propagation. Opt. Laser Technol. 43(7), 1318\u20131320 (2011)","journal-title":"Opt. Laser Technol."},{"key":"175_CR73","volume-title":"The Collected Mathematical Papers of James Joseph Sylvester. vol. 4","author":"J.J. Sylvester","year":"1912","unstructured":"Sylvester J.J.: The Collected Mathematical Papers of James Joseph Sylvester. vol. 4. Cambridge University Press, Cambridge, UK (1912)"},{"key":"175_CR74","unstructured":"Synopsys-CODE-V. http:\/\/optics.synopsys.com\/codev\/index.html (2014). Accessed 20 Mar 2014"},{"key":"175_CR75","doi-asserted-by":"crossref","first-page":"276","DOI":"10.1080\/09500340.2010.546894","volume":"58","author":"A.G. White","year":"2011","unstructured":"White A.G., Jennewein T., Barbieri M.: Single-photon device requirements for operating linear optics quantum computing outside the post-selection basis. J. Modern Opt. 58, 276\u2013287 (2011)","journal-title":"J. Modern Opt."},{"issue":"4","key":"175_CR76","doi-asserted-by":"crossref","first-page":"4900107","DOI":"10.1109\/JSTQE.2013.2241398","volume":"19","author":"M.P. Tan","year":"2013","unstructured":"Tan M.P., Kasten A.M., Sulkin J.D., Choquette K.D.: Planar photonic crystal vertical-cavity surface-emitting lasers. IEEE J. Sel. Topics Quantum Electron. 19(4), 4900107\u20134900107 (2013)","journal-title":"IEEE J. Sel. Topics Quantum Electron."},{"key":"175_CR77","doi-asserted-by":"crossref","first-page":"424","DOI":"10.1088\/1464-4266\/1\/4\/312","volume":"1","author":"S.M. Tan","year":"1999","unstructured":"Tan S.M.: A computational toolbox for quantum and atomic optics. J. Opt. B: Quantum Semiclass. Opt. 1, 424\u2013432 (1999)","journal-title":"J. Opt. B: Quantum Semiclass. Opt."},{"key":"175_CR78","unstructured":"\u00dcnl\u00fc, M.S., Strite, S.: Resonant cavity enhanced photonic devices. J. Appl. Phys. 78(2), 607\u2013639 (1995)"},{"issue":"1","key":"175_CR79","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-8(1:30)2012","volume":"8","author":"F. Wiedijk","year":"2012","unstructured":"Wiedijk F.: A synthesis of the procedural and declarative styles of interactive theorem proving. Log. Methods Comput. Sci. 8(1), 1\u201326 (2012)","journal-title":"Log. Methods Comput. Sci."},{"key":"175_CR80","unstructured":"Wilson, W.C., Atkinson, G.M.: MOEMS modeling using the geometrical matrix toolbox. Technical report, NASA, Langley Research Center (2005)"},{"key":"175_CR81","doi-asserted-by":"crossref","unstructured":"Yin, L., Hong, W.: Domain decomposition method: a direct solution of Maxwell equations. In: Antennas and Propagation Society International Symposium, IEEE, vol.2, pp. 1290\u20131293 (1999)","DOI":"10.1109\/APS.1999.789550"}],"container-title":["Mathematics in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-014-0175-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11786-014-0175-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11786-014-0175-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T16:26:48Z","timestamp":1746203208000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11786-014-0175-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,3]]},"references-count":81,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,3]]}},"alternative-id":["175"],"URL":"https:\/\/doi.org\/10.1007\/s11786-014-0175-z","relation":{},"ISSN":["1661-8270","1661-8289"],"issn-type":[{"type":"print","value":"1661-8270"},{"type":"electronic","value":"1661-8289"}],"subject":[],"published":{"date-parts":[[2014,3]]}}}