×

Found 395 Documents (Results 1–100)

A naive prover for first-order logic: a minimal example of analytic completeness. (English) Zbl 07850759

Ramanayake, Revantha (ed.) et al., Automated reasoning with analytic tableaux and related methods. 32nd international conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14278, 468-480 (2023).
MSC:  68V15
PDFBibTeX XMLCite
Full Text: DOI

Verification of NP-hardness reduction functions for exact lattice problems. (English) Zbl 07838497

Pientka, Brigitte (ed.) et al., Automated deduction – CADE 29. 29th international conference on automated deduction, Rome, Italy, July 1–4, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14132, 365-381 (2023).
MSC:  03B35 68V15
PDFBibTeX XMLCite
Full Text: DOI arXiv

Quantitative robustness analysis of sensor attacks on cyber-physical systems. (English) Zbl 07807961

Proceedings of the 26th ACM international conference on hybrid systems: computation and control, HSCC 2023, part of the 16th CPS-IoT week, San Antonio, TX, USA, May 9–12, 2023. New York, NY: Association for Computing Machinery (ACM). Paper No. 20, 12 p. (2023).
MSC:  68Q45 68Q60 93C30
PDFBibTeX XMLCite
Full Text: DOI

A Coq formalization of Lebesgue induction principle and Tonelli’s theorem. (English) Zbl 1529.68315

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, 39-55 (2023).
PDFBibTeX XMLCite
Full Text: DOI HAL

A verified implementation of \(\mathrm{B}^+\)-trees in Isabelle/HOL. (English) Zbl 07719840

Seidl, Helmut (ed.) et al., Theoretical aspects of computing – ICTAC 2022. 19th international colloquium, Tbilisi, Georgia, September 27–29, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13572, 324-341 (2022).
MSC:  68Qxx
PDFBibTeX XMLCite
Full Text: DOI arXiv

Re-imagining the Isabelle archive of formal proofs. (English) Zbl 07691297

Buzzard, Kevin (ed.) et al., Intelligent computer mathematics. 15th international conference, CICM 2022, Tbilisi, Georgia, September 19–23, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13467, 162-167 (2022).
MSC:  68Vxx
PDFBibTeX XMLCite
Full Text: DOI

Formalising basic topology for computational logic in simple type theory. (English) Zbl 07691290

Buzzard, Kevin (ed.) et al., Intelligent computer mathematics. 15th international conference, CICM 2022, Tbilisi, Georgia, September 19–23, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13467, 56-74 (2022).
MSC:  68Vxx
PDFBibTeX XMLCite
Full Text: DOI

Isabelle/HOL/GST: a formal proof environment for generalized set theories. (English) Zbl 07691289

Buzzard, Kevin (ed.) et al., Intelligent computer mathematics. 15th international conference, CICM 2022, Tbilisi, Georgia, September 19–23, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13467, 38-55 (2022).
MSC:  68Vxx
PDFBibTeX XMLCite
Full Text: DOI arXiv

Generalized arrays for Stainless frames. (English) Zbl 1498.68172

Finkbeiner, Bernd (ed.) et al., Verification, model checking, and abstract interpretation. 23rd international conference, VMCAI 2022, Philadelphia, PA, USA, January 16–18, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13182, 332-354 (2022).
PDFBibTeX XMLCite
Full Text: DOI Link

Adaptive parameter tuning for reachability analysis of nonlinear systems. (English) Zbl 07807689

Proceedings of the 24th ACM international conference on hybrid systems: computation and control, HSCC 2021, part of CPS-IoT week, Nashville, TN, USA, May 19–21, 2021. New York, NY: Association for Computing Machinery (ACM). Paper No. 16, 11 p. (2021).
MSC:  68Q45 68Q60 93C30
PDFBibTeX XMLCite
Full Text: DOI Link

A mechanically verified theory of contracts. (English) Zbl 07500642

Cerone, Antonio (ed.) et al., Theoretical aspects of computing – ICTAC 2021. 18th international colloquium, virtual event, Nur-Sultan, Kazakhstan, September 8–10, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12819, 134-151 (2021).
MSC:  68Qxx
PDFBibTeX XMLCite
Full Text: DOI arXiv

Functional correctness of C implementations of Dijkstra’s, Kruskal’s, and Prim’s algorithms. (English) Zbl 1493.68216

Silva, Alexandra (ed.) et al., Computer aided verification. 33rd international conference, CAV 2021, virtual event, July 20–23, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12760, 801-826 (2021).
MSC:  68Q60 68R10 68V15
PDFBibTeX XMLCite
Full Text: DOI

Synthesis with asymptotic resource bounds. (English) Zbl 1493.68112

Silva, Alexandra (ed.) et al., Computer aided verification. 33rd international conference, CAV 2021, virtual event, July 20–23, 2021. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 12759, 783-807 (2021).
MSC:  68N30 68N18
PDFBibTeX XMLCite
Full Text: DOI arXiv

\( \pi\) with leftovers: a mechanisation in Agda. (English) Zbl 1490.68143

Peters, Kirstin (ed.) et al., Formal techniques for distributed objects, components, and systems. 41st IFIP WG 6.1 international conference, FORTE 2021, held as part of the 16th international federated conference on distributed computing techniques, DisCoTec 2021, Valletta, Malta, June 14–18, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12719, 157-174 (2021).
PDFBibTeX XMLCite
Full Text: DOI arXiv

For a few dollars more. Verified fine-grained algorithm analysis down to LLVM. (English) Zbl 1473.68222

Yoshida, Nobuko (ed.), Programming languages and systems. 30th European symposium on programming, ESOP 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12648, 292-319 (2021).
MSC:  68W40 68P10 68Q60
PDFBibTeX XMLCite
Full Text: DOI

Is Solidity solid enough? (English) Zbl 1520.91442

Bracciali, Andrea (ed.) et al., Financial cryptography and data security. FC 2019 international workshops, VOTING and WTSC, St. Kitts, St. Kitts and Nevis, February 18–22, 2019, Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 11599, 138-153 (2020).
MSC:  91G99 94A60 91-04
PDFBibTeX XMLCite
Full Text: DOI

The Imandra automated reasoning system (system description). (English) Zbl 07614691

Peltier, Nicolas (ed.) et al., Automated reasoning. 10th international joint conference, IJCAR 2020, Paris, France, July 1–4, 2020. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12167, 464-471 (2020).
MSC:  68V15
PDFBibTeX XMLCite
Full Text: DOI arXiv

Extensible extraction of efficient imperative programs with foreign functions, manually managed memory, and proofs. (English) Zbl 07614665

Peltier, Nicolas (ed.) et al., Automated reasoning. 10th international joint conference, IJCAR 2020, Paris, France, July 1–4, 2020. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12167, 119-137 (2020).
MSC:  68V15
PDFBibTeX XMLCite
Full Text: DOI

A formalization of properties of continuous functions on closed intervals. (English) Zbl 1503.68298

Bigatti, Anna Maria (ed.) et al., Mathematical software – ICMS 2020. 7th international conference, Braunschweig, Germany, July 13–16, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12097, 272-280 (2020).
PDFBibTeX XMLCite
Full Text: DOI

Verifying selective CPS transformation for shift and reset. (English) Zbl 1503.68037

Bowman, William J. (ed.) et al., Trends in functional programming. 20th international symposium, TFP 2019, Vancouver, BC, Canada, June 12–14, 2019. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 12053, 38-57 (2020).
MSC:  68N18 68V20
PDFBibTeX XMLCite
Full Text: DOI

Verified decision procedures for modal logics. (English) Zbl 07649980

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 31, 19 p. (2019).
MSC:  68V15 03B45
PDFBibTeX XMLCite
Full Text: DOI

Quantitative continuity and computable analysis in Coq. (English) Zbl 07649977

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 28, 21 p. (2019).
MSC:  68V15
PDFBibTeX XMLCite
Full Text: DOI

Ornaments for proof reuse in Coq. (English) Zbl 07649975

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 26, 19 p. (2019).
MSC:  68V15
PDFBibTeX XMLCite
Full Text: DOI

Binary-compatible verification of filesystems with ACL2. (English) Zbl 07649974

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 25, 18 p. (2019).
MSC:  68V15
PDFBibTeX XMLCite
Full Text: DOI

Proof pearl: Purely functional, simple and efficient priority search trees and applications to Prim and Dijkstra. (English) Zbl 07649972

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 23, 18 p. (2019).
MSC:  68P05
PDFBibTeX XMLCite
Full Text: DOI

Refinement with time – refining the run-time of algorithms in Isabelle/HOL. (English) Zbl 07649969

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 20, 18 p. (2019).
MSC:  68V15
PDFBibTeX XMLCite
Full Text: DOI

A certifying extraction with time bounds from Coq to call-by-value lambda calculus. (English) Zbl 07649966

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 17, 19 p. (2019).
MSC:  68V15
PDFBibTeX XMLCite
Full Text: DOI arXiv

Nine chapters of analytic number theory in Isabelle/HOL. (English) Zbl 07649965

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 16, 19 p. (2019).
MSC:  68V20
PDFBibTeX XMLCite
Full Text: DOI

Generic authenticated data structures, formally. (English) Zbl 07649959

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 10, 18 p. (2019).
MSC:  68P05 68V15
PDFBibTeX XMLCite
Full Text: DOI

Higher-order Tarski Grothendieck as a foundation for formal proof. (English) Zbl 07649958

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 9, 16 p. (2019).
MSC:  68V20
PDFBibTeX XMLCite
Full Text: DOI

A certificate-based approach to formally verified approximations. (English) Zbl 07649957

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 8, 19 p. (2019).
MSC:  68V15
PDFBibTeX XMLCite
Full Text: DOI

Data types as quotients of polynomial functors. (English) Zbl 07649955

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 6, 19 p. (2019).
MSC:  68Q65
PDFBibTeX XMLCite
Full Text: DOI

Proving type class laws for Haskell. (English) Zbl 1495.68034

Van Horn, David (ed.) et al., Trends in functional programming. 17th international conference, TFP 2016, College Park, MD, USA, June 8–10, 2016. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 10447, 61-74 (2019).
MSC:  68N18 16Y60 68V15
PDFBibTeX XMLCite
Full Text: DOI arXiv

Verified real asymptotics in Isabelle/HOL. (English) Zbl 1467.68204

Bradford, Russell (ed.), Proceedings of the 44th international symposium on symbolic and algebraic computation, ISSAC ’19, Beijing, China, July 15–18, 2019. New York, NY: Association for Computing Machinery (ACM). 147-154 (2019).
MSC:  68V15 26A03 68W30
PDFBibTeX XMLCite
Full Text: DOI

Towards bit-width-independent proofs in SMT solvers. (English) Zbl 1535.68454

Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 366-384 (2019).
MSC:  68V15
PDFBibTeX XMLCite
Full Text: DOI arXiv

\(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic. (English) Zbl 1535.03178

Fontaine, Pascal (ed.), Automated deduction – CADE 27. 27th international conference on automated deduction, Natal, Brazil, August 27–30, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11716, 94-110 (2019).
MSC:  03B70 68V15
PDFBibTeX XMLCite
Full Text: DOI

Hybrid relations in Isabelle/UTP. (English) Zbl 07168637

Ribeiro, Pedro (ed.) et al., Unifying theories of programming. 7th international symposium, UTP 2019, dedicated to Tony Hoare on the occasion of his 85th birthday, Porto, Portugal, October 8, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11885, 130-153 (2019).
MSC:  68Q60 68V20 93C30
PDFBibTeX XMLCite
Full Text: DOI 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