The FacetedDBLP logo    Search for: in:

Disable automatic phrases ?     Syntactic query expansion: ?

Searching for phrase isabelle/hol (changed automatically) with no syntactic query expansion in all metadata.

Publication years (Num. hits)
1994-1998 (15) 1999-2000 (17) 2001-2002 (24) 2003-2004 (32) 2005 (18) 2006 (23) 2007 (21) 2008 (24) 2009 (27) 2010-2011 (17) 2012-2014 (22) 2015 (15) 2016-2017 (26) 2018 (25) 2019 (30) 2020 (31) 2021 (32) 2022 (25) 2023 (30) 2024 (6)
Publication types (Num. hits)
article(138) book(2) incollection(3) inproceedings(307) phdthesis(10)
Venues (Conferences, Journals, ...)
CoRR(54) TPHOLs(43) J. Autom. Reason.(29) Arch. Formal Proofs(24) ITP(24) CPP(17) CADE(10) CICM(9) IJCAR(7) SEFM(7) TYPES(7) Formal Aspects Comput.(6) APLAS(4) CSF(4) ESOP(4) FM(4) More (+10 of total 158)
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
186Steven Obua, Sebastian Skalberg Importing HOL into Isabelle/HOL. Search on Bibsonomy IJCAR The full citation details ... 2006 DBLP  DOI  BibTeX  RDF
128Sean McLaughlin An Interpretation of Isabelle/HOL in HOL Light. Search on Bibsonomy IJCAR The full citation details ... 2006 DBLP  DOI  BibTeX  RDF
103Graeme Smith 0001, Florian Kammüller, Thomas Santen Encoding Object-Z in Isabelle/HOL. Search on Bibsonomy ZB The full citation details ... 2002 DBLP  DOI  BibTeX  RDF reference semantics, Object-Z, higher-order logic, Isabelle
93Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow The Isabelle Framework. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
92Alexander Schimpf, Stephan Merz, Jan-Georg Smaus Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
92Florian Kammüller, Jeff W. Sanders Idempotent Relations in Isabelle/HOL. Search on Bibsonomy ICTAC The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
91Markus Kaiser 0002, Ralf Lämmel An Isabelle/HOL-based model of stratego-like traversal strategies. Search on Bibsonomy PPDP The full citation details ... 2009 DBLP  DOI  BibTeX  RDF generic functional programming, traversal strategies, domain specific languages, rewriting, isabelle/hol, software transformation, stratego
83Haykal Tej, Burkhart Wolff A Corrected Failure Divergence Model for CSP in Isabelle/HOL. Search on Bibsonomy FME The full citation details ... 1997 DBLP  DOI  BibTeX  RDF
82Thomas Santen A Theory of Structured Model-Based Specifications in Isabelle/HOL. Search on Bibsonomy TPHOLs The full citation details ... 1997 DBLP  DOI  BibTeX  RDF
80Sabine Glesner, Jan Olaf Blech Coalgebraic Semantics for Component Systems. Search on Bibsonomy Architecting Systems with Trustworthy Components The full citation details ... 2004 DBLP  DOI  BibTeX  RDF verification, semantics, Components, Isabelle/HOL, coinduction, component interaction
80David von Oheimb, Tobias Nipkow Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited. Search on Bibsonomy FME The full citation details ... 2002 DBLP  DOI  BibTeX  RDF Java, Hoare logic, side effects, dynamic binding, Isabelle/HOL, auxiliary variables
80David von Oheimb Hoare Logic for Mutual Recursion and Local Variables. Search on Bibsonomy FSTTCS The full citation details ... 1999 DBLP  DOI  BibTeX  RDF axiomaticsemantics, relative completeness, local variables, call-by-value parameters, soundness, Hoare logic, Isabelle/HOL, mutual recursion
79Achim D. Brucker, Burkhart Wolff Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing. Search on Bibsonomy TAP The full citation details ... 2007 DBLP  DOI  BibTeX  RDF symbolic test case generations, theorem proving, computer security, black box testing, Isabelle/HOL, test sequence generation
73Yue Tang, Jin Song Dong, Jing Sun 0002, Brendan P. Mahony Reasoning about Semantic Web in Isabelle/HOL. Search on Bibsonomy APSEC The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
72Jan Olaf Blech, Lars Gesellensetter, Sabine Glesner Formal Verification of Dead Code Elimination in Isabelle/HOL. Search on Bibsonomy SEFM The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
72Stefan Berghofer Extracting a Normalization Algorithm in Isabelle/HOL. Search on Bibsonomy TYPES The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
72Christine Röckl, Daniel Hirschkoff, Stefan Berghofer Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the pi-Calculus and Mechanizing the Theory of Contexts. Search on Bibsonomy FoSSaCS The full citation details ... 2001 DBLP  DOI  BibTeX  RDF
72Cornelia Pusch Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL. Search on Bibsonomy TACAS The full citation details ... 1999 DBLP  DOI  BibTeX  RDF
64Albert Rizaldi Formal specification, monitoring, and verification of autonomous vehicles in Isabelle/HOL (Formale Spezifikation, Erfüllbarkeitsanalyse, und formale Verifikation von autonomen Fahrzeugen in Isabelle/HOL) (PDF / PS) Search on Bibsonomy 2020   RDF
63Andreas Lochbihler Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
63Steven Obua Proving Bounds for Real Linear Programs in Isabelle/HOL. Search on Bibsonomy TPHOLs The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
63Simon J. Gay A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL. Search on Bibsonomy TPHOLs The full citation details ... 2001 DBLP  DOI  BibTeX  RDF semantics, Types, pi calculus, automatic theorem proving
63Leonor Prensa Nieto, Javier Esparza Verifying Single and Multi-mutator Garbage Collectors with Owicki-Gries in Isabelle/HOL. Search on Bibsonomy MFCS The full citation details ... 2000 DBLP  DOI  BibTeX  RDF
63Pierre Chartier Formalisation of B in Isabelle/HOL. Search on Bibsonomy B The full citation details ... 1998 DBLP  DOI  BibTeX  RDF
63Tobias Nipkow More Church-Rosser Proofs (in Isabelle/HOL). Search on Bibsonomy CADE The full citation details ... 1996 DBLP  DOI  BibTeX  RDF
62Damián Barsotti, Leonor Prensa Nieto, Alwen Tiu Verification of clock synchronization algorithms: experiments on a combination of deductive tools. Search on Bibsonomy Formal Aspects Comput. The full citation details ... 2007 DBLP  DOI  BibTeX  RDF Combination of deductive tools, Verification, Theorem proving, Clock synchronization
62Christian Urban Nominal Techniques in Isabelle/HOL. Search on Bibsonomy J. Autom. Reason. The full citation details ... 2008 DBLP  DOI  BibTeX  RDF Nominal logic work, Lambda-calculus, Theorem provers
62Jacques D. Fleuriot On the Mechanization of Real Analysis in Isabelle/HOL. Search on Bibsonomy TPHOLs The full citation details ... 2000 DBLP  DOI  BibTeX  RDF
60Dirk Leinenbach, Wolfgang J. Paul, Elena Petrova Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes. Search on Bibsonomy SEFM The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
60Matthias Daum 0001, Jan Dörrenbächer, Burkhart Wolff Proving Fairness and Implementation Correctness of a Microkernel Scheduler. Search on Bibsonomy J. Autom. Reason. The full citation details ... 2009 DBLP  DOI  BibTeX  RDF Formal verification, Interactive theorem proving, Microkernel, Isabelle/HOL
60Gerwin Klein, Philip Derrin, Kevin Elphinstone Experience report: seL4: formally verifying a high-performance microkernel. Search on Bibsonomy ICFP The full citation details ... 2009 DBLP  DOI  BibTeX  RDF seL4, haskell, microkernel, Isabelle/HOL
60Nik Sultana, Simon J. Thompson Mechanical verification of refactorings. Search on Bibsonomy PEPM The full citation details ... 2008 DBLP  DOI  BibTeX  RDF refactoring, Isabelle/HOL
60Sabine Glesner Finite Integer Computations: An Algebraic Foundation for Their Correctness. Search on Bibsonomy Formal Aspects Comput. The full citation details ... 2006 DBLP  DOI  BibTeX  RDF Additional Keywords finite integer and residue class arithmetic, changing representation sizes, Java Card bytecode optimization, constant folding, Java and C arithmetic, formal verification, inconsistency, Java Card, Isabelle/HOL
60David von Oheimb, Volkmar Lotz, Georg Walter Analyzing SLE 88 memory management security using Interacting State Machines. Search on Bibsonomy Int. J. Inf. Sec. The full citation details ... 2005 DBLP  DOI  BibTeX  RDF Security, Smart cards, Memory management, Formal analysis, Isabelle/HOL
60S. J. Ambler, Roy L. Crole, Alberto Momigliano A definitional approach to primitivexs recursion over higher order abstract syntax. Search on Bibsonomy MERLIN The full citation details ... 2003 DBLP  DOI  BibTeX  RDF Isabelle HOL, topos theory, ?-calculus, higher order abstract syntax, primitive recursion, initial algebras
60Lawrence C. Paulson Mechanized proofs for a recursive authentication protocol. Search on Bibsonomy CSFW The full citation details ... 1997 DBLP  DOI  BibTeX  RDF mechanized proofs, recursive authentication protocol, inductive approach, message nesting, basic security theorem, adjacent pairs, honest agents, protocol complexity, agents, protocols, specification, symmetry, mutual authentication, Isabelle/HOL, session keys
59Morten P. Lindegaard, Anne E. Haxthausen Proof Support for RAISE by a Reuse Approach Based on Institutions. Search on Bibsonomy AMAST The full citation details ... 2004 DBLP  DOI  BibTeX  RDF proof support, Institutions, algebraic semantics, HOL, RSL
52Jinshuang Wang, Huabing Yang, Xingyuan Zhang Liveness Reasoning with Isabelle/HOL. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF Liveness Proof, Inductive Protocol Verification, Parametric Fairness, Probabilistic Model
52Lukas Bulwahn, Alexander Krauss 0001, Florian Haftmann, Levent Erkök, John Matthews Imperative Functional Programming with Isabelle/HOL. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
52Daniel Wasserrab, Andreas Lochbihler Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
52William Billingsley, Peter Robinson 0001 Student Proof Exercises Using MathsTiles and Isabelle/HOL in an Intelligent Book. Search on Bibsonomy J. Autom. Reason. The full citation details ... 2007 DBLP  DOI  BibTeX  RDF Intelligent book, MathsTiles, Isabelle
52Christian Urban, Stefan Berghofer A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. Search on Bibsonomy IJCAR The full citation details ... 2006 DBLP  DOI  BibTeX  RDF Lambda-calculus, proof assistants, nominal logic, primitive recursion
52Christian Urban, Christine Tasson Nominal Techniques in Isabelle/HOL. Search on Bibsonomy CADE The full citation details ... 2005 DBLP  DOI  BibTeX  RDF theorem-assistants, Lambda-calculus, nominal logic, structural induction
52Norbert Schirmer A Verification Environment for Sequential Imperative Programs in Isabelle/HOL. Search on Bibsonomy LPAR The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
52Baris Sertkaya, Halit Oguztüzün Proof of the Basic Theorem on Concept Lattices in Isabelle/HOL. Search on Bibsonomy ISCIS The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
52Jeremy Avigad, Kevin Donnelly Formalizing O Notation in Isabelle/HOL. Search on Bibsonomy IJCAR The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
52Leonor Prensa Nieto The Rely-Guarantee Method in Isabelle/HOL. Search on Bibsonomy ESOP The full citation details ... 2003 DBLP  DOI  BibTeX  RDF
52Yasuhiko Minamide, Koji Okuma Verifying CPS transformations in Isabelle/HOL. Search on Bibsonomy MERLIN The full citation details ... 2003 DBLP  DOI  BibTeX  RDF program transformation, theorem proving, correctness proofs
52David Hemer, Ian J. Hayes, Paul A. Strooper Refinement Calculus for Logic Programming in Isabelle/HOL. Search on Bibsonomy TPHOLs The full citation details ... 2001 DBLP  DOI  BibTeX  RDF
52Stephan Merz Weak Alternating Automata in Isabelle/HOL. Search on Bibsonomy TPHOLs The full citation details ... 2000 DBLP  DOI  BibTeX  RDF
51Markus Wenzel 0001, Lawrence C. Paulson Isabelle/Isar. Search on Bibsonomy The Seventeen Provers of the World The full citation details ... 2006 DBLP  DOI  BibTeX  RDF
51Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Fernanto Tiu Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants. Search on Bibsonomy TACAS The full citation details ... 2006 DBLP  DOI  BibTeX  RDF
51Steffen Helke, Florian Kammüller Structure Preserving Data Abstractions for Statecharts. Search on Bibsonomy FORTE The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
50Martin Wildmoser, Tobias Nipkow Certifying Machine Code Safety: Shallow Versus Deep Embedding. Search on Bibsonomy TPHOLs The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
48Hao Xu, Yongwang Zhao Isabelle/Cloud: Delivering Isabelle/HOL as a Cloud IDE for Theorem Proving. Search on Bibsonomy Internetware The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
48Achim D. Brucker Nano JSON: Working with JSON formatted data in Isabelle/HOL and Isabelle/ML. Search on Bibsonomy Arch. Formal Proofs The full citation details ... 2022 DBLP  BibTeX  RDF
48Diego Marmsoler, Achim D. Brucker Isabelle/Solidity: A deep Embedding of Solidity in Isabelle/HOL. Search on Bibsonomy Arch. Formal Proofs The full citation details ... 2022 DBLP  BibTeX  RDF
47Xavier Parent, Christoph Benzmüller Conditional normative reasoning as a fragment of HOL (Isabelle/HOL dataset). Search on Bibsonomy Arch. Formal Proofs The full citation details ... 2024 DBLP  BibTeX  RDF
47Ondrej Kuncar, Andrei Popescu 0001 Safety and conservativity of definitions in HOL and Isabelle/HOL. Search on Bibsonomy Proc. ACM Program. Lang. The full citation details ... 2018 DBLP  DOI  BibTeX  RDF
47Dina Taiwé Kolyang HOL-Z, an integrated formal support environment for Z in Isabelle/HOL. Search on Bibsonomy 1999   RDF
41René Thiemann, Christian Sternagel Certification of Termination Proofs Using CeTA. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
41Stefan Berghofer Program Extraction in Simply-Typed Higher Order Logic. Search on Bibsonomy TYPES The full citation details ... 2002 DBLP  DOI  BibTeX  RDF
40Javier de Dios, Ricardo Peña-Marí Formal Certification of a Resource-Aware Language Implementation. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF memory management, functional languages, compiler verification
40Jeremy E. Dawson, Alwen Tiu Formalising Observer Theory for Environment-Sensitive Bisimulation. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
40Rafal Kolanski, Gerwin Klein Types, Maps and Separation Logic. Search on Bibsonomy TPHOLs The full citation details ... 2009 DBLP  DOI  BibTeX  RDF
40Rok Strnisa, Peter Sewell, Matthew J. Parkinson The java module system: core design and semantic definition. Search on Bibsonomy OOPSLA The full citation details ... 2007 DBLP  DOI  BibTeX  RDF LJAM, superpackage, java, module, JAM
40Christoph Sprenger 0001, David A. Basin A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols. Search on Bibsonomy TPHOLs The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
40Tom Ridge, James Margetson A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic. Search on Bibsonomy TPHOLs The full citation details ... 2005 DBLP  DOI  BibTeX  RDF
40Michael Drouineaud, Maksym Bortin, Paolo Torrini, Karsten Sohr A First Step Towards Formal Verification of Security Policy Properties for RBAC. Search on Bibsonomy QSIC The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
40Jeremy E. Dawson, Rajeev Goré Formalised Cut Admissibility for Display Logic. Search on Bibsonomy TPHOLs The full citation details ... 2002 DBLP  DOI  BibTeX  RDF
40Christine Röckl, Javier Esparza Proof-Checking Protocols Using Bisimulations. Search on Bibsonomy CONCUR The full citation details ... 1999 DBLP  DOI  BibTeX  RDF
40Andrei Popescu 0001, Elsa L. Gunter, Christopher J. Osborn Strong Normalization for System F by HOAS on Top of FOAS. Search on Bibsonomy LICS The full citation details ... 2010 DBLP  DOI  BibTeX  RDF Higher-Order Abstract Syntax, Isabelle/HOL, System F
40Patrick Schaller, Benedikt Schmidt 0002, David A. Basin, Srdjan Capkun Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks. Search on Bibsonomy CSF The full citation details ... 2009 DBLP  DOI  BibTeX  RDF Wireless Network Protocols, Security Protocols, Isabelle/HOL, Formal Security Model
40Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood seL4: formal verification of an OS kernel. Search on Bibsonomy SOSP The full citation details ... 2009 DBLP  DOI  BibTeX  RDF l4, sel4, microkernel, isabelle/hol
40Philip Derrin, Kevin Elphinstone, Gerwin Klein, David A. Cock, Manuel M. T. Chakravarty Running the manual: an approach to high-assurance microkernel development. Search on Bibsonomy Haskell The full citation details ... 2006 DBLP  DOI  BibTeX  RDF formalisation, verification, operating systems, rapid prototyping, Haskell, monads, executable specification, Isabelle/HOL
39Achim D. Brucker, Burkhart Wolff hol-TestGen. Search on Bibsonomy FASE The full citation details ... 2009 DBLP  DOI  BibTeX  RDF symbolic test-case generations, theorem proving, black box testing, white box testing, interactive testing
39Ludovic Henrio, Florian Kammüller A Mechanized Model of the Theory of Objects. Search on Bibsonomy FMOODS The full citation details ... 2007 DBLP  DOI  BibTeX  RDF
39Achim D. Brucker, Burkhart Wolff Interactive Testing with HOL-TestGen. Search on Bibsonomy FATES The full citation details ... 2005 DBLP  DOI  BibTeX  RDF symbolic test case generations, theorem proving, black box testing, white box testing, interactive testing
39Thomas Santen Isomorphisms - A Link Between the Shallow and the Deep. Search on Bibsonomy TPHOLs The full citation details ... 1999 DBLP  DOI  BibTeX  RDF
32Jonathan Julián Huerta y Munive, Simon Foster 0001, Mario Gleirscher, Georg Struth, Christian Pardillo Laursen, Thomas Hickman Scalable Automated Verification for Cyber-Physical Systems in Isabelle/HOL. Search on Bibsonomy CoRR The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
32Julian Parsert Linear Programming in Isabelle/HOL. Search on Bibsonomy CoRR The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
32Mnacho Echenim, Mehdi Mhalla A Formalization of the CHSH Inequality and Tsirelson's Upper-bound in Isabelle/HOL. Search on Bibsonomy J. Autom. Reason. The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
32Hanna Lachnitt, Mathias Fleury, Leni Aniva, Andrew Reynolds 0001, Haniel Barbosa, Andres Nötzli, Clark W. Barrett, Cesare Tinelli IsaRare: Automatic Verification of SMT Rewrites in Isabelle/HOL. Search on Bibsonomy TACAS (1) The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
32Sohaib Soualah, Mohamed Khalgui, Allaoua Chaoui Effective Parallel Formal Verification of Reconfigurable Discrete-Event Systems Formalizing with Isabelle/HOL. Search on Bibsonomy AINA (2) The full citation details ... 2024 DBLP  DOI  BibTeX  RDF
32Andreas V. Hess, Sebastian Alexander Mödersheim, Achim D. Brucker Stateful Protocol Composition in Isabelle/HOL. Search on Bibsonomy ACM Trans. Priv. Secur. The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
32Jonas Bayer, Aleksey Gonus, Christoph Benzmüller, Dana S. Scott Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation. Search on Bibsonomy CoRR The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
32Ata Keskin A Formalization of Martingales in Isabelle/HOL. Search on Bibsonomy CoRR The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
32Chelsea Edmonds, Lawrence C. Paulson Formal Probabilistic Methods for Combinatorial Structures in Isabelle/HOL. Search on Bibsonomy CoRR The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
32Leo Freitas Topologically sorting VDM-SL definitions for Isabelle/HOL translation. Search on Bibsonomy CoRR The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
32Simon Foster 0001, Burkhart Wolff Automated Reasoning for Physical Quantities, Units, and Measurements in Isabelle/HOL. Search on Bibsonomy CoRR The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
32Terru Stübinger, Lars Hupel Extending Isabelle/HOL's Code Generator with support for the Go programming language. Search on Bibsonomy CoRR The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
32Stepán Starosta Infinite Words and Morphic Languages Formalized in Isabelle/HOL. Search on Bibsonomy CoRR The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
32Leo Freitas, Peter Gorm Larsen VDM recursive functions in Isabelle/HOL. Search on Bibsonomy CoRR The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
32Mnacho Echenim, Mehdi Mhalla A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL. Search on Bibsonomy CoRR The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
32Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL. Search on Bibsonomy J. Autom. Reason. The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
32Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot Correction: Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL. Search on Bibsonomy J. Autom. Reason. The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
32Asta Halkjær From, Anders Schlichtkrull, Jørgen Villadsen A sequent calculus for first-order logic formalized in Isabelle/HOL. Search on Bibsonomy J. Log. Comput. The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
32Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato 0001 Program logic for higher-order probabilistic programs in Isabelle/HOL. Search on Bibsonomy Sci. Comput. Program. The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
32Pasquale Noce Formal Verification of Cryptographic Protocols with Isabelle/HOL. Search on Bibsonomy Handb. Formal Anal. Verification Cryptogr. The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
32Achim D. Brucker, Amy Stell Verifying Feedforward Neural Networks for Classification in Isabelle/HOL. Search on Bibsonomy FM The full citation details ... 2023 DBLP  DOI  BibTeX  RDF
Displaying result #1 - #100 of 460 (100 per page; Change: )
Pages: [1][2][3][4][5][>>]
Valid XHTML 1.1! Valid CSS! [Valid RSS]
Maintained by L3S.
Previously maintained by Jörg Diederich.
Based upon DBLP by Michael Ley.
open data data released under the ODC-BY 1.0 license