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
Bian, Jinting; Hiep, Hans-Dieter A.; de Boer, Frank S.; de Gouw, Stijn Integrating ADTs in KeY and their application to history-based reasoning about collection. (English) Zbl 07785151 Form. Methods Syst. Des. 61, No. 1, 63-89 (2022). MSC: 68-XX PDFBibTeX XMLCite \textit{J. Bian} et al., Form. Methods Syst. Des. 61, No. 1, 63--89 (2022; Zbl 07785151) Full Text: DOI OA License
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
Karayel, Emin; Gonzàlez, Edgar Strong eventual consistency of the collaborative editing framework WOOT. (English) Zbl 1485.68021 Distrib. Comput. 35, No. 2, 145-164 (2022). MSC: 68M14 68P05 68Q60 68U15 68V20 PDFBibTeX XMLCite \textit{E. Karayel} and \textit{E. Gonzàlez}, Distrib. Comput. 35, No. 2, 145--164 (2022; Zbl 1485.68021) Full Text: DOI
Huerta y Munive, Jonathan Julián; Struth, Georg Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL. (English) Zbl 07498609 J. Autom. Reasoning 66, No. 1, 93-139 (2022). MSC: 68V15 PDFBibTeX XMLCite \textit{J. J. Huerta y Munive} and \textit{G. Struth}, J. Autom. Reasoning 66, No. 1, 93--139 (2022; Zbl 07498609) Full Text: DOI
Bian, Jinting; Hiep, Hans-Dieter A.; de Boer, Frank S.; de Gouw, Stijn Integrating ADTs in KeY and their application to history-based reasoning. (English) Zbl 1521.68076 Huisman, Marieke (ed.) et al., Formal methods. 24th international symposium, FM 2021, virtual event, November 20–26, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13047, 255-272 (2021). MSC: 68Q60 68Q65 68V15 PDFBibTeX XMLCite \textit{J. Bian} et al., Lect. Notes Comput. Sci. 13047, 255--272 (2021; Zbl 1521.68076) 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
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
Huerta y Munive, Jonathan Julián Affine systems of ODEs in Isabelle/HOL for hybrid-program verification. (English) Zbl 1476.68301 de Boer, Frank (ed.) et al., Software engineering and formal methods. 18th international conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12310, 77-92 (2020). MSC: 68V20 34A30 68Q60 PDFBibTeX XMLCite \textit{J. J. Huerta y Munive}, Lect. Notes Comput. Sci. 12310, 77--92 (2020; Zbl 1476.68301) Full Text: DOI
Ribeiro, Maria; Adão, Pedro; Mateus, Paulo Formal verification of Ethereum smart contracts using Isabelle/HOL. (English) Zbl 1476.68156 Nigam, Vivek (ed.) et al., Logic, language, and security. Essays dedicated to Andre Scedrov on the occasion of his 65th birthday. Cham: Springer. Lect. Notes Comput. Sci. 12300, 71-97 (2020). MSC: 68Q60 03B70 68V15 91B41 94A60 PDFBibTeX XMLCite \textit{M. Ribeiro} et al., Lect. Notes Comput. Sci. 12300, 71--97 (2020; Zbl 1476.68156) 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
Syeda, Hira Taqdees; Klein, Gerwin Formal reasoning under cached address translation. (English) Zbl 1468.68070 J. Autom. Reasoning 64, No. 5, 911-945 (2020). MSC: 68N25 03B70 68N30 68V15 PDFBibTeX XMLCite \textit{H. T. Syeda} and \textit{G. Klein}, J. Autom. Reasoning 64, No. 5, 911--945 (2020; Zbl 1468.68070) 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
Foster, Simon; Cavalcanti, Ana; Canham, Samuel; Woodcock, Jim; Zeyda, Frank Unifying theories of reactive design contracts. (English) Zbl 1436.68195 Theor. Comput. Sci. 802, 105-140 (2020). MSC: 68Q60 68Q55 68V15 PDFBibTeX XMLCite \textit{S. Foster} et al., Theor. Comput. Sci. 802, 105--140 (2020; Zbl 1436.68195) Full Text: DOI arXiv Link
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
Guttmann, Walter Verifying minimum spanning tree algorithms with Stone relation algebras. (English) Zbl 1401.68247 J. Log. Algebr. Methods Program. 101, 132-150 (2018). MSC: 68R10 03B35 03G15 05C22 68Q60 68T15 PDFBibTeX XMLCite \textit{W. Guttmann}, J. Log. Algebr. Methods Program. 101, 132--150 (2018; Zbl 1401.68247) Full Text: DOI
Schwammberger, Maike An abstract model for proving safety of autonomous urban traffic. (English) Zbl 1400.68126 Theor. Comput. Sci. 744, 143-169 (2018). MSC: 68Q60 03B70 68Q45 90B20 PDFBibTeX XMLCite \textit{M. Schwammberger}, Theor. Comput. Sci. 744, 143--169 (2018; Zbl 1400.68126) Full Text: DOI
Lochbihler, Andreas Mechanising a type-safe model of multithreaded Java with a verified compiler. (English) Zbl 1451.68178 J. Autom. Reasoning 61, No. 1-4, 243-332 (2018). MSC: 68Q60 68N15 68N20 68Q55 68V15 PDFBibTeX XMLCite \textit{A. Lochbihler}, J. Autom. Reasoning 61, No. 1--4, 243--332 (2018; Zbl 1451.68178) Full Text: DOI
Diekmann, Cornelius; Hupel, Lars; Michaelis, Julius; Haslbeck, Maximilian; Carle, Georg Verified iptables firewall analysis and verification. (English) Zbl 1451.68173 J. Autom. Reasoning 61, No. 1-4, 191-242 (2018). MSC: 68Q60 68M10 68M25 68V15 PDFBibTeX XMLCite \textit{C. Diekmann} et al., J. Autom. Reasoning 61, No. 1--4, 191--242 (2018; Zbl 1451.68173) Full Text: DOI
Bauereiß, Thomas; Pesenti Gritti, Armando; Popescu, Andrei; Raimondi, Franco CoSMed: a confidentiality-verified social media platform. (English) Zbl 1451.68168 J. Autom. Reasoning 61, No. 1-4, 113-139 (2018). MSC: 68Q60 68V15 PDFBibTeX XMLCite \textit{T. Bauereiß} et al., J. Autom. Reasoning 61, No. 1--4, 113--139 (2018; Zbl 1451.68168) Full Text: DOI Link
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
Brunner, Julian; Lammich, Peter Formal verification of an executable LTL model checker with partial order reduction. (English) Zbl 1426.68162 J. Autom. Reasoning 60, No. 1, 3-21 (2018). MSC: 68Q60 PDFBibTeX XMLCite \textit{J. Brunner} and \textit{P. Lammich}, J. Autom. Reasoning 60, No. 1, 3--21 (2018; Zbl 1426.68162) Full Text: DOI Link
Hölzl, Johannes Markov chains and Markov decision processes in Isabelle/HOL. (English) Zbl 1425.68375 J. Autom. Reasoning 59, No. 3, 345-387 (2017). MSC: 68T15 60J10 68Q60 90C40 PDFBibTeX XMLCite \textit{J. Hölzl}, J. Autom. Reasoning 59, No. 3, 345--387 (2017; Zbl 1425.68375) Full Text: DOI
Pinisetty, Srinivas; Preoteasa, Viorel; Tripakis, Stavros; Jéron, Thierry; Falcone, Yliès; Marchand, Hervé Predictive runtime enforcement. (English) Zbl 1370.68207 Form. Methods Syst. Des. 51, No. 1, 154-199 (2017). MSC: 68Q60 68Q45 PDFBibTeX XMLCite \textit{S. Pinisetty} et al., Form. Methods Syst. Des. 51, No. 1, 154--199 (2017; Zbl 1370.68207) Full Text: DOI HAL
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
Esparza, Javier; Křetínský, Jan; Sickert, Salomon From LTL to deterministic automata. A safraless compositional approach. (English) Zbl 1368.68233 Form. Methods Syst. Des. 49, No. 3, 219-271 (2016). MSC: 68Q45 03B44 03D05 68Q60 PDFBibTeX XMLCite \textit{J. Esparza} et al., Form. Methods Syst. Des. 49, No. 3, 219--271 (2016; Zbl 1368.68233) Full Text: DOI arXiv
Dongol, Brijesh; Hayes, Ian J.; Struth, Georg Convolution as a unifying concept: applications in separation logic, interval calculi, and concurrency. (English) Zbl 1367.68210 ACM Trans. Comput. Log. 17, No. 3, Article No. 15, 25 p. (2016). MSC: 68Q85 03B70 06F07 68Q55 68Q60 PDFBibTeX XMLCite \textit{B. Dongol} et al., ACM Trans. Comput. Log. 17, No. 3, Article No. 15, 25 p. (2016; Zbl 1367.68210) Full Text: DOI
Wimmer, Simon Formalized timed automata. (English) Zbl 1478.68183 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, 425-440 (2016). MSC: 68Q60 68Q45 68Q85 68V15 68V20 PDFBibTeX XMLCite \textit{S. Wimmer}, Lect. Notes Comput. Sci. 9807, 425--440 (2016; Zbl 1478.68183) Full Text: DOI
Nipkow, Tobias Automatic functional correctness proofs for functional search trees. (English) Zbl 1478.68065 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, 307-322 (2016). MSC: 68P05 68Q60 68V15 PDFBibTeX XMLCite \textit{T. Nipkow}, Lect. Notes Comput. Sci. 9807, 307--322 (2016; Zbl 1478.68065) Full Text: DOI
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
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
Berghammer, Rudolf; Höfner, Peter; Stucke, Insa Cardinality of relations and relational approximation algorithms. (English) Zbl 1351.68152 J. Log. Algebr. Methods Program. 85, No. 2, 269-286 (2016). MSC: 68Q60 03G15 68N30 68W25 PDFBibTeX XMLCite \textit{R. Berghammer} et al., J. Log. Algebr. Methods Program. 85, No. 2, 269--286 (2016; Zbl 1351.68152) Full Text: DOI
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
Zou, Liang; Zhan, Naijun; Wang, Shuling; Fränzle, Martin Formal verification of Simulink/Stateflow diagrams. (English) Zbl 1471.68159 Finkbeiner, Bernd (ed.) et al., Automated technology for verification and analysis. 13th international symposium, ATVA 2015, Shanghai, China, October 12–15, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9364, 464-481 (2015). MSC: 68Q60 68V15 93-10 93C30 93C95 PDFBibTeX XMLCite \textit{L. Zou} et al., Lect. Notes Comput. Sci. 9364, 464--481 (2015; Zbl 1471.68159) Full Text: DOI
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
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
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
Lammich, Peter; Tuerk, Thomas Applying data refinement for monadic programs to Hopcroft’s algorithm. (English) Zbl 1360.68757 Beringer, Lennart (ed.) et al., Interactive theorem proving. Third international conference, ITP 2012, Princeton, NJ, USA, August 13–15, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-32346-1/pbk). Lecture Notes in Computer Science 7406, 166-182 (2012). MSC: 68T15 68N15 68Q45 68Q60 PDFBibTeX XMLCite \textit{P. Lammich} and \textit{T. Tuerk}, Lect. Notes Comput. Sci. 7406, 166--182 (2012; Zbl 1360.68757) Full Text: DOI
Preoteasa, Viorel; Back, Ralph-Johan Invariant diagrams with data refinement. (English) Zbl 1242.68074 Formal Asp. Comput. 24, No. 1, 67-95 (2012). MSC: 68N30 68Q60 68T15 PDFBibTeX XMLCite \textit{V. Preoteasa} and \textit{R.-J. Back}, Formal Asp. Comput. 24, No. 1, 67--95 (2012; Zbl 1242.68074) Full Text: DOI
Heidarian, Faranak; Schmaltz, Julien; Vaandrager, Frits Analysis of a clock synchronization protocol for wireless sensor networks. (English) Zbl 1307.68009 Theor. Comput. Sci. 413, No. 1, 87-105 (2012). MSC: 68M14 68M10 68M12 68Q45 68Q60 68T15 PDFBibTeX XMLCite \textit{F. Heidarian} et al., Theor. Comput. Sci. 413, No. 1, 87--105 (2012; Zbl 1307.68009) Full Text: DOI
Marić, Filip; Janičić, Predrag Formalization of abstract state transition systems for SAT. (English) Zbl 1237.68179 Log. Methods Comput. Sci. 7, No. 3, Paper No. 19, 37 p. (2011). MSC: 68T15 68Q60 PDFBibTeX XMLCite \textit{F. Marić} and \textit{P. Janičić}, Log. Methods Comput. Sci. 7, No. 3, Paper No. 19, 37 p. (2011; Zbl 1237.68179) Full Text: DOI arXiv
Kammüller, Florian Mechanical analysis of finite idempotent relations. (English) Zbl 1230.68175 Fundam. Inform. 107, No. 1, 43-65 (2011). MSC: 68T15 68Q60 PDFBibTeX XMLCite \textit{F. Kammüller}, Fundam. Inform. 107, No. 1, 43--65 (2011; Zbl 1230.68175) Full Text: DOI
Lochbihler, Andreas; Bulwahn, Lukas Animating the formalised semantics of a Java-like language. (English) Zbl 1342.68294 Van Eekelen, Marko (ed.) et al., Interactive theorem proving. Second international conference, ITP 2011, Berg en Dal, The Netherlands, August 22–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22862-9/pbk). Lecture Notes in Computer Science 6898, 216-232 (2011). MSC: 68T15 68N15 68Q60 PDFBibTeX XMLCite \textit{A. Lochbihler} and \textit{L. Bulwahn}, Lect. Notes Comput. Sci. 6898, 216--232 (2011; Zbl 1342.68294) Full Text: DOI
Li, Yongjian; Hung, William N. N.; Song, Xiaoyu A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL. (English) Zbl 1244.68053 Theor. Comput. Sci. 412, No. 25, 2746-2765 (2011). MSC: 68Q60 68T15 68Q55 PDFBibTeX XMLCite \textit{Y. Li} et al., Theor. Comput. Sci. 412, No. 25, 2746--2765 (2011; Zbl 1244.68053) Full Text: DOI
Marić, Filip Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL. (English) Zbl 1208.68205 Theor. Comput. Sci. 411, No. 50, 4333-4356 (2010). MSC: 68T20 68Q60 PDFBibTeX XMLCite \textit{F. Marić}, Theor. Comput. Sci. 411, No. 50, 4333--4356 (2010; Zbl 1208.68205) Full Text: DOI
da Costa, Simone André; Ribeiro, Leila Formal verification of graph grammars using mathematical induction. (English) Zbl 1347.68243 Machado, Patricia D. L. (ed.), Proceedings of the 11th Brazilian symposium on formal methods (SBMF 2008) Salvador, Brazil, August 26–29, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 240, 43-60 (2009). MSC: 68Q60 68Q42 PDFBibTeX XMLCite \textit{S. A. da Costa} and \textit{L. Ribeiro}, Electron. Notes Theor. Comput. Sci. 240, 43--60 (2009; Zbl 1347.68243) Full Text: DOI
Klein, Gerwin Operating system verification—an overview. (English) Zbl 1192.68432 Sādhanā 34, No. 1, 27-69 (2009). MSC: 68Q60 68N25 PDFBibTeX XMLCite \textit{G. Klein}, Sādhanā 34, No. 1, 27--69 (2009; Zbl 1192.68432) Full Text: DOI
Schimpf, Alexander; Merz, Stephan; Smaus, Jan-Georg Construction of Büchi automata for LTL model checking verified in Isabelle/HOL. (English) Zbl 1252.68196 Berghofer, Stefan (ed.) et al., Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-03358-2/pbk). Lecture Notes in Computer Science 5674, 424-439 (2009). MSC: 68Q60 03B44 03D05 68T15 PDFBibTeX XMLCite \textit{A. Schimpf} et al., Lect. Notes Comput. Sci. 5674, 424--439 (2009; Zbl 1252.68196) Full Text: DOI
Alkassar, Eyad; Hillebrand, Mark A.; Leinenbach, Dirk C.; Schirmer, Norbert W.; Starostin, Artem; Tsyban, Alexandra Balancing the load. Leveraging a semantics stack for systems verification. (English) Zbl 1191.68407 J. Autom. Reasoning 42, No. 2-4, 389-454 (2009). MSC: 68Q60 68N30 03B70 PDFBibTeX XMLCite \textit{E. Alkassar} et al., J. Autom. Reasoning 42, No. 2--4, 389--454 (2009; Zbl 1191.68407) Full Text: DOI
Daum, Matthias; Dörrenbächer, Jan; Wolff, Burkhart Proving fairness and implementation correctness of a microkernel scheduler. (English) Zbl 1191.68409 J. Autom. Reasoning 42, No. 2-4, 349-388 (2009). MSC: 68Q60 68N25 68T15 PDFBibTeX XMLCite \textit{M. Daum} et al., J. Autom. Reasoning 42, No. 2--4, 349--388 (2009; Zbl 1191.68409) Full Text: DOI
Krauss, Alexander Pattern minimization problems over recursive data types. (English) Zbl 1323.68215 Proceedings of the 13th ACM SIGPLAN international conference on functional programming, ICFP ’08, Victoria, BC, Canada, September 20–28, 2008. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-59593-919-7). ACM SIGPLAN Notices 43, No. 9, 267-274 (2008). MSC: 68N30 68N18 68Q17 68Q45 68Q60 68T15 PDFBibTeX XMLCite \textit{A. Krauss}, in: Proceedings of the 13th ACM SIGPLAN international conference on functional programming, ICFP '08, Victoria, BC, Canada, September 20--28, 2008. New York, NY: Association for Computing Machinery (ACM). 267--274 (2008; Zbl 1323.68215) Full Text: DOI
Spichkova, Maria Refinement-based verification of interactive real-time systems. (English) Zbl 1283.68214 Boiten, Eerke (ed.) et al., Proceedings of the 13th BCS-FACS refinement workshop (REFINE 2008), Turku, Finland, May 27, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 214, 131-157 (2008). MSC: 68Q60 68Q85 68T15 PDFBibTeX XMLCite \textit{M. Spichkova}, Electron. Notes Theor. Comput. Sci. 214, 131--157 (2008; Zbl 1283.68214) Full Text: DOI
Lammich, Peter; Müller-Olm, Markus Conflict analysis of programs with procedures, dynamic thread creation, and monitors. (English) Zbl 1149.68355 Alpuente, María (ed.) et al., Static analysis. 15th international symposium, SAS 2008, Valencia, Spain, July 16–18, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-69163-1/pbk). Lecture Notes in Computer Science 5079, 205-220 (2008). MSC: 68N30 PDFBibTeX XMLCite \textit{P. Lammich} and \textit{M. Müller-Olm}, Lect. Notes Comput. Sci. 5079, 205--220 (2008; Zbl 1149.68355) Full Text: DOI
Barsotti, Damián; Nieto, Leonor Prensa; Tiu, Alwen Verification of clock synchronization algorithms: experiments on a combination of deductive tools. (English) Zbl 1125.68107 Formal Asp. Comput. 19, No. 3, 321-341 (2007). MSC: 68T15 68Q60 PDFBibTeX XMLCite \textit{D. Barsotti} et al., Formal Asp. Comput. 19, No. 3, 321--341 (2007; Zbl 1125.68107) Full Text: DOI Link
Helke, Steffen; Kammüller, Florian Structure preserving data abstractions for statecharts. (English) Zbl 1169.68506 Wang, Farn (ed.), Formal techniques for networked and distributed systems – FORTE 2005. 25th IFIP WG 6.1 international conference, Taipei, Taiwan, October 2–5, 2005. Proceedings. Berlin: Springer (ISBN 3-540-29189-X/pbk). Lecture Notes in Computer Science 3731, 305-319 (2005). MSC: 68Q60 68Q45 68T15 PDFBibTeX XMLCite \textit{S. Helke} and \textit{F. Kammüller}, Lect. Notes Comput. Sci. 3731, 305--319 (2005; Zbl 1169.68506) Full Text: DOI
Weber, Tjark Towards mechanized program verification with separation logic. (English) Zbl 1095.68058 Marcinkowski, Jerzy (ed.) et al., Computer science logic. 18th international workshop, CSL 2004, 13th annual conference of the EACSL, Karpacz, Poland, September 20–24, 2004. Proceedings. Berlin: Springer (ISBN 3-540-23024-6/pbk). Lecture Notes in Computer Science 3210, 250-264 (2004). MSC: 68Q60 03B70 68T15 PDFBibTeX XMLCite \textit{T. Weber}, Lect. Notes Comput. Sci. 3210, 250--264 (2004; Zbl 1095.68058) Full Text: DOI
Wang, Farn Inductive composition of numbers with maximum, minimum, and addition. (English) Zbl 1136.68429 Int. J. Found. Comput. Sci. 15, No. 6, 865-892 (2004). MSC: 68Q60 68Q10 68Q42 68Q45 68Q85 PDFBibTeX XMLCite \textit{F. Wang}, Int. J. Found. Comput. Sci. 15, No. 6, 865--892 (2004; Zbl 1136.68429) 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