|
|
|
|
Venues (Conferences, Journals, ...)
|
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
The graphs summarize 188 occurrences of 119 keywords
|
|
|
|
|
Results
Found 460 publication records. Showing 460 according to the selection in the facets
| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 32 | Yutaka Nagashima, Zijin Xu, Ningli Wang, Daniel Sebastian Goc, James Bang |
Template-Based Conjecturing for Automated Induction in Isabelle/HOL.  |
FSEN  |
2023 |
DBLP DOI BibTeX RDF |
|
| 32 | Martin Bromberger, Martin Desharnais, Christoph Weidenbach |
An Isabelle/HOL Formalization of the SCL(FOL) Calculus. |
CADE |
2023 |
DBLP DOI BibTeX RDF |
|
| 32 | Angeliki Koutsoukou-Argyraki |
Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk). |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 32 | Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato 0001 |
Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL. |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 32 | Akihisa Yamada 0002, Jérémy Dubut |
Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl). |
ITP |
2023 |
DBLP DOI BibTeX RDF |
|
| 32 | Angeliki Koutsoukou-Argyraki, Mantas Baksys, Chelsea Edmonds |
A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 32 | Katherine Kosaian, Yong Kiam Tan, André Platzer |
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 32 | Brae J. Webb, Ian J. Hayes, Mark Utting |
Verifying Term Graph Optimizations using Isabelle/HOL. |
CPP |
2023 |
DBLP DOI BibTeX RDF |
|
| 32 | Fang Yan, Simon Foster 0001, Ibrahim Habli |
Automated Compositional Verification for Robotic State Machines using Isabelle/HOL. |
ICECCS |
2023 |
DBLP DOI BibTeX RDF |
|
| 32 | Simon Foster 0001, Burkhart Wolff |
Automated Reasoning for Physical Quantities, Units, and Measurements in Isabelle/HOL. |
ICECCS |
2023 |
DBLP DOI BibTeX RDF |
|
| 32 | Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds 0001, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli |
Automatic Verification of SMT Rewrites in Isabelle/HOL. |
SMT |
2023 |
DBLP BibTeX RDF |
|
| 32 | Jonas Bayer, Alexey Gonus, Christoph Benzmüller, Dana S. Scott |
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation. |
CICM |
2023 |
DBLP DOI BibTeX RDF |
|
| 32 | Aabid Seeyal Abdul Kharim, T. V. H. Prathamesh, Shweta Rajiv, Rishi Vyas |
Formalizing Free Groups in Isabelle/HOL: The Nielsen-Schreier Theorem and the Conjugacy Problem. |
CICM |
2023 |
DBLP DOI BibTeX RDF |
|
| 32 | Mirna Dzamonja, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson |
Formalizing Ordinal Partition Relations Using Isabelle/HOL. |
Exp. Math. |
2022 |
DBLP DOI BibTeX RDF |
|
| 32 | Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson |
Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL. |
Exp. Math. |
2022 |
DBLP DOI BibTeX RDF |
|
| 32 | Katherine Kosaian, Yong Kiam Tan, André Platzer |
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. |
CoRR |
2022 |
DBLP DOI BibTeX RDF |
|
| 32 | Ciarán Dunne, J. B. Wells |
Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories. |
CoRR |
2022 |
DBLP DOI BibTeX RDF |
|
| 32 | Brae J. Webb, Ian J. Hayes, Mark Utting |
Verifying term graph optimizations using Isabelle/HOL. |
CoRR |
2022 |
DBLP DOI BibTeX RDF |
|
| 32 | Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson |
Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL. |
CoRR |
2022 |
DBLP DOI BibTeX RDF |
|
| 32 | Yutaka Nagashima, Zijin Xu, Ningli Wang, Daniel Sebastian Goc, James Bang |
Property-Based Conjecturing for Automated Induction in Isabelle/HOL. |
CoRR |
2022 |
DBLP DOI BibTeX RDF |
|
| 32 | Wilayat Khan, Zhe Hou, David Sanán, Jamel Nebhen, Yang Liu 0003, Alwen Tiu |
An Executable Formal Model of the VHDL in Isabelle/HOL. |
CoRR |
2022 |
DBLP BibTeX RDF |
|
| 32 | Niels Mündler, Tobias Nipkow |
A Verified Implementation of B+-Trees in Isabelle/HOL. |
CoRR |
2022 |
DBLP DOI BibTeX RDF |
|
| 32 | Jeffrey Ketland |
Boolos's Curious Inference in Isabelle/HOL. |
Arch. Formal Proofs |
2022 |
DBLP BibTeX RDF |
|
| 32 | Christoph Benzmüller, David Fuenmayor, Alexander Steen, Geoff Sutcliffe |
Automation of Boolos' Curious Inference in Isabelle/HOL. |
Arch. Formal Proofs |
2022 |
DBLP BibTeX RDF |
|
| 32 | Katherine Cordwell, Yong Kiam Tan, André Platzer |
A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL. |
Arch. Formal Proofs |
2022 |
DBLP BibTeX RDF |
|
| 32 | Sadegh Dalvandi, Brijesh Dongol, Simon Doherty, Heike Wehrheim |
Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 32 | Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot |
Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL. |
J. Autom. Reason. |
2022 |
DBLP DOI BibTeX RDF |
|
| 32 | Dongchen Jiang, Bo Xu |
Generation of C++ Code from Isabelle/HOL Specification. |
Int. J. Softw. Eng. Knowl. Eng. |
2022 |
DBLP DOI BibTeX RDF |
|
| 32 | Niels Mündler, Tobias Nipkow |
A Verified Implementation of B+-Trees in Isabelle/HOL. |
ICTAC |
2022 |
DBLP DOI BibTeX RDF |
|
| 32 | Sharar Ahmadi, Brijesh Dongol, Matt Griffin |
Proving Memory Access Violations in Isabelle/HOL. |
FTSCS |
2022 |
DBLP DOI BibTeX RDF |
|
| 32 | Xavier Parent, Christoph Benzmüller |
Automated Verification of Deontic Correspondences in Isabelle/HOL - First Results. |
ARQNL@IJCAR |
2022 |
DBLP BibTeX RDF |
|
| 32 | Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato 0001 |
Program Logic for Higher-Order Probabilistic Programs in Isabelle/HOL. |
FLOPS |
2022 |
DBLP DOI BibTeX RDF |
|
| 32 | Asta Halkjær From, Frederik Krogsdal Jacobsen |
Verifying a Sequent Calculus Prover for First-Order Logic with Functions in Isabelle/HOL. |
ITP |
2022 |
DBLP DOI BibTeX RDF |
|
| 32 | Mihails Milehins |
An extension of the framework types-to-sets for Isabelle/HOL. |
CPP |
2022 |
DBLP DOI BibTeX RDF |
|
| 32 | Ciarán Dunne, J. B. Wells |
Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories. |
CICM |
2022 |
DBLP DOI BibTeX RDF |
|
| 32 | Daniel Kirchner |
Computer-Verified Foundations of Metaphysics and an Ontology of Natural Numbers in Isabelle/HOL. |
|
2022 |
RDF |
|
| 32 | Zhenjiang Qian, Wei Liu, Yiyang Yao |
Verification of Operating Systems for Internet of Things in Smart Cities From the Assembly Perspective Using Isabelle/HOL. |
IEEE Access |
2021 |
DBLP DOI BibTeX RDF |
|
| 32 | Haitao Wang 0024, Lihua Song |
Study of Isabelle/HOL on Formal Algorithm Analysis and Code Generation. |
IEEE Access |
2021 |
DBLP DOI BibTeX RDF |
|
| 32 | Martin Raska, Stepán Starosta |
Producing symmetrical facts for lists induced by the list reversal mapping in Isabelle/HOL. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
| 32 | Laura Kovács, Hanna Lachnitt, Stefan Szeider |
Formalizing Graph Trail Properties in Isabelle/HOL. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
| 32 | Asta Halkjær From, Frederik Krogsdal Jacobsen, Jørgen Villadsen |
SeCaV: A Sequent Calculus Verifier in Isabelle/HOL. |
LSFA |
2021 |
DBLP DOI BibTeX RDF |
|
| 32 | Mnacho Echenim, Mehdi Mhalla |
Quantum projective measurements and the CHSH inequality in Isabelle/HOL. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
| 32 | Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot |
Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
| 32 | David Fuenmayor |
Topological semantics for paraconsistent and paracomplete logics in Isabelle/HOL. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
| 32 | Simon Foster 0001, Chung-Kil Hur, Jim Woodcock 0001 |
Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
| 32 | Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson |
Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
| 32 | Simon Foster 0001, Jonathan Julián Huerta y Munive, Mario Gleirscher, Georg Struth |
Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
| 32 | Mark Chevallier, Jacques D. Fleuriot |
Formalising the Foundations of Discrete Reinforcement Learning in Isabelle/HOL. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
| 32 | Thomas Hickman, Christian Pardillo Laursen, Simon Foster 0001 |
Certifying Differential Equation Solutions from Computer Algebra Systems in Isabelle/HOL. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
| 32 | Lukas Stevens, Tobias Nipkow |
A Verified Decision Procedure for Orders in Isabelle/HOL. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
| 32 | Christoph Benzmüller |
Exploring Simplified Variants of Gödel's Ontological Argument in Isabelle/HOL. |
Arch. Formal Proofs |
2021 |
DBLP BibTeX RDF |
|
| 32 | Christoph Benzmüller, Sebastian Reiche |
Automating Public Announcement Logic and the Wise Men Puzzle in Isabelle/HOL. |
Arch. Formal Proofs |
2021 |
DBLP BibTeX RDF |
|
| 32 | Zhé Hóu, David Sanán, Alwen Tiu, Yang Liu 0003, Koh Chuen Hoa, Jin Song Dong |
An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory Model. |
J. Autom. Reason. |
2021 |
DBLP DOI BibTeX RDF |
|
| 32 | Anthony Bordg, Hanna Lachnitt, Yijun He |
Certified Quantum Computation in Isabelle/HOL. |
J. Autom. Reason. |
2021 |
DBLP DOI BibTeX RDF |
|
| 32 | Asta Halkjær From, Anders Schlichtkrull, Jørgen Villadsen |
A Sequent Calculus for First-Order Logic Formalized in Isabelle/HOL. |
CILC |
2021 |
DBLP BibTeX RDF |
|
| 32 | Simon Foster 0001, Jonathan Julián Huerta y Munive, Mario Gleirscher, Georg Struth |
Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs. |
FM |
2021 |
DBLP DOI BibTeX RDF |
|
| 32 | Matt Griffin, Brijesh Dongol |
Verifying Secure Speculation in Isabelle/HOL. |
FM |
2021 |
DBLP DOI BibTeX RDF |
|
| 32 | Lukas Stevens, Tobias Nipkow |
A Verified Decision Procedure for Orders in Isabelle/HOL. |
ATVA |
2021 |
DBLP DOI BibTeX RDF |
|
| 32 | Stepan Holub, Stepán Starosta |
Lyndon Words Formalized in Isabelle/HOL. |
DLT |
2021 |
DBLP DOI BibTeX RDF |
|
| 32 | Alexander Birch Jensen |
Towards Verifying GOAL Agents in Isabelle/HOL. |
ICAART (1) |
2021 |
DBLP DOI BibTeX RDF |
|
| 32 | Christoph Benzmüller, David Fuenmayor |
Value-Oriented Legal Argumentation in Isabelle/HOL. |
ITP |
2021 |
DBLP DOI BibTeX RDF |
|
| 32 | Max W. Haslbeck, René Thiemann |
An Isabelle/HOL formalization of AProVE's termination method for LLVM IR. |
CPP |
2021 |
DBLP DOI BibTeX RDF |
|
| 32 | Simon Foster 0001, Chung-Kil Hur, Jim Woodcock 0001 |
Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL. |
CONCUR |
2021 |
DBLP DOI BibTeX RDF |
|
| 32 | Yutaka Nagashima |
Faster Smarter Proof by Induction in Isabelle/HOL. |
IJCAI |
2021 |
DBLP DOI BibTeX RDF |
|
| 32 | Diego Marmsoler, Achim D. Brucker |
A Denotational Semantics of Solidity in Isabelle/HOL. |
SEFM |
2021 |
DBLP DOI BibTeX RDF |
|
| 32 | Stepan Holub |
Computing the Border Array in Isabelle/HOL (short paper). |
CICM Workshops |
2021 |
DBLP BibTeX RDF |
|
| 32 | Martin Raska, Stepán Starosta |
Producing Symmetrical Facts for lIsts induced by the List Reversal Mapping in Isabelle/HOL (short paper). |
CICM Workshops |
2021 |
DBLP BibTeX RDF |
|
| 32 | Asta Halkjær From, Agnes Moesgård Eschen, Jørgen Villadsen |
Formalizing Axiomatic Systems for Propositional Logic in Isabelle/HOL. |
CICM |
2021 |
DBLP DOI BibTeX RDF |
|
| 32 | Alfio Ricardo de Brito Martini |
Reasoning about Partial Correctness Assertions in Isabelle/HOL. |
RITA |
2020 |
DBLP DOI BibTeX RDF |
|
| 32 | Yutaka Nagashima |
Simple Dataset for Proof Method Recommendation in Isabelle/HOL (Dataset Description). |
CoRR |
2020 |
DBLP BibTeX RDF |
|
| 32 | Sadegh Dalvandi, Brijesh Dongol, Simon Doherty |
Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL. |
CoRR |
2020 |
DBLP BibTeX RDF |
|
| 32 | Yutaka Nagashima |
Smart Induction for Isabelle/HOL (System Description). |
CoRR |
2020 |
DBLP BibTeX RDF |
|
| 32 | Asta Halkjær From, Jørgen Villadsen, Patrick Blackburn |
Isabelle/HOL as a Meta-Language for Teaching Logic. |
ThEdu@IJCAR |
2020 |
DBLP DOI BibTeX RDF |
|
| 32 | Anthony Bordg, Hanna Lachnitt, Yijun He |
Certified Quantum Computation in Isabelle/HOL. |
CoRR |
2020 |
DBLP BibTeX RDF |
|
| 32 | Yutaka Nagashima |
Towards United Reasoning for Automatic Induction in Isabelle/HOL. |
CoRR |
2020 |
DBLP BibTeX RDF |
|
| 32 | Yutaka Nagashima |
SeLFiE: Modular Semantic Reasoning for Induction in Isabelle/HOL. |
CoRR |
2020 |
DBLP BibTeX RDF |
|
| 32 | Yutaka Nagashima |
Faster Smarter Induction in Isabelle/HOL with SeLFiE. |
CoRR |
2020 |
DBLP BibTeX RDF |
|
| 32 | Filip Maric, Sana Stojanovic-Durdevic |
Formalizing IMO Problems and Solutions in Isabelle/HOL. |
ThEdu@IJCAR |
2020 |
DBLP DOI BibTeX RDF |
|
| 32 | Salomon Sickert |
An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation. |
Arch. Formal Proofs |
2020 |
DBLP BibTeX RDF |
|
| 32 | René Thiemann, Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan J. C. Joosten, Akihisa Yamada 0002 |
Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL. |
J. Autom. Reason. |
2020 |
DBLP DOI BibTeX RDF |
|
| 32 | Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada 0002 |
A Verified Implementation of Algebraic Numbers in Isabelle/HOL. |
J. Autom. Reason. |
2020 |
DBLP DOI BibTeX RDF |
|
| 32 | Mnacho Echenim, Hervé Guiol, Nicolas Peltier |
Formalizing the Cox-Ross-Rubinstein Pricing of European Derivatives in Isabelle/HOL. |
J. Autom. Reason. |
2020 |
DBLP DOI BibTeX RDF |
|
| 32 | Wenda Li, Lawrence C. Paulson |
Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL. |
J. Autom. Reason. |
2020 |
DBLP DOI BibTeX RDF |
|
| 32 | Simon Foster 0001, Jonathan Julián Huerta y Munive, Georg Struth |
Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL. |
RAMiCS |
2020 |
DBLP DOI BibTeX RDF |
|
| 32 | Andreas Lochbihler, Ognjen Maric |
Authenticated Data Structures as Functors in Isabelle/HOL. |
FMBC@CAV |
2020 |
DBLP DOI BibTeX RDF |
|
| 32 | Maria Ribeiro, Pedro Adão, Paulo Mateus |
Formal Verification of Ethereum Smart Contracts Using Isabelle/HOL. |
Logic, Language, and Security |
2020 |
DBLP DOI BibTeX RDF |
|
| 32 | Paulo Emílio de Vilhena, Lawrence C. Paulson |
Algebraically Closed Fields in Isabelle/HOL. |
IJCAR (2) |
2020 |
DBLP DOI BibTeX RDF |
|
| 32 | Walter Guttmann |
Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL. |
IJCAR (2) |
2020 |
DBLP DOI BibTeX RDF |
|
| 32 | Sohaib Soualah, Yousra Hafidi, Mohamed Khalgui, Allaoua Chaoui, Laïd Kahloul |
Efficient Verification of Reconfigurable Discrete-Event System Using Isabelle/HOL Theorem Prover and Hadoop. |
ICSOFT (Selected Papers) |
2020 |
DBLP DOI BibTeX RDF |
|
| 32 | Sohaib Soualah, Yousra Hafidi, Mohamed Khalgui, Allaoua Chaoui, Laïd Kahloul |
Formalization and Verification of Reconfigurable Discrete-event System using Model Driven Engineering and Isabelle/HOL. |
ICSOFT |
2020 |
DBLP DOI BibTeX RDF |
|
| 32 | Fabian Immler, Yong Kiam Tan |
The Poincaré-Bendixson theorem in Isabelle/HOL. |
CPP |
2020 |
DBLP DOI BibTeX RDF |
|
| 32 | Ralph Bottesch, Max W. Haslbeck, Alban Reynaud, René Thiemann |
Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL. |
NFM |
2020 |
DBLP DOI BibTeX RDF |
|
| 32 | Yutaka Nagashima |
Smart Induction for Isabelle/HOL (Tool Paper). |
FMCAD |
2020 |
DBLP DOI BibTeX RDF |
|
| 32 | Jonathan Julián Huerta y Munive |
Affine Systems of ODEs in Isabelle/HOL for Hybrid-Program Verification. |
SEFM |
2020 |
DBLP DOI BibTeX RDF |
|
| 32 | Laura Kovács, Hanna Lachnitt, Stefan Szeider |
Formalizing Graph Trail Properties in Isabelle/HOL. |
CICM |
2020 |
DBLP DOI BibTeX RDF |
|
| 32 | Yutaka Nagashima |
Simple Dataset for Proof Method Recommendation in Isabelle/HOL. |
CICM |
2020 |
DBLP DOI BibTeX RDF |
|
| 32 | Mathias Fleury |
Formalization of logical calculi in Isabelle/HOL. |
|
2020 |
RDF |
|
| 32 | Jonathan Julián Huerta y Munive |
Algebraic verification of hybrid systems in Isabelle/HOL |
|
2020 |
RDF |
|
| 32 | Wilayat Khan, David Sanán, Zhe Hou, Yang Liu 0003 |
On embedding a hardware description language in Isabelle/HOL. |
Des. Autom. Embed. Syst. |
2019 |
DBLP DOI BibTeX RDF |
|
| 32 | Lars Hupel |
Certifying Dictionary Construction in Isabelle/HOL. |
Fundam. Informaticae |
2019 |
DBLP DOI BibTeX RDF |
|
Displaying result #101 - #200 of 460 (100 per page; Change: ) Pages: [ <<][ 1][ 2][ 3][ 4][ 5][ >>] |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license