×

Found 94 Documents (Results 1–94)

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

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
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

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

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
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

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

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

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

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

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).
MSC:  68-02 65G50 65Y04 68Q60 68T15
PDFBibTeX XMLCite
Full Text: Link

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

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

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

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

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

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

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

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

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

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

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

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

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
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

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
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