Muñoz, Cesar A.; Ayala-Rincón, Mauricio; Moscato, Mariano M.; Dutle, Aaron M.; Narkawicz, Anthony J.; Almeida, Ariane Alves; da Silva, Andréia B. Avelar; Ramos, Thiago M. Ferreira Formal verification of termination criteria for first-order recursive functions. (English) Zbl 07800193 J. Autom. Reasoning 67, No. 4, Paper No. 40, 30 p. (2023). MSC: 68V15 PDFBibTeX XMLCite \textit{C. A. Muñoz} et al., J. Autom. Reasoning 67, No. 4, Paper No. 40, 30 p. (2023; Zbl 07800193) Full Text: DOI
Bauer-Marquart, Fabian; Leue, Stefan; Schilling, Christian symQV: automated symbolic verification of quantum programs. (English) Zbl 07728843 Chechik, Marsha (ed.) et al., Formal methods. 25th international symposium, FM 2023, Lübeck, Germany, March 6–10, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14000, 181-198 (2023). MSC: 68Q60 68N30 68V15 81P68 PDFBibTeX XMLCite \textit{F. Bauer-Marquart} et al., Lect. Notes Comput. Sci. 14000, 181--198 (2023; Zbl 07728843) Full Text: DOI arXiv
Castañeda, Armando; Hurault, Aurélie; Quéinnec, Philippe; Roy, Matthieu Tasks in modular proofs of concurrent algorithms. (English) Zbl 07687226 Inf. Comput. 292, Article ID 105040, 21 p. (2023). MSC: 68Qxx PDFBibTeX XMLCite \textit{A. Castañeda} et al., Inf. Comput. 292, Article ID 105040, 21 p. (2023; Zbl 07687226) Full Text: DOI arXiv
Martin-Martin, Enrique; Montenegro, Manuel; Riesco, Adrián; Rodríguez-Hortalá, Juan; Rubio, Rubén Verification of the ROS NavFn planner using executable specification languages. (English) Zbl 07665444 J. Log. Algebr. Methods Program. 132, Article ID 100860, 23 p. (2023). MSC: 68-XX PDFBibTeX XMLCite \textit{E. Martin-Martin} et al., J. Log. Algebr. Methods Program. 132, Article ID 100860, 23 p. (2023; Zbl 07665444) Full Text: DOI
Miranda-Perea, Favio Ezequiel; del Carmen González Huesca, Lourdes; Linares Arévalo, Pilar Selene A dual-context sequent calculus for the constructive modal logic S4. (English) Zbl 07676413 Math. Struct. Comput. Sci. 32, No. 9, 1205-1233 (2022). MSC: 03-XX PDFBibTeX XMLCite \textit{F. E. Miranda-Perea} et al., Math. Struct. Comput. Sci. 32, No. 9, 1205--1233 (2022; Zbl 07676413) Full Text: DOI
Hirata, Michikazu; Minamide, Yasuhiko; Sato, Tetsuya Program logic for higher-order probabilistic programs in Isabelle/HOL. (English) Zbl 07570114 Hanus, Michael (ed.) et al., Functional and logic programming. 16th international symposium, FLOPS 2022, Kyoto, Japan, May 10–12, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13215, 57-74 (2022). MSC: 68N17 68N18 PDFBibTeX XMLCite \textit{M. Hirata} et al., Lect. Notes Comput. Sci. 13215, 57--74 (2022; Zbl 07570114) Full Text: DOI
Zhang, Hengchu; Honoré, Wolf; Koh, Nicolas; Li, Yao; Li, Yishuai; Xia, Li-Yao; Beringer, Lennart; Mansky, William; Pierce, Benjamin; Zdancewic, Steve Verifying an HTTP key-value server with interaction trees and VST. (English) Zbl 07699449 Cohen, Liron (ed.) et al., 12th international conference on interactive theorem proving, ITP 2021, Rome, Italy, virtual conference, June 29 – July 1, 2021. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 193, Article 32, 19 p. (2021). MSC: 68V15 PDFBibTeX XMLCite \textit{H. Zhang} et al., LIPIcs -- Leibniz Int. Proc. Inform. 193, Article 32, 19 p. (2021; Zbl 07699449) Full Text: DOI
Liu, Yezhou; Nicolescu, Radu; Sun, Jing Formal verification of cP systems using Coq. (English) Zbl 1490.68100 J. Membr. Comput. 3, No. 3, 205-220 (2021). MSC: 68Q07 68V20 PDFBibTeX XMLCite \textit{Y. Liu} et al., J. Membr. Comput. 3, No. 3, 205--220 (2021; Zbl 1490.68100) Full Text: DOI
Safari, Mohsen; Oortwijn, Wytse; Huisman, Marieke Automated verification of the parallel Bellman-Ford algorithm. (English) Zbl 1497.68396 Drăgoi, Cezara (ed.) et al., Static analysis. 28th international symposium, SAS 2021, Chicago, IL, USA, October 17–19, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12913, 346-358 (2021). MSC: 68R10 68Q60 68W10 PDFBibTeX XMLCite \textit{M. Safari} et al., Lect. Notes Comput. Sci. 12913, 346--358 (2021; Zbl 1497.68396) Full Text: DOI
Popescu, Andrei; Traytel, Dmitriy Distilling the requirements of Gödel’s incompleteness theorems with a proof assistant. (English) Zbl 07433027 J. Autom. Reasoning 65, No. 7, 1027-1070 (2021). MSC: 68V15 PDFBibTeX XMLCite \textit{A. Popescu} and \textit{D. Traytel}, J. Autom. Reasoning 65, No. 7, 1027--1070 (2021; Zbl 07433027) Full Text: DOI
Letan, Thomas; Régis-Gianas, Yann; Chifflier, Pierre; Hiet, Guillaume Modular verification of programs with effects and effects handlers. (English) Zbl 1458.68119 Formal Asp. Comput. 33, No. 1, 127-150 (2021). MSC: 68Q60 68V15 PDFBibTeX XMLCite \textit{T. Letan} et al., Formal Asp. Comput. 33, No. 1, 127--150 (2021; Zbl 1458.68119) Full Text: DOI
Christensen, Michael; McMahan, Joseph; Nichols, Lawton; Roesch, Jared; Sherwood, Timothy; Hardekopf, Ben Safe functional systems through integrity types and verified assembly. (English) Zbl 1477.68030 Theor. Comput. Sci. 851, 39-61 (2021). MSC: 68M07 68N18 68Q60 PDFBibTeX XMLCite \textit{M. Christensen} et al., Theor. Comput. Sci. 851, 39--61 (2021; Zbl 1477.68030) Full Text: DOI
Wimmer, Simon; von Mutius, Joshua Verified certification of reachability checking for timed automata. (English) Zbl 1507.68200 Biere, Armin (ed.) et al., Tools and algorithms for the construction and analysis of systems. 26th international conference, TACAS 2020, held as part of the European joint conferences on theory and practice of software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12078, 425-443 (2020). MSC: 68Q60 68Q45 68V15 PDFBibTeX XMLCite \textit{S. Wimmer} and \textit{J. von Mutius}, Lect. Notes Comput. Sci. 12078, 425--443 (2020; Zbl 1507.68200) Full Text: DOI
Oortwijn, Wytse; Huisman, Marieke; Joosten, Sebastiaan J. C.; van de Pol, Jaco Automated verification of parallel nested DFS. (English) Zbl 1517.68248 Biere, Armin (ed.) et al., Tools and algorithms for the construction and analysis of systems. 26th international conference, TACAS 2020, held as part of the European joint conferences on theory and practice of software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12078, 247-265 (2020). MSC: 68Q60 68Q85 68V15 PDFBibTeX XMLCite \textit{W. Oortwijn} et al., Lect. Notes Comput. Sci. 12078, 247--265 (2020; Zbl 1517.68248) Full Text: DOI
Carneiro, Mario Metamath Zero: designing a theorem prover prover. (English) Zbl 1455.68243 Benzmüller, Christoph (ed.) et al., Intelligent computer mathematics. 13th international conference, CICM 2020, Bertinoro, Italy, July 26–31, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12236, 71-88 (2020). MSC: 68V15 68Q60 PDFBibTeX XMLCite \textit{M. Carneiro}, Lect. Notes Comput. Sci. 12236, 71--88 (2020; Zbl 1455.68243) Full Text: DOI arXiv
del Carmen González Huesca, Lourdes; Miranda Perea, Favio Ezequiel; Linares-Arévalo, P. Selene Dual and axiomatic systems for constructive S4, a formally verified equivalence. (English) Zbl 1495.03032 Felty, Amy (ed.) et al., 14th international workshop on logical and semantic frameworks, with applications, LSFA 2019, Natal, Brazil, in August 2019. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 348, 61-83 (2020). MSC: 03B45 68V15 03B35 PDFBibTeX XMLCite \textit{L. del Carmen González Huesca} et al., Electron. Notes Theor. Comput. Sci. 348, 61--83 (2020; Zbl 1495.03032) Full Text: DOI
Jiang, Jingjing; Qiao, Lei; Yang, Mengfei; Yang, Hua; Liu, Bo Operating system task management requirements layer modeling and verification based on Coq. (Chinese. English summary) Zbl 1463.68015 J. Softw. 31, No. 8, 2375-2387 (2020). MSC: 68N25 68Q60 68V15 PDFBibTeX XMLCite \textit{J. Jiang} et al., J. Softw. 31, No. 8, 2375--2387 (2020; Zbl 1463.68015) Full Text: DOI
Thiemann, René; Bottesch, Ralph; Divasón, Jose; Haslbeck, Max W.; Joosten, Sebastiaan J. C.; Yamada, Akihisa Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL. (English) Zbl 1468.68309 J. Autom. Reasoning 64, No. 5, 827-856 (2020). MSC: 68V15 11H06 11Y16 68V20 PDFBibTeX XMLCite \textit{R. Thiemann} et al., J. Autom. Reasoning 64, No. 5, 827--856 (2020; Zbl 1468.68309) Full Text: DOI
Sheng, Feng; Zhu, Huibiao; He, Jifeng; Yang, Zongyuan; Bowen, Jonathan P. Theoretical and practical approaches to the denotational semantics for MDESL based on UTP. (English) Zbl 1458.68041 Formal Asp. Comput. 32, No. 2-3, 275-314 (2020). MSC: 68N30 68Q55 PDFBibTeX XMLCite \textit{F. Sheng} et al., Formal Asp. Comput. 32, No. 2--3, 275--314 (2020; Zbl 1458.68041) Full Text: DOI
Lammich, Peter Efficient verified (UN)SAT certificate checking. (English) Zbl 1468.68134 J. Autom. Reasoning 64, No. 3, 513-532 (2020). MSC: 68Q60 68V15 PDFBibTeX XMLCite \textit{P. Lammich}, J. Autom. Reasoning 64, No. 3, 513--532 (2020; Zbl 1468.68134) Full Text: DOI
Chen, Ran; Cohen, Cyril; Lévy, Jean-Jacques; Merz, Stephan; Théry, Laurent Formal proofs of Tarjan’s strongly connected components algorithm in Why3, Coq and Isabelle. (English) Zbl 07649962 Harrison, John (ed.) et al., 10th international conference on interactive theorem proving, ITP 2019, September 9–12, 2019, Portland, OR, USA. Proceedings. Wadern: Schloss Dagstuhl – Leibniz-Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 141, Article 13, 19 p. (2019). MSC: 68V15 PDFBibTeX XMLCite \textit{R. Chen} et al., LIPIcs -- Leibniz Int. Proc. Inform. 141, Article 13, 19 p. (2019; Zbl 07649962) Full Text: DOI arXiv
Marmsoler, Diego; Gidey, Habtom Kashay Interactive verification of architectural design patterns in FACTum. (English) Zbl 1425.68273 Formal Asp. Comput. 31, No. 5, 541-610 (2019). MSC: 68Q65 68T15 PDFBibTeX XMLCite \textit{D. Marmsoler} and \textit{H. K. Gidey}, Formal Asp. Comput. 31, No. 5, 541--610 (2019; Zbl 1425.68273) Full Text: DOI
González Huesca, Lourdes del Carmen; Miranda-Perea, Favio E.; Linares-Arévalo, P. Selene Axiomatic and dual systems for constructive necessity, a formally verified equivalence. (English) Zbl 1444.03054 J. Appl. Non-Class. Log. 29, No. 3, 255-287 (2019). MSC: 03B45 03B35 PDFBibTeX XMLCite \textit{L. d. C. González Huesca} et al., J. Appl. Non-Class. Log. 29, No. 3, 255--287 (2019; Zbl 1444.03054) Full Text: DOI
Sandberg Ericsson, Adam; Myreen, Magnus O.; Åman Pohjola, Johannes A verified generational garbage collector for CakeML. (English) Zbl 1468.68066 J. Autom. Reasoning 63, No. 2, 463-488 (2019). MSC: 68N20 68V15 PDFBibTeX XMLCite \textit{A. Sandberg Ericsson} et al., J. Autom. Reasoning 63, No. 2, 463--488 (2019; Zbl 1468.68066) Full Text: DOI
Nipkow, Tobias; Brinkop, Hauke Amortized complexity verified. (English) Zbl 1465.68060 J. Autom. Reasoning 62, No. 3, 367-391 (2019). MSC: 68P05 68N18 68V20 PDFBibTeX XMLCite \textit{T. Nipkow} and \textit{H. Brinkop}, J. Autom. Reasoning 62, No. 3, 367--391 (2019; Zbl 1465.68060) Full Text: DOI
Charguéraud, Arthur; Pottier, François Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. (English) Zbl 1468.68120 J. Autom. Reasoning 62, No. 3, 331-365 (2019). MSC: 68Q60 03B70 68N18 68P05 68V20 PDFBibTeX XMLCite \textit{A. Charguéraud} and \textit{F. Pottier}, J. Autom. Reasoning 62, No. 3, 331--365 (2019; Zbl 1468.68120) Full Text: DOI HAL
Lammich, Peter; Sefidgar, S. Reza Formalizing network flow algorithms: a refinement approach in Isabelle/HOL. (English) Zbl 1468.68328 J. Autom. Reasoning 62, No. 2, 261-280 (2019). MSC: 68V20 05C21 68W40 90C35 PDFBibTeX XMLCite \textit{P. Lammich} and \textit{S. R. Sefidgar}, J. Autom. Reasoning 62, No. 2, 261--280 (2019; Zbl 1468.68328) Full Text: DOI Link
Grégoire, Thomas; Chlipala, Adam Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms. (English) Zbl 1468.68130 J. Autom. Reasoning 62, No. 2, 193-213 (2019). MSC: 68Q60 68V15 PDFBibTeX XMLCite \textit{T. Grégoire} and \textit{A. Chlipala}, J. Autom. Reasoning 62, No. 2, 193--213 (2019; Zbl 1468.68130) Full Text: DOI Link
Völlinger, Kim; Akili, Samira On a verification framework for certifying distributed algorithms: distributed checking and consistency. (English) Zbl 1508.68080 Baier, Christel (ed.) et al., Formal techniques for distributed objects, components, and systems. 38th IFIP WG 6.1 international conference, FORTE 2018, held as part of the 13th international federated conference on distributed computing techniques, DisCoTec 2018, Madrid, Spain, June 18–21, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10854, 161-180 (2018). MSC: 68N30 68W15 PDFBibTeX XMLCite \textit{K. Völlinger} and \textit{S. Akili}, Lect. Notes Comput. Sci. 10854, 161--180 (2018; Zbl 1508.68080) Full Text: DOI
Paulson, Lawrence C. Computational logic: its origins and applications. (English) Zbl 1402.68160 Proc. R. Soc. Lond., A, Math. Phys. Eng. Sci. 474, No. 2210, Article ID 20170872, 14 p. (2018). MSC: 68T15 68-03 01A60 01A61 03B35 03B70 68Q60 PDFBibTeX XMLCite \textit{L. C. Paulson}, Proc. R. Soc. Lond., A, Math. Phys. Eng. Sci. 474, No. 2210, Article ID 20170872, 14 p. (2018; Zbl 1402.68160) Full Text: DOI arXiv
Abdulaziz, Mohammad; Norrish, Michael; Gretton, Charles Formally verified algorithms for upper-bounding state space diameters. (English) Zbl 1451.68164 J. Autom. Reasoning 61, No. 1-4, 485-520 (2018). MSC: 68Q60 68T20 68V15 PDFBibTeX XMLCite \textit{M. Abdulaziz} et al., J. Autom. Reasoning 61, No. 1--4, 485--520 (2018; Zbl 1451.68164) Full Text: DOI
Fares, Elie; Bodeveix, Jean-Paul; Filali, Mamoun Event algebra for transition systems composition application to timed automata. (English) Zbl 1398.68340 Acta Inf. 55, No. 5, 363-400 (2018). MSC: 68Q60 68Q45 68Q85 PDFBibTeX XMLCite \textit{E. Fares} et al., Acta Inf. 55, No. 5, 363--400 (2018; Zbl 1398.68340) Full Text: DOI Link
Genet, Thomas; Haudebourg, Timothée; Jensen, Thomas Verifying higher-order functions with tree automata. (English) Zbl 1504.68129 Baier, Christel (ed.) et al., Foundations of software science and computation structures. 21st international conference, FOSSACS 2018, held as part of the European joint conferences on theory and practice of software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10803, 565-582 (2018). MSC: 68Q60 68N18 68Q42 68Q45 PDFBibTeX XMLCite \textit{T. Genet} et al., Lect. Notes Comput. Sci. 10803, 565--582 (2018; Zbl 1504.68129) Full Text: DOI
Struth, Georg Hoare semigroups. (English) Zbl 1390.68440 Math. Struct. Comput. Sci. 28, No. 6, 775-799 (2018). MSC: 68Q60 03B70 20M10 PDFBibTeX XMLCite \textit{G. Struth}, Math. Struct. Comput. Sci. 28, No. 6, 775--799 (2018; Zbl 1390.68440) Full Text: DOI
Clochard, Martin; Gondelman, Léon; Pereira, Mário The matrix reproved (verification pearl). (English) Zbl 1426.68164 J. Autom. Reasoning 60, No. 3, 365-383 (2018). MSC: 68Q60 65F30 68V15 68W30 PDFBibTeX XMLCite \textit{M. Clochard} et al., J. Autom. Reasoning 60, No. 3, 365--383 (2018; Zbl 1426.68164) Full Text: DOI HAL
Blazy, Sandrine (ed.); Chechik, Marsha (ed.) Selected extended papers of VSTTE 2016. (English) Zbl 1426.68006 J. Autom. Reasoning 60, No. 3, 255-256 (2018). MSC: 68-06 68N30 68Q60 68V15 PDFBibTeX XMLCite \textit{S. Blazy} (ed.) and \textit{M. Chechik} (ed.), J. Autom. Reasoning 60, No. 3, 255--256 (2018; Zbl 1426.68006) Full Text: DOI
Paviotti, Marco; Bengtson, Jesper Formally verifying exceptions for low-level code with separation logic. (English) Zbl 1382.68053 J. Log. Algebr. Methods Program. 94, 1-14 (2018). MSC: 68N30 03B70 68Q60 68T15 PDFBibTeX XMLCite \textit{M. Paviotti} and \textit{J. Bengtson}, J. Log. Algebr. Methods Program. 94, 1--14 (2018; Zbl 1382.68053) Full Text: DOI Link
Biernacka, Małgorzata; Charatonik, Witold; Zielińska, Klara Generalized refocusing: from hybrid strategies to abstract machines. (English) Zbl 1441.68131 Miller, Dale (ed.), 2nd international conference on formal structures for computation and deduction. FSCD 2017, Oxford, UK, September 3–9, 2017. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 84, Article 10, 17 p. (2017). MSC: 68Q60 68Q55 68V15 PDFBibTeX XMLCite \textit{M. Biernacka} et al., LIPIcs -- Leibniz Int. Proc. Inform. 84, Article 10, 17 p. (2017; Zbl 1441.68131) Full Text: DOI
Magron, Victor; Constantinides, George; Donaldson, Alastair Certified roundoff error bounds using semidefinite programming. (English) Zbl 1380.65084 ACM Trans. Math. Softw. 43, No. 4, Article No. 34, 31 p. (2017). MSC: 65G50 90C22 PDFBibTeX XMLCite \textit{V. Magron} et al., ACM Trans. Math. Softw. 43, No. 4, Article No. 34, 31 p. (2017; Zbl 1380.65084) Full Text: DOI arXiv
Stucke, Insa Reasoning about cardinalities of relations with applications supported by proof assistants. (English) Zbl 1486.68105 Höfner, Peter (ed.) et al., Relational and algebraic methods in computer science. 16th international conference, RAMiCS 2017, Lyon, France, May 15–18, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10226, 290-306 (2017). MSC: 68Q60 03G15 05C15 68V15 68V20 PDFBibTeX XMLCite \textit{I. Stucke}, Lect. Notes Comput. Sci. 10226, 290--306 (2017; Zbl 1486.68105) Full Text: DOI
Boldo, Sylvie; Melquiond, Guillaume Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system. (English) Zbl 1385.68001 Amsterdam: Elsevier/ISTE Press (ISBN 978-1-78548-112-3/hbk; 978-0-08-101170-6/ebook). xx, 306 p. (2017). Reviewer: Manfred Kerber (Birmingham) MSC: 68-02 65G50 65Y04 68Q60 68T15 PDFBibTeX XMLCite \textit{S. Boldo} and \textit{G. Melquiond}, Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system. Amsterdam: Elsevier/ISTE Press (2017; Zbl 1385.68001) Full Text: Link
Lucanu, Dorel; Rusu, Vlad; Arusoaie, Andrei A generic framework for symbolic execution: a coinductive approach. (English) Zbl 1356.68044 J. Symb. Comput. 80, Part 1, 125-163 (2017). MSC: 68N30 68Q55 68W30 PDFBibTeX XMLCite \textit{D. Lucanu} et al., J. Symb. Comput. 80, Part 1, 125--163 (2017; Zbl 1356.68044) Full Text: DOI HAL
Betarte, Gustavo; Campo, Juan; Luna, Carlos; Romano, Agustín Formal analysis of Android’s permission-based security model. (English) Zbl 1424.68029 Sci. Ann. Comput. Sci. 26, No. 1, 27-68 (2016). MSC: 68N25 68Q60 68T15 94A62 PDFBibTeX XMLCite \textit{G. Betarte} et al., Sci. Ann. Comput. Sci. 26, No. 1, 27--68 (2016; Zbl 1424.68029) Full Text: DOI
Mahboubi, Assia Machine-checked mathematics. (English) Zbl 1375.68101 Nieuw Arch. Wiskd. (5) 17, No. 3, 172-176 (2016). Reviewer: Nail Zamov (Kazan) MSC: 68T15 01A60 03B35 68-03 PDFBibTeX XMLCite \textit{A. Mahboubi}, Nieuw Arch. Wiskd. (5) 17, No. 3, 172--176 (2016; Zbl 1375.68101)
Bisping, Benjamin; Brodmann, Paul-David; Jungnickel, Tim; Rickmann, Christina; Seidler, Henning; Stüber, Anke; Wilhelm-Weidner, Arno; Peters, Kirstin; Nestmann, Uwe Mechanical verification of a constructive proof for FLP. (English) Zbl 1478.68146 Blanchette, Jasmin Christian (ed.) et al., Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22–25, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9807, 107-122 (2016). MSC: 68Q60 68M14 68M15 68V15 68V20 PDFBibTeX XMLCite \textit{B. Bisping} et al., Lect. Notes Comput. Sci. 9807, 107--122 (2016; Zbl 1478.68146) Full Text: DOI
Armstrong, Alasdair; Gomes, Victor B. F.; Struth, Georg Building program construction and verification tools from algebraic principles. (English) Zbl 1342.68066 Formal Asp. Comput. 28, No. 2, 265-293 (2016). MSC: 68N30 68Q60 68T15 PDFBibTeX XMLCite \textit{A. Armstrong} et al., Formal Asp. Comput. 28, No. 2, 265--293 (2016; Zbl 1342.68066) Full Text: DOI
Klein, Gerwin (ed.); Gamboa, Ruben (ed.) Interactive theorem proving. Preface of the special issue. (English) Zbl 1336.00112 J. Autom. Reasoning 56, No. 3, 201-203 (2016). MSC: 00B15 68-06 68T15 PDFBibTeX XMLCite \textit{G. Klein} (ed.) and \textit{R. Gamboa} (ed.), J. Autom. Reasoning 56, No. 3, 201--203 (2016; Zbl 1336.00112) Full Text: DOI
Bernardeschi, Cinzia; Domenici, Andrea Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system. (English) Zbl 1356.68177 Inf. Process. Lett. 116, No. 6, 409-415 (2016). MSC: 68T15 68Q60 93C10 93C30 PDFBibTeX XMLCite \textit{C. Bernardeschi} and \textit{A. Domenici}, Inf. Process. Lett. 116, No. 6, 409--415 (2016; Zbl 1356.68177) Full Text: DOI Link
Leino, K. Rustan M.; Lucio, Paqui An assertional proof of the stability and correctness of Natural Mergesort. (English) Zbl 1367.68080 ACM Trans. Comput. Log. 17, No. 1, Article No. 6, 22 p. (2015). MSC: 68P10 68Q60 68T15 PDFBibTeX XMLCite \textit{K. R. M. Leino} and \textit{P. Lucio}, ACM Trans. Comput. Log. 17, No. 1, Article No. 6, 22 p. (2015; Zbl 1367.68080) Full Text: DOI
Rand, Robert; Zdancewic, Steve VPHL: a verified partial-correctness logic for probabilistic programs. (English) Zbl 1351.68080 Ghica, Dan (ed.), Proceedings of the 31st conference on the mathematical foundations of programming semantics (MFPS XXXI), Nijmegen, The Netherlands, June 22–25, 2015. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 319, 351-367, electronic only (2015). MSC: 68N30 03B70 68N19 68Q87 PDFBibTeX XMLCite \textit{R. Rand} and \textit{S. Zdancewic}, Electron. Notes Theor. Comput. Sci. 319, 351--367 (2015; Zbl 1351.68080) Full Text: DOI
Bizjak, Aleš; Møgelberg, Rasmus Ejlers A model of guarded recursion with clock synchronisation. (English) Zbl 1351.68057 Ghica, Dan (ed.), Proceedings of the 31st conference on the mathematical foundations of programming semantics (MFPS XXXI), Nijmegen, The Netherlands, June 22–25, 2015. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 319, 83-101, electronic only (2015). MSC: 68N18 03B15 03B70 18C50 68N30 68Q55 PDFBibTeX XMLCite \textit{A. Bizjak} and \textit{R. E. Møgelberg}, Electron. Notes Theor. Comput. Sci. 319, 83--101 (2015; Zbl 1351.68057) Full Text: DOI
Hulette, Geoffrey C.; Armstrong, Robert C.; Mayo, Jackson R.; Ruthruff, Joseph R. Theorem-proving analysis of digital control logic interacting with continuous dynamics. (English) Zbl 1351.68249 Bogomolov, Sergiy (ed.) et al., Selected papers based on the presentations at the 7th and 8th international workshops on numerical software verification (NSV), Vienna, Austria, July 17–18, 2014 and April 13, 2015. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 317, 71-83 (2015). MSC: 68T15 68Q60 80A99 93C30 PDFBibTeX XMLCite \textit{G. C. Hulette} et al., Electron. Notes Theor. Comput. Sci. 317, 71--83 (2015; Zbl 1351.68249) Full Text: DOI
Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos; Romano, Agustín Verifying Android’s permission model. (English) Zbl 1471.68129 Leucker, Martin (ed.) et al., Theoretical aspects of computing – ICTAC 2015. 12th international colloquium, Cali, Colombia, October 29–31, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9399, 485-504 (2015). MSC: 68Q60 68M25 68N25 68V15 PDFBibTeX XMLCite \textit{G. Betarte} et al., Lect. Notes Comput. Sci. 9399, 485--504 (2015; Zbl 1471.68129) Full Text: DOI
Martin-Dorel, Érik; Hanrot, Guillaume; Mayero, Micaela; Théry, Laurent Formally verified certificate checkers for hardest-to-round computation. (English) Zbl 1315.68222 J. Autom. Reasoning 54, No. 1, 1-29 (2015). MSC: 68T15 65G99 68Q60 68W30 PDFBibTeX XMLCite \textit{É. Martin-Dorel} et al., J. Autom. Reasoning 54, No. 1, 1--29 (2015; Zbl 1315.68222) Full Text: DOI HAL
Heras, Jónathan; Martín-Mateos, Francisco Jesús; Pascual, Vico Modelling algebraic structures and morphisms in ACL2. (English) Zbl 1325.68214 Appl. Algebra Eng. Commun. Comput. 26, No. 3, 277-303 (2015). MSC: 68T15 68W30 PDFBibTeX XMLCite \textit{J. Heras} et al., Appl. Algebra Eng. Commun. Comput. 26, No. 3, 277--303 (2015; Zbl 1325.68214) Full Text: DOI Link
Moreira, Nelma; Pereira, David; Melo de Sousa, Simão Deciding Kleene algebra terms equivalence in Coq. (English) Zbl 1329.68232 J. Log. Algebr. Methods Program. 84, No. 3, 377-401 (2015). MSC: 68T15 68Q45 68Q60 PDFBibTeX XMLCite \textit{N. Moreira} et al., J. Log. Algebr. Methods Program. 84, No. 3, 377--401 (2015; Zbl 1329.68232) Full Text: DOI
Dufourd, Jean-François Formal study of functional orbits in finite domains. (English) Zbl 1317.68208 Theor. Comput. Sci. 564, 63-88 (2015). MSC: 68T15 68Q60 68Q65 68U05 PDFBibTeX XMLCite \textit{J.-F. Dufourd}, Theor. Comput. Sci. 564, 63--88 (2015; Zbl 1317.68208) Full Text: DOI
Boldo, Sylvie; Clément, François; Filliâtre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre Trusting computations: a mechanized proof from partial differential equations to actual program. (English) Zbl 1369.35051 Comput. Math. Appl. 68, No. 3, 325-352 (2014). MSC: 35Q35 65M06 68Q60 65G20 68T15 65M12 PDFBibTeX XMLCite \textit{S. Boldo} et al., Comput. Math. Appl. 68, No. 3, 325--352 (2014; Zbl 1369.35051) Full Text: DOI arXiv
Kozen, Dexter NetKAT – a formal system for the verification of networks. (English) Zbl 1453.68051 Garrigue, Jacques (ed.), Programming languages and systems. 12th Asian symposium, APLAS 2014, Singapore, Singapore, November 17–19, 2014, Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8858, 1-18 (2014). MSC: 68N30 68M10 68Q45 68Q60 PDFBibTeX XMLCite \textit{D. Kozen}, Lect. Notes Comput. Sci. 8858, 1--18 (2014; Zbl 1453.68051) Full Text: DOI
Hidalgo-Doblado, M. J.; Alonso-Jiménez, J. A.; Borrego-Díaz, J.; Martín-Mateos, F. J.; Ruiz-Reina, J. L. Formally verified tableau-based reasoners for a description logic. (English) Zbl 1314.68282 J. Autom. Reasoning 52, No. 3, 331-360 (2014). MSC: 68T15 68Q60 68T27 PDFBibTeX XMLCite \textit{M. J. Hidalgo-Doblado} et al., J. Autom. Reasoning 52, No. 3, 331--360 (2014; Zbl 1314.68282) Full Text: DOI Link
Alkassar, Eyad; Böhme, Sascha; Mehlhorn, Kurt; Rizkallah, Christine A framework for the verification of certifying computations. (English) Zbl 1314.68180 J. Autom. Reasoning 52, No. 3, 241-273 (2014). MSC: 68Q60 68T15 PDFBibTeX XMLCite \textit{E. Alkassar} et al., J. Autom. Reasoning 52, No. 3, 241--273 (2014; Zbl 1314.68180) Full Text: DOI arXiv
Muñoz, César; Narkawicz, Anthony Formalization of Bernstein polynomials and applications to global optimization. (English) Zbl 1314.68286 J. Autom. Reasoning 51, No. 2, 151-196 (2013). MSC: 68T15 65K10 PDFBibTeX XMLCite \textit{C. Muñoz} and \textit{A. Narkawicz}, J. Autom. Reasoning 51, No. 2, 151--196 (2013; Zbl 1314.68286) Full Text: DOI
Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders Refinements for free! (English) Zbl 1426.68165 Gonthier, Georges (ed.) et al., Certified programs and proofs. Third international conference, CPP 2013, Melbourne, VIC, Australia, December 11–13, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8307, 147-162 (2013). MSC: 68Q60 68V15 68V20 PDFBibTeX XMLCite \textit{C. Cohen} et al., Lect. Notes Comput. Sci. 8307, 147--162 (2013; Zbl 1426.68165) Full Text: DOI HAL
Křena, Bohuslav; Vojnar, Tomáš Automated formal analysis and verification: an overview. (English) Zbl 1286.68318 Int. J. Gen. Syst. 42, No. 4, 335-365 (2013). MSC: 68Q60 68T15 68N30 PDFBibTeX XMLCite \textit{B. Křena} and \textit{T. Vojnar}, Int. J. Gen. Syst. 42, No. 4, 335--365 (2013; Zbl 1286.68318) Full Text: DOI
Sabel, David; Schmidt-Schauß, Manfred A two-valued logic for properties of strict functional programs allowing partial functions. (English) Zbl 1267.68088 J. Autom. Reasoning 50, No. 4, 383-421 (2013). MSC: 68N18 03B70 PDFBibTeX XMLCite \textit{D. Sabel} and \textit{M. Schmidt-Schauß}, J. Autom. Reasoning 50, No. 4, 383--421 (2013; Zbl 1267.68088) Full Text: DOI
Alglave, Jade A formal hierarchy of weak memory models. (English) Zbl 1284.68157 Form. Methods Syst. Des. 41, No. 2, 178-210 (2012). MSC: 68N30 68Q55 68T15 PDFBibTeX XMLCite \textit{J. Alglave}, Form. Methods Syst. Des. 41, No. 2, 178--210 (2012; Zbl 1284.68157) Full Text: DOI
Alglave, Jade; Maranget, Luc; Sarkar, Susmit; Sewell, Peter Fences in weak memory models. (English) Zbl 1247.68155 Form. Methods Syst. Des. 40, No. 2, 170-205 (2012). MSC: 68Q60 68N30 68M99 68T15 PDFBibTeX XMLCite \textit{J. Alglave} et al., Form. Methods Syst. Des. 40, No. 2, 170--205 (2012; Zbl 1247.68155) Full Text: DOI
Moreira, Nelma; Pereira, David; Melo de Sousa, Simão Deciding regular expressions (in-)equivalence in Coq. (English) Zbl 1330.68265 Kahl, Wolfram (ed.) et al., Relational and algebraic methods in computer science. 13th international conference, RAMiCS 2012, Cambridge, UK, September 17–20, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-33313-2/pbk). Lecture Notes in Computer Science 7560, 98-113 (2012). MSC: 68T15 68Q45 68Q60 PDFBibTeX XMLCite \textit{N. Moreira} et al., Lect. Notes Comput. Sci. 7560, 98--113 (2012; Zbl 1330.68265) Full Text: DOI
de Oliveira, Diego Caminha B.; Déharbe, David; Fontaine, Pascal Combining decision procedures by (model-)equality propagation. (English) Zbl 1243.68150 Sci. Comput. Program. 77, No. 4, 518-532 (2012). MSC: 68N30 03B70 68Q60 PDFBibTeX XMLCite \textit{D. C. B. de Oliveira} et al., Sci. Comput. Program. 77, No. 4, 518--532 (2012; Zbl 1243.68150) Full Text: DOI
Ahrens, Benedikt Extended initiality for typed abstract syntax. (English) Zbl 1362.68039 Log. Methods Comput. Sci. 8, No. 2, Paper No. 1, 35 p. (2012). MSC: 68N30 18C10 18C50 68N18 68T15 PDFBibTeX XMLCite \textit{B. Ahrens}, Log. Methods Comput. Sci. 8, No. 2, Paper No. 1, 35 p. (2012; Zbl 1362.68039) Full Text: DOI arXiv
Ahrens, Benedikt; Zsido, Julianna Initial semantics for higher-order typed syntax in Coq. (English) Zbl 1451.68312 J. Formaliz. Reason. 4, No. 1, 25-69 (2011). MSC: 68V15 18C50 68N30 68Q55 68V20 PDFBibTeX XMLCite \textit{B. Ahrens} and \textit{J. Zsido}, J. Formaliz. Reason. 4, No. 1, 25--69 (2011; Zbl 1451.68312) Full Text: DOI arXiv
Boldo, Sylvie; Marché, Claude Formal verification of numerical programs: from C annotated programs to mechanical proofs. (English) Zbl 1264.68054 Math. Comput. Sci. 5, No. 4, 377-393 (2011). MSC: 68N30 68Q60 68N15 65Y04 PDFBibTeX XMLCite \textit{S. Boldo} and \textit{C. Marché}, Math. Comput. Sci. 5, No. 4, 377--393 (2011; Zbl 1264.68054) Full Text: DOI
Corbineau, Pierre; Duclos, Mathilde; Lakhnech, Yassine Certified security proofs of cryptographic protocols in the computational model: an application to intrusion resilience. (English) Zbl 1350.68229 Jouannaud, Jean-Pierre (ed.) et al., Certified programs and proofs. First international conference, CPP 2011, Kenting, Taiwan, December 7–9, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-25378-2/pbk). Lecture Notes in Computer Science 7086, 378-393 (2011). MSC: 68T15 94A60 PDFBibTeX XMLCite \textit{P. Corbineau} et al., Lect. Notes Comput. Sci. 7086, 378--393 (2011; Zbl 1350.68229) Full Text: DOI
Bickford, Mark; Constable, Robert; Halpern, Joseph; Petride, Sabina Knowledge-based synthesis of distributed systems using event structures. (English) Zbl 1213.68202 Log. Methods Comput. Sci. 7, No. 2, Paper No. 14, 36 p. (2011). MSC: 68N30 03B42 68Q45 68T15 PDFBibTeX XMLCite \textit{M. Bickford} et al., Log. Methods Comput. Sci. 7, No. 2, Paper No. 14, 36 p. (2011; Zbl 1213.68202) Full Text: DOI
Domínguez, César; Rubio, Julio Effective homology of bicomplexes, formalized in Coq. (English) Zbl 1207.68211 Theor. Comput. Sci. 412, No. 11, 962-970 (2011). MSC: 68Q65 55U15 68T15 68W30 PDFBibTeX XMLCite \textit{C. Domínguez} and \textit{J. Rubio}, Theor. Comput. Sci. 412, No. 11, 962--970 (2011; Zbl 1207.68211) Full Text: DOI
Paşca, Ioana Formally verified conditions for regularity of interval matrices. (English) Zbl 1286.68400 Autexier, Serge (ed.) et al., Intelligent computer mathematics. 10th international conference, AISC 2010, 17th symposium, Calculemus 2010, and 9th international conference, MKM 2010, Paris, France, July 5–10, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14127-0/pbk). Lecture Notes in Computer Science 6167. Lecture Notes in Artificial Intelligence, 219-233 (2010). MSC: 68T15 PDFBibTeX XMLCite \textit{I. Paşca}, Lect. Notes Comput. Sci. 6167, 219--233 (2010; Zbl 1286.68400) Full Text: DOI Link
Domínguez, César; Rubio, Julio Computing in Coq with infinite algebraic data structures. (English) Zbl 1286.68396 Autexier, Serge (ed.) et al., Intelligent computer mathematics. 10th international conference, AISC 2010, 17th symposium, Calculemus 2010, and 9th international conference, MKM 2010, Paris, France, July 5–10, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14127-0/pbk). Lecture Notes in Computer Science 6167. Lecture Notes in Artificial Intelligence, 204-218 (2010). MSC: 68T15 68Q65 68W30 PDFBibTeX XMLCite \textit{C. Domínguez} and \textit{J. Rubio}, Lect. Notes Comput. Sci. 6167, 204--218 (2010; Zbl 1286.68396) Full Text: DOI
Chiarabini, Luca Program development by proof transformation. (English) Zbl 1208.68012 München, Univ. München, Fakultät für Mathematik, Informatik und Statistik (Diss.). xiv, 118 p. (2009). MSC: 68-02 68Q60 05C70 68Q32 68T15 PDFBibTeX XMLCite \textit{L. Chiarabini}, Program development by proof transformation. München, Univ. München, Fakultät für Mathematik, Informatik und Statistik (Diss.) (2009; Zbl 1208.68012) Full Text: Link
Koprowski, Adam; Waldmann, Johannes Max/Plus tree automata for termination of term rewriting. (English) Zbl 1224.68041 Acta Cybern. 19, No. 2, 357-392 (2009). MSC: 68Q42 68Q45 16Y60 PDFBibTeX XMLCite \textit{A. Koprowski} and \textit{J. Waldmann}, Acta Cybern. 19, No. 2, 357--392 (2009; Zbl 1224.68041)
Leroy, Xavier A formally verified compiler back-end. (English) Zbl 1185.68215 J. Autom. Reasoning 43, No. 4, 363-446 (2009). MSC: 68N20 68Q60 68T15 PDFBibTeX XMLCite \textit{X. Leroy}, J. Autom. Reasoning 43, No. 4, 363--446 (2009; Zbl 1185.68215) Full Text: DOI arXiv
Schreiner, Wolfgang The RISC ProofNavigator: a proving assistant for program verification in the classroom. (English) Zbl 1162.68478 Formal Asp. Comput. 21, No. 3, 277-291 (2009). MSC: 68Q60 PDFBibTeX XMLCite \textit{W. Schreiner}, Formal Asp. Comput. 21, No. 3, 277--291 (2009; Zbl 1162.68478) Full Text: DOI HAL
Jorge, J. Santiago; Gulias, Victor M.; Freire, Jose L. Certifying properties of an efficient functional program for computing Gröbner bases. (English) Zbl 1159.13016 J. Symb. Comput. 44, No. 5, 571-582 (2009). MSC: 13P10 68W30 PDFBibTeX XMLCite \textit{J. S. Jorge} et al., J. Symb. Comput. 44, No. 5, 571--582 (2009; Zbl 1159.13016) Full Text: DOI
Jorge, J. Santiago; Gulias, Victor M.; Castro, Laura M. Using Coq to prove properties of the cache level of a functional video-on-demand server. (English) Zbl 1166.68348 Autexier, Serge (ed.) et al., Intelligent computer mathematics. 9th international conference, AISC 2008, 15th symposium, Calculemus 2008, 7th international conference, MKM 2008, Birmingham, UK, July 28–August 1, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-85109-7/pbk). Lecture Notes in Computer Science 5144. Lecture Notes in Artificial Intelligence, 296-299 (2008). MSC: 68T15 68N18 68Q60 68U35 PDFBibTeX XMLCite \textit{J. S. Jorge} et al., Lect. Notes Comput. Sci. 5144, 296--299 (2008; Zbl 1166.68348) Full Text: DOI
Boyer, Benoît; Genet, Thomas; Jensen, Thomas Certifying a tree automata completion checker. (English) Zbl 1165.68400 Armando, Alessandro (ed.) et al., Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12–15, 2008 Proceedings. Berlin: Springer (ISBN 978-3-540-71069-1/pbk). Lecture Notes in Computer Science 5195. Lecture Notes in Artificial Intelligence, 523-538 (2008). MSC: 68Q60 68Q45 PDFBibTeX XMLCite \textit{B. Boyer} et al., Lect. Notes Comput. Sci. 5195, 523--538 (2008; Zbl 1165.68400) Full Text: DOI
Niqui, Milad; Tveretina, Olga Modular development of hybrid systems for verification in Coq. (English) Zbl 1143.68580 Egerstedt, Magnus (ed.) et al., Hybrid systems: Computation and control. 11th international workshop, HSCC 2008, St. Louis, MO, USA, April 22–24, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-78928-4/pbk). Lecture Notes in Computer Science 4981, 638-641 (2008). MSC: 68T15 68Q45 68Q60 93C30 PDFBibTeX XMLCite \textit{M. Niqui} and \textit{O. Tveretina}, Lect. Notes Comput. Sci. 4981, 638--641 (2008; Zbl 1143.68580) Full Text: DOI
Jaeger, Éric; Dubois, Catherine Why would you trust \(B\)? (English) Zbl 1137.68355 Dershowitz, Nachum (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 14th international conference, LPAR 2007, Yerevan, Armenia, October 15–19, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-75558-6/pbk). Lecture Notes in Computer Science 4790. Lecture Notes in Artificial Intelligence, 288-302 (2007). MSC: 68N30 03B70 68Q60 68T15 PDFBibTeX XMLCite \textit{É. Jaeger} and \textit{C. Dubois}, Lect. Notes Comput. Sci. 4790, 288--302 (2007; Zbl 1137.68355) Full Text: DOI
Coupet-Grimal, Solange; Jakubiec, Line Certifying circuits in type theory. (English) Zbl 1061.68105 Formal Asp. Comput. 16, No. 4, 352-373 (2004). MSC: 68Q65 PDFBibTeX XMLCite \textit{S. Coupet-Grimal} and \textit{L. Jakubiec}, Formal Asp. Comput. 16, No. 4, 352--373 (2004; Zbl 1061.68105) Full Text: DOI
Marché, C.; Paulin-Mohring, C.; Urbain, X. The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML. (English) Zbl 1073.68678 J. Log. Algebr. Program. 58, No. 1-2, 89-106 (2004). MSC: 68Q60 68N15 PDFBibTeX XMLCite \textit{C. Marché} et al., J. Log. Algebr. Program. 58, No. 1--2, 89--106 (2004; Zbl 1073.68678) Full Text: DOI
Coupet-Grimal, Solange; Nouvet, Catherine Formal verification of an incremental garbage collector. (English) Zbl 1074.68548 J. Log. Comput. 13, No. 6, 815-833 (2003). MSC: 68N30 03B44 PDFBibTeX XMLCite \textit{S. Coupet-Grimal} and \textit{C. Nouvet}, J. Log. Comput. 13, No. 6, 815--833 (2003; Zbl 1074.68548) Full Text: DOI
Coupet-Grimal, Solange An axiomatization of linear temporal logic in the calculus of inductive constructions. (English) Zbl 1093.68024 J. Log. Comput. 13, No. 6, 801-813 (2003). MSC: 68N30 03B44 PDFBibTeX XMLCite \textit{S. Coupet-Grimal}, J. Log. Comput. 13, No. 6, 801--813 (2003; Zbl 1093.68024) Full Text: DOI
Brucker, Achim D.; Wolff, Burkhart Using theory morphisms for implementing formal methods tools. (English) Zbl 1023.68654 Geuvers, Herman (ed.) et al., Types for proofs and programs. International workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002. Selected papers. Berlin: Springer. Lect. Notes Comput. Sci. 2646, 59-77 (2003). MSC: 68T15 68Q60 03B70 PDFBibTeX XMLCite \textit{A. D. Brucker} and \textit{B. Wolff}, Lect. Notes Comput. Sci. 2646, 59--77 (2003; Zbl 1023.68654) Full Text: Link
Paulin-Mohring, Christine Modelisation of timed automata in Coq. (English) Zbl 1087.68575 Kobayashi, Naoki (ed.) et al., Theoretical aspects of computer software. 4th international symposium, TACS 2001, Sendai, Japan, October 29–31, 2001. Proceedings. Berlin: Springer (ISBN 3-540-42736-8/pbk). Lecture Notes in Computer Science 2215, 298-315 (2001). MSC: 68Q45 68Q60 68T15 PDFBibTeX XMLCite \textit{C. Paulin-Mohring}, Lect. Notes Comput. Sci. 2215, 298--315 (2001; Zbl 1087.68575) Full Text: Link
Monroy, Raúl; Bundy, Alan; Green, Ian Planning proofs of equations in CCS. (English) Zbl 1034.68646 Autom. Softw. Eng. 7, No. 3, 263-304 (2000). MSC: 68U99 68N99 68Q60 68T15 PDFBibTeX XML Full Text: DOI
Nipkow, Tobias; Slind, Konrad I/O automata in Isabelle/HOL. (English) Zbl 07774801 Dybjer, Peter (ed.) et al., Types for proofs and programs. International workshop TYPES ’94, Båstad, Sweden, June 6–10, 1994. Selected papers. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 996, 101-119 (1995). MSC: 68Q60 68M12 68Q10 68Q45 68V15 PDFBibTeX XMLCite \textit{T. Nipkow} and \textit{K. Slind}, Lect. Notes Comput. Sci. 996, 101--119 (1995; Zbl 07774801) Full Text: DOI