×

Found 162 Documents (Results 1–100)

Formalization of functional block diagrams using HOL theorem proving. (English) Zbl 1528.68395

Lima, Lucas (ed.) et al., Formal methods: foundations and applications. 25th Brazilian symposium, SBMF 2022, virtual event, December 6–9, 2022. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13768, 22-35 (2022).
MSC:  68V20 68M15 90B25
PDFBibTeX XMLCite
Full Text: DOI

Formalization of RBD-based cause consequence analysis in HOL. (English) Zbl 1485.68289

Kamareddine, Fairouz (ed.) et al., Intelligent computer mathematics. 14th international conference, CICM 2021, Timisoara, Romania, July 26–31, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12833, 47-64 (2021).
MSC:  68V20 68M15 90B25
PDFBibTeX XMLCite
Full Text: DOI

Deductive verification of floating-point Java programs in KeY. (English) Zbl 1474.68186

Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 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. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12652, 242-261 (2021).
MSC:  68Q60 65G50 68N15
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

Deductive binary code verification against source-code-level specifications. (English) Zbl 1511.68080

Ahrendt, Wolfgang (ed.) et al., Tests and proofs. 14th international conference, TAP 2020, held as part of STAF 2020, Bergen, Norway, June 22–23, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12165, 43-58 (2020).
MSC:  68N30 68N20
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

A verified compiler from Isabelle/HOL to CakeML. (English) Zbl 1418.68045

Ahmed, Amal (ed.), Programming languages and systems. 27th European symposium on programming, ESOP 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. 10801, 999-1026 (2018).
MSC:  68N20 68N18 68T15
PDFBibTeX XMLCite
Full Text: DOI

Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions. (English) Zbl 1468.68060

Galmiche, Didier (ed.) et al., Automated reasoning. 9th international joint conference, IJCAR 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14–17, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10900, 646-662 (2018).
MSC:  68N18 68N20 68V15
PDFBibTeX XMLCite
Full Text: DOI

Program verification in the presence of cached address translation. (English) Zbl 1468.68069

Avigad, Jeremy (ed.) et al., Interactive theorem proving. 9th international conference, ITP 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10895, 542-559 (2018).
PDFBibTeX XMLCite
Full Text: DOI

How to simulate it in Isabelle: towards formal proof for secure multi-party computation. (English) Zbl 1483.68486

Ayala-Rincón, Mauricio (ed.) et al., Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26–29, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10499, 114-130 (2017).
PDFBibTeX XMLCite
Full Text: DOI arXiv

A verified algorithm enumerating event structures. (English) Zbl 1367.68245

Geuvers, Herman (ed.) et al., Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17–21, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-62074-9/pbk; 978-3-319-62075-6/ebook). Lecture Notes in Computer Science 10383. Lecture Notes in Artificial Intelligence, 239-254 (2017).
MSC:  68T15 05A15 06-04 68Q10 68U35
PDFBibTeX XMLCite
Full Text: DOI arXiv Link

Theory morphisms in Church’s type theory with quotation and evaluation. (English) Zbl 1367.68302

Geuvers, Herman (ed.) et al., Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17–21, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-62074-9/pbk; 978-3-319-62075-6/ebook). Lecture Notes in Computer Science 10383. Lecture Notes in Artificial Intelligence, 147-162 (2017).
MSC:  68T30 03B15 68W30
PDFBibTeX XMLCite
Full Text: DOI arXiv

Friends with benefits. Implementing corecursion in foundational proof assistants. (English) Zbl 1485.68280

Yang, Hongseok (ed.), Programming languages and systems. 26th European symposium on programming, ESOP 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 10201, 111-140 (2017).
MSC:  68V15
PDFBibTeX XMLCite
Full Text: DOI

Equational reasoning with applicative functors. (English) Zbl 1464.68063

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, 252-273 (2016).
MSC:  68N18 18A99 68V15
PDFBibTeX XMLCite
Full Text: DOI

An Isabelle/HOL formalisation of Green’s theorem. (English) Zbl 1468.68312

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, 3-19 (2016).
MSC:  68V20 26B20
PDFBibTeX XMLCite
Full Text: DOI Link

Translating Scala programs to Isabelle/HOL. System description. (English) Zbl 1475.68437

Olivetti, Nicola (ed.) et al., Automated reasoning. 8th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9706, 568-577 (2016).
MSC:  68V15 68Q60
PDFBibTeX XMLCite
Full Text: DOI arXiv

A verified SAT solver framework with learn, forget, restart, and incrementality. (English) Zbl 1475.68432

Olivetti, Nicola (ed.) et al., Automated reasoning. 8th international joint conference, IJCAR 2016, Coimbra, Portugal, June 27 – July 2, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9706, 25-44 (2016).
MSC:  68V15 68T05 68T20
PDFBibTeX XMLCite
Full Text: DOI HAL

Pattern matches in HOL: a new representation and improved code generation. (English) Zbl 1465.68299

Urban, Christian (ed.) et al., Interactive theorem proving. 6th international conference, ITP 2015, Nanjing, China, August 24–27, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9236, 453-468 (2015).
MSC:  68V15 68N30
PDFBibTeX XMLCite
Full Text: DOI

Proof-producing reflection for HOL. With an application to model polymorphism. (English) Zbl 1465.03052

Urban, Christian (ed.) et al., Interactive theorem proving. 6th international conference, ITP 2015, Nanjing, China, August 24–27, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9236, 170-186 (2015).
PDFBibTeX XMLCite
Full Text: DOI

Truly modular (co)datatypes for Isabelle/HOL. (English) Zbl 1416.68151

Klein, Gerwin (ed.) et al., Interactive theorem proving. 5th international conference, ITP 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8558, 93-110 (2014).
MSC:  68T15
PDFBibTeX XMLCite
Full Text: DOI Link

Steps towards verified implementations of HOL Light. (English) Zbl 1317.68225

Blazy, Sandrine (ed.) et al., Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22–26, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39633-5/pbk). Lecture Notes in Computer Science 7998, 490-495 (2013).
MSC:  68T15
PDFBibTeX XMLCite
Full Text: DOI

Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving. (English) Zbl 1362.68251

Proceedings of the 2012 27th annual ACM/IEEE symposium on logic in computer science, LICS 2012, Dubrovnik, Croatia, June 25–28, 2012. Los Alamitos, CA: IEEE Computer Society (ISBN 978-0-7695-4769-5). 596-605 (2012).
MSC:  68T15 68Q65
PDFBibTeX XMLCite
Full Text: DOI

Proof-producing synthesis of ML from higher-order logic. (English) Zbl 1291.68364

Proceedings of the 17th ACM SIGPLAN international conference on functional programming, ICFP ’12, Copenhagen, Denmark, September 9–15, 2012. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-1054-3). ACM SIGPLAN Notices 47, No. 9, 115-126 (2012).
MSC:  68T15 68N18
PDFBibTeX XMLCite
Full Text: DOI

Standalone tactics using OpenTheory. (English) Zbl 1360.68756

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, 405-411 (2012).
MSC:  68T15
PDFBibTeX XMLCite
Full Text: DOI

Stateless HOL. (English) Zbl 1457.68300

Hirschowitz, Tom (ed.), Types for proofs and programs. Revised selected papers, Aussois, France, May 12–15, 2009. Proceeedings. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 53, 47-61 (2011).
MSC:  68V15
PDFBibTeX XMLCite
Full Text: arXiv Link

Simple, functional, sound and complete parsing for all context-free grammars. (English) Zbl 1350.68164

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, 103-118 (2011).
MSC:  68Q42 68T15
PDFBibTeX XMLCite
Full Text: DOI

Mechanised computability theory. (English) Zbl 1342.68299

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, 297-311 (2011).
MSC:  68T15 03B40 03D20 03D25 68Q05
PDFBibTeX XMLCite
Full Text: DOI

Validating QBF validity in HOL4. (English) Zbl 1342.68290

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, 168-183 (2011).
MSC:  68T15
PDFBibTeX XMLCite
Full Text: DOI

Termination of Isabelle functions via termination of rewriting. (English) Zbl 1342.68289

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, 152-167 (2011).
MSC:  68T15 68Q42
PDFBibTeX XMLCite
Full Text: DOI

On the formalization of the Lebesgue integration theory in HOL. (English) Zbl 1291.68362

Kaufmann, Matt (ed.) et al., Interactive theorem proving. First international conference, ITP 2010, Edinburgh, UK, July 11–14, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14051-8/pbk). Lecture Notes in Computer Science 6172, 387-402 (2010).
MSC:  68T15 26A42
PDFBibTeX XMLCite
Full Text: DOI

Nitpick: a counterexample generator for higher-order logic based on a relational model finder. (English) Zbl 1291.68326

Kaufmann, Matt (ed.) et al., Interactive theorem proving. First international conference, ITP 2010, Edinburgh, UK, July 11–14, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-14051-8/pbk). Lecture Notes in Computer Science 6172, 131-146 (2010).
MSC:  68T15
PDFBibTeX XMLCite
Full Text: DOI

Verifying distributed systems: the operational approach. (English) Zbl 1315.68105

Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’09, Savannah, GA, USA, January 18–24, 2009. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-60558-379-2). 429-440 (2009).
MSC:  68N30 68N19 68M14 68Q60 68T15
PDFBibTeX XMLCite
Full Text: DOI

LCF-style platform based on multiway decision graphs. (English) Zbl 1347.68299

Falaschi, Moreno (ed.), Proceedings of the 17th international workshop on functional and (constraint) logic programming (WFLP 2008), Siena, Italy, July 3–4, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 246, 3-26 (2009).
MSC:  68T15 68Q60
PDFBibTeX XMLCite
Full Text: DOI

Transforming programs into recursive functions. (English) Zbl 1347.68304

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, 185-200 (2009).
MSC:  68T15 68N30 68Q60
PDFBibTeX XMLCite
Full Text: DOI

Formalising FinFuns – generating code for functions as data from Isabelle/HOL. (English) Zbl 1252.68260

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, 310-326 (2009).
MSC:  68T15
PDFBibTeX XMLCite
Full Text: DOI

A purely definitional universal domain. (English) Zbl 1252.68065

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, 260-275 (2009).
MSC:  68N18 68T15 68Q55
PDFBibTeX XMLCite
Full Text: DOI

Formal analysis of optical waveguides in HOL. (English) Zbl 1252.68256

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, 228-243 (2009).
MSC:  68T15
PDFBibTeX XMLCite
Full Text: DOI

Using structural recursion for corecursion. (English) Zbl 1246.68196

Berardi, Stefano (ed.) et al., Types for proofs and programs. International conference, TYPES 2008, Torino, Italy, March 26–29, 2008. Revised selected papers. Berlin: Springer (ISBN 978-3-642-02443-6/pbk). Lecture Notes in Computer Science 5497, 220-236 (2009).
MSC:  68T15 03B35
PDFBibTeX XMLCite
Full Text: DOI Link

Local theory specifications in Isabelle/Isar. (English) Zbl 1246.68197

Berardi, Stefano (ed.) et al., Types for proofs and programs. International conference, TYPES 2008, Torino, Italy, March 26–29, 2008. Revised selected papers. Berlin: Springer (ISBN 978-3-642-02443-6/pbk). Lecture Notes in Computer Science 5497, 153-168 (2009).
MSC:  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

Filter Results by …

Document Type

all top 5

Author

all top 5

Year of Publication

all top 3

Main Field

all top 3

Software