×

Found 60 Documents (Results 1–60)

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).
PDFBibTeX XMLCite
Full Text: DOI arXiv

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
Full Text: DOI

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
Full Text: DOI

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
Full Text: DOI

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
Full Text: DOI arXiv

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).
PDFBibTeX XMLCite
Full Text: DOI

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).
PDFBibTeX XMLCite
Full Text: DOI

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).
PDFBibTeX XMLCite
Full Text: DOI

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
Full Text: DOI

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
Full Text: DOI

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
Full Text: DOI

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
Full Text: DOI

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
Full Text: DOI

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
Full Text: DOI

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
Full Text: DOI

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
Full Text: DOI

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
Full Text: Link

Filter Results by …

Document Type

all top 5

Author

all top 5

Year of Publication

all top 3

Main Field

all top 3

Software