|
|
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 |
186 | Steven Obua, Sebastian Skalberg |
Importing HOL into Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, pp. 298-302, 2006, Springer, 3-540-37187-7. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
128 | Sean McLaughlin |
An Interpretation of Isabelle/HOL in HOL Light. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, pp. 192-204, 2006, Springer, 3-540-37187-7. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
103 | Graeme Smith 0001, Florian Kammüller, Thomas Santen |
Encoding Object-Z in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ZB ![In: ZB 2002: Formal Specification and Development in Z and B, 2nd International Conference of B and Z Users, Grenoble, France, January 23-25, 2002, Proceedings, pp. 82-99, 2002, Springer, 3-540-43166-7. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
reference semantics, Object-Z, higher-order logic, Isabelle |
93 | Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow |
The Isabelle Framework. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, pp. 33-38, 2008, Springer, 978-3-540-71065-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
92 | Alexander Schimpf, Stephan Merz, Jan-Georg Smaus |
Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 424-439, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
92 | Florian Kammüller, Jeff W. Sanders |
Idempotent Relations in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICTAC ![In: Theoretical Aspects of Computing - ICTAC 2004, First International Colloquium, Guiyang, China, September 20-24, 2004, Revised Selected Papers, pp. 310-324, 2004, Springer, 3-540-25304-1. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
91 | Markus Kaiser 0002, Ralf Lämmel |
An Isabelle/HOL-based model of stratego-like traversal strategies. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PPDP ![In: Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal, pp. 93-104, 2009, ACM, 978-1-60558-568-0. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
generic functional programming, traversal strategies, domain specific languages, rewriting, isabelle/hol, software transformation, stratego |
83 | Haykal Tej, Burkhart Wolff |
A Corrected Failure Divergence Model for CSP in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FME ![In: FME '97: Industrial Applications and Strengthened Foundations of Formal Methods, 4th International Symposium of Formal Methods Europe, Graz, Austria, September 15-19, 1997, Proceedings, pp. 318-337, 1997, Springer, 3-540-63533-5. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
82 | Thomas Santen |
A Theory of Structured Model-Based Specifications in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings, pp. 243-258, 1997, Springer, 3-540-63379-0. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
80 | Sabine Glesner, Jan Olaf Blech |
Coalgebraic Semantics for Component Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Architecting Systems with Trustworthy Components ![In: Architecting Systems with Trustworthy Components, International Seminar, Dagstuhl Castle, Germany, December 12-17, 2004. Revised Selected Papers, pp. 245-261, 2004, Springer, 3-540-35800-5. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
verification, semantics, Components, Isabelle/HOL, coinduction, component interaction |
80 | David von Oheimb, Tobias Nipkow |
Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FME ![In: FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002, Proceedings, pp. 89-105, 2002, Springer, 3-540-43928-5. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
Java, Hoare logic, side effects, dynamic binding, Isabelle/HOL, auxiliary variables |
80 | David von Oheimb |
Hoare Logic for Mutual Recursion and Local Variables. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FSTTCS ![In: Foundations of Software Technology and Theoretical Computer Science, 19th Conference, Chennai, India, December 13-15, 1999, Proceedings, pp. 168-180, 1999, Springer, 3-540-66836-5. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
axiomaticsemantics, relative completeness, local variables, call-by-value parameters, soundness, Hoare logic, Isabelle/HOL, mutual recursion |
79 | Achim D. Brucker, Burkhart Wolff |
Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TAP ![In: Tests and Proofs - 1st International Conference, TAP 2007, Zurich, Switzerland, February 12-13, 2007. Revised Papers, pp. 149-168, 2007, Springer, 978-3-540-73769-8. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
symbolic test case generations, theorem proving, computer security, black box testing, Isabelle/HOL, test sequence generation |
73 | Yue Tang, Jin Song Dong, Jing Sun 0002, Brendan P. Mahony |
Reasoning about Semantic Web in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
APSEC ![In: 11th Asia-Pacific Software Engineering Conference (APSEC 2004), 30 November - 3 December 2004, Busan, Korea, pp. 46-53, 2004, IEEE Computer Society, 0-7695-2245-9. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
72 | Jan Olaf Blech, Lars Gesellensetter, Sabine Glesner |
Formal Verification of Dead Code Elimination in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SEFM ![In: Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 7-9 September 2005, Koblenz, Germany, pp. 200-209, 2005, IEEE Computer Society, 0-7695-2435-4. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
72 | Stefan Berghofer |
Extracting a Normalization Algorithm in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers, pp. 50-65, 2004, Springer, 3-540-31428-8. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
72 | Christine 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](Pics/bibsonomy.png) |
FoSSaCS ![In: Foundations of Software Science and Computation Structures, 4th International Conference, FOSSACS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings, pp. 364-378, 2001, Springer, 3-540-41864-4. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
72 | Cornelia Pusch |
Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TACAS ![In: Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS '99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings, pp. 89-103, 1999, Springer, 3-540-65703-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
64 | Albert 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](Pics/bibsonomy.png) |
|
2020 |
RDF |
|
63 | Andreas Lochbihler |
Formalising FinFuns - Generating Code for Functions as Data from Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 310-326, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
63 | Steven Obua |
Proving Bounds for Real Linear Programs in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, pp. 227-244, 2005, Springer, 3-540-28372-2. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
63 | Simon J. Gay |
A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings, pp. 217-232, 2001, Springer, 3-540-42525-X. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
semantics, Types, pi calculus, automatic theorem proving |
63 | Leonor Prensa Nieto, Javier Esparza |
Verifying Single and Multi-mutator Garbage Collectors with Owicki-Gries in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MFCS ![In: Mathematical Foundations of Computer Science 2000, 25th International Symposium, MFCS 2000, Bratislava, Slovakia, August 28 - September 1, 2000, Proceedings, pp. 619-628, 2000, Springer, 3-540-67901-4. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
63 | Pierre Chartier |
Formalisation of B in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
B ![In: B'98: Recent Advances in the Development and Use of the B Method, Second International B Conference, Montpellier, France, April 22-24, 1998, Proceedings, pp. 66-82, 1998, Springer, 3-540-64405-9. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
63 | Tobias Nipkow |
More Church-Rosser Proofs (in Isabelle/HOL). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30 - August 3, 1996, Proceedings, pp. 733-747, 1996, Springer, 3-540-61511-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
62 | Damián Barsotti, Leonor Prensa Nieto, Alwen Tiu |
Verification of clock synchronization algorithms: experiments on a combination of deductive tools. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 19(3), pp. 321-341, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Combination of deductive tools, Verification, Theorem proving, Clock synchronization |
62 | Christian Urban |
Nominal Techniques in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 40(4), pp. 327-356, 2008. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
Nominal logic work, Lambda-calculus, Theorem provers |
62 | Jacques D. Fleuriot |
On the Mechanization of Real Analysis in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings, pp. 145-161, 2000, Springer, 3-540-67863-8. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
60 | Dirk Leinenbach, Wolfgang J. Paul, Elena Petrova |
Towards the Formal Verification of a C0 Compiler: Code Generation and Implementation Correctnes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SEFM ![In: Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 7-9 September 2005, Koblenz, Germany, pp. 2-12, 2005, IEEE Computer Society, 0-7695-2435-4. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
60 | Matthias Daum 0001, Jan Dörrenbächer, Burkhart Wolff |
Proving Fairness and Implementation Correctness of a Microkernel Scheduler. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 42(2-4), pp. 349-388, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Formal verification, Interactive theorem proving, Microkernel, Isabelle/HOL |
60 | Gerwin Klein, Philip Derrin, Kevin Elphinstone |
Experience report: seL4: formally verifying a high-performance microkernel. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceeding of the 14th ACM SIGPLAN international conference on Functional programming, ICFP 2009, Edinburgh, Scotland, UK, August 31 - September 2, 2009, pp. 91-96, 2009, ACM, 978-1-60558-332-7. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
seL4, haskell, microkernel, Isabelle/HOL |
60 | Nik Sultana, Simon J. Thompson |
Mechanical verification of refactorings. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PEPM ![In: Proceedings of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, PEPM 2008, San Francisco, California, USA, January 7-8, 2008, pp. 51-60, 2008, ACM, 978-1-59593-977-7. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
refactoring, Isabelle/HOL |
60 | Sabine Glesner |
Finite Integer Computations: An Algebraic Foundation for Their Correctness. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 18(2), pp. 244-262, 2006. The full citation details ...](Pics/full.jpeg) |
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 |
60 | David von Oheimb, Volkmar Lotz, Georg Walter |
Analyzing SLE 88 memory management security using Interacting State Machines. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Int. J. Inf. Sec. ![In: Int. J. Inf. Sec. 4(3), pp. 155-171, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
Security, Smart cards, Memory management, Formal analysis, Isabelle/HOL |
60 | S. J. Ambler, Roy L. Crole, Alberto Momigliano |
A definitional approach to primitivexs recursion over higher order abstract syntax. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003, ACM, 978-1-58113-800-9. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
Isabelle HOL, topos theory, ?-calculus, higher order abstract syntax, primitive recursion, initial algebras |
60 | Lawrence C. Paulson |
Mechanized proofs for a recursive authentication protocol. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSFW ![In: 10th Computer Security Foundations Workshop (CSFW '97), June 10-12, 1997, Rockport, Massachusetts, USA, pp. 84-95, 1997, IEEE Computer Society, 0-8186-7990-5. The full citation details ...](Pics/full.jpeg) |
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 |
59 | Morten P. Lindegaard, Anne E. Haxthausen |
Proof Support for RAISE by a Reuse Approach Based on Institutions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AMAST ![In: Algebraic Methodology and Software Technology, 10th International Conference, AMAST 2004, Stirling, Scotland, UK, July 12-16, 2004, Proceedings, pp. 319-333, 2004, Springer, 3-540-22381-9. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
proof support, Institutions, algebraic semantics, HOL, RSL |
52 | Jinshuang Wang, Huabing Yang, Xingyuan Zhang |
Liveness Reasoning with Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 485-499, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Liveness Proof, Inductive Protocol Verification, Parametric Fairness, Probabilistic Model |
52 | Lukas Bulwahn, Alexander Krauss 0001, Florian Haftmann, Levent Erkök, John Matthews |
Imperative Functional Programming with Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, pp. 134-149, 2008, Springer, 978-3-540-71065-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
52 | Daniel Wasserrab, Andreas Lochbihler |
Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, pp. 294-309, 2008, Springer, 978-3-540-71065-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
52 | William Billingsley, Peter Robinson 0001 |
Student Proof Exercises Using MathsTiles and Isabelle/HOL in an Intelligent Book. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 39(2), pp. 181-218, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
Intelligent book, MathsTiles, Isabelle |
52 | Christian Urban, Stefan Berghofer |
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, pp. 498-512, 2006, Springer, 3-540-37187-7. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
Lambda-calculus, proof assistants, nominal logic, primitive recursion |
52 | Christian Urban, Christine Tasson |
Nominal Techniques in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings, pp. 38-53, 2005, Springer, 3-540-28005-7. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
theorem-assistants, Lambda-calculus, nominal logic, structural induction |
52 | Norbert Schirmer |
A Verification Environment for Sequential Imperative Programs in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings, pp. 398-414, 2004, Springer, 3-540-25236-3. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
52 | Baris Sertkaya, Halit Oguztüzün |
Proof of the Basic Theorem on Concept Lattices in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISCIS ![In: Computer and Information Sciences - ISCIS 2004, 19th International Symposium, Kemer-Antalya, Turkey, October 27-29, 2004. Proceedings, pp. 976-985, 2004, Springer, 3-540-23526-4. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
52 | Jeremy Avigad, Kevin Donnelly |
Formalizing O Notation in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning - Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings, pp. 357-371, 2004, Springer, 3-540-22345-2. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
52 | Leonor Prensa Nieto |
The Rely-Guarantee Method in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ESOP ![In: Programming Languages and Systems, 12th European Symposium on Programming, ESOP 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, pp. 348-362, 2003, Springer, 3-540-00886-1. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
52 | Yasuhiko Minamide, Koji Okuma |
Verifying CPS transformations in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003, ACM, 978-1-58113-800-9. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
program transformation, theorem proving, correctness proofs |
52 | David Hemer, Ian J. Hayes, Paul A. Strooper |
Refinement Calculus for Logic Programming in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings, pp. 249-264, 2001, Springer, 3-540-42525-X. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
52 | Stephan Merz |
Weak Alternating Automata in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings, pp. 424-441, 2000, Springer, 3-540-67863-8. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
51 | Markus Wenzel 0001, Lawrence C. Paulson |
Isabelle/Isar. ![Search on Bibsonomy](Pics/bibsonomy.png) |
The Seventeen Provers of the World ![In: The Seventeen Provers of the World, Foreword by Dana S. Scott, pp. 41-49, 2006, Springer, 3-540-30704-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
51 | Pascal 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](Pics/bibsonomy.png) |
TACAS ![In: Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006, Proceedings, pp. 167-181, 2006, Springer, 3-540-33056-9. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
51 | Steffen Helke, Florian Kammüller |
Structure Preserving Data Abstractions for Statecharts. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FORTE ![In: Formal Techniques for Networked and Distributed Systems - FORTE 2005, 25th IFIP WG 6.1 International Conference, Taipei, Taiwan, October 2-5, 2005, Proceedings, pp. 305-319, 2005, Springer, 3-540-29189-X. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
50 | Martin Wildmoser, Tobias Nipkow |
Certifying Machine Code Safety: Shallow Versus Deep Embedding. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings, pp. 305-320, 2004, Springer, 3-540-23017-3. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
48 | Hao Xu, Yongwang Zhao |
Isabelle/Cloud: Delivering Isabelle/HOL as a Cloud IDE for Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Internetware ![In: Proceedings of the 14th Asia-Pacific Symposium on Internetware, Internetware 2023, Hangzhou, China, August 4-6, 2023, pp. 313-322, 2023, ACM. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
48 | Achim D. Brucker |
Nano JSON: Working with JSON formatted data in Isabelle/HOL and Isabelle/ML. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2022, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP BibTeX RDF |
|
48 | Diego Marmsoler, Achim D. Brucker |
Isabelle/Solidity: A deep Embedding of Solidity in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2022, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP BibTeX RDF |
|
47 | Xavier Parent, Christoph Benzmüller |
Conditional normative reasoning as a fragment of HOL (Isabelle/HOL dataset). ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2024, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP BibTeX RDF |
|
47 | Ondrej Kuncar, Andrei Popescu 0001 |
Safety and conservativity of definitions in HOL and Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proc. ACM Program. Lang. ![In: Proc. ACM Program. Lang. 2(POPL), pp. 24:1-24:26, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
47 | Dina Taiwé Kolyang |
HOL-Z, an integrated formal support environment for Z in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
1999 |
RDF |
|
41 | René Thiemann, Christian Sternagel |
Certification of Termination Proofs Using CeTA. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 452-468, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
41 | Stefan Berghofer |
Program Extraction in Simply-Typed Higher Order Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers, pp. 21-38, 2002, Springer, 3-540-14031-X. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
40 | Javier de Dios, Ricardo Peña-Marí |
Formal Certification of a Resource-Aware Language Implementation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 196-211, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
memory management, functional languages, compiler verification |
40 | Jeremy E. Dawson, Alwen Tiu |
Formalising Observer Theory for Environment-Sensitive Bisimulation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 180-195, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
40 | Rafal Kolanski, Gerwin Klein |
Types, Maps and Separation Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, pp. 276-292, 2009, Springer, 978-3-642-03358-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
|
40 | Rok Strnisa, Peter Sewell, Matthew J. Parkinson |
The java module system: core design and semantic definition. ![Search on Bibsonomy](Pics/bibsonomy.png) |
OOPSLA ![In: Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007, October 21-25, 2007, Montreal, Quebec, Canada, pp. 499-514, 2007, ACM, 978-1-59593-786-5. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
LJAM, superpackage, java, module, JAM |
40 | Christoph Sprenger 0001, David A. Basin |
A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, pp. 302-318, 2007, Springer, 978-3-540-74590-7. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
40 | Tom Ridge, James Margetson |
A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, pp. 294-309, 2005, Springer, 3-540-28372-2. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
40 | Michael Drouineaud, Maksym Bortin, Paolo Torrini, Karsten Sohr |
A First Step Towards Formal Verification of Security Policy Properties for RBAC. ![Search on Bibsonomy](Pics/bibsonomy.png) |
QSIC ![In: 4th International Conference on Quality Software (QSIC 2004), 8-10 September 2004, Braunschweig, Germany, pp. 60-67, 2004, IEEE Computer Society, 0-7695-2207-6. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
40 | Jeremy E. Dawson, Rajeev Goré |
Formalised Cut Admissibility for Display Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings, pp. 131-147, 2002, Springer, 3-540-44039-9. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
40 | Christine Röckl, Javier Esparza |
Proof-Checking Protocols Using Bisimulations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CONCUR ![In: CONCUR '99: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24-27, 1999, Proceedings, pp. 525-540, 1999, Springer, 3-540-66425-4. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
40 | Andrei Popescu 0001, Elsa L. Gunter, Christopher J. Osborn |
Strong Normalization for System F by HOAS on Top of FOAS. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LICS ![In: Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom, pp. 31-40, 2010, IEEE Computer Society, 978-0-7695-4114-3. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
Higher-Order Abstract Syntax, Isabelle/HOL, System F |
40 | Patrick Schaller, Benedikt Schmidt 0002, David A. Basin, Srdjan Capkun |
Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSF ![In: Proceedings of the 22nd IEEE Computer Security Foundations Symposium, CSF 2009, Port Jefferson, New York, USA, July 8-10, 2009, pp. 109-123, 2009, IEEE Computer Society, 978-0-7695-3712-2. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
Wireless Network Protocols, Security Protocols, Isabelle/HOL, Formal Security Model |
40 | Gerwin 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](Pics/bibsonomy.png) |
SOSP ![In: Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, October 11-14, 2009, pp. 207-220, 2009, ACM, 978-1-60558-752-3. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
l4, sel4, microkernel, isabelle/hol |
40 | Philip 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](Pics/bibsonomy.png) |
Haskell ![In: Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2006, Portland, Oregon, USA, September 17, 2006, pp. 60-71, 2006, ACM, 1-59593-489-8. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
formalisation, verification, operating systems, rapid prototyping, Haskell, monads, executable specification, Isabelle/HOL |
39 | Achim D. Brucker, Burkhart Wolff |
hol-TestGen. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FASE ![In: Fundamental Approaches to Software Engineering, 12th International Conference, FASE 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, pp. 417-420, 2009, Springer, 978-3-642-00592-3. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP DOI BibTeX RDF |
symbolic test-case generations, theorem proving, black box testing, white box testing, interactive testing |
39 | Ludovic Henrio, Florian Kammüller |
A Mechanized Model of the Theory of Objects. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMOODS ![In: Formal Methods for Open Object-Based Distributed Systems, 9th IFIP WG 6.1 International Conference, FMOODS 2007, Paphos, Cyprus, June 6-8, 2007, Proceedings, pp. 190-205, 2007, Springer, 978-3-540-72919-8. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
39 | Achim D. Brucker, Burkhart Wolff |
Interactive Testing with HOL-TestGen. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FATES ![In: Formal Approaches to Software Testing, 5th International Workshop, FATES 2005, Edinburgh, UK, July 11, 2005, Revised Selected Papers, pp. 87-102, 2005, Springer, 3-540-34454-3. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
symbolic test case generations, theorem proving, black box testing, white box testing, interactive testing |
39 | Thomas Santen |
Isomorphisms - A Link Between the Shallow and the Deep. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September, 1999, Proceedings, pp. 37-54, 1999, Springer, 3-540-66463-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
32 | Jonathan 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](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2401.12061, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
32 | Julian Parsert |
Linear Programming in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2403.19639, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
32 | Mnacho Echenim, Mehdi Mhalla |
A Formalization of the CHSH Inequality and Tsirelson's Upper-bound in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 68(1), pp. 2, March 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
32 | Hanna 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](Pics/bibsonomy.png) |
TACAS (1) ![In: Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, pp. 311-330, 2024, Springer, 978-3-031-57245-6. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
32 | Sohaib Soualah, Mohamed Khalgui, Allaoua Chaoui |
Effective Parallel Formal Verification of Reconfigurable Discrete-Event Systems Formalizing with Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AINA (2) ![In: Advanced Information Networking and Applications - Proceedings of the 38th International Conference on Advanced Information Networking and Applications (AINA-2024), Kitakyushu, Japan, 17-19 April, 2024, Volume 2, pp. 199-212, 2024, Springer, 978-3-031-57852-6. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
32 | Andreas V. Hess, Sebastian Alexander Mödersheim, Achim D. Brucker |
Stateful Protocol Composition in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Priv. Secur. ![In: ACM Trans. Priv. Secur. 26(3), pp. 25:1-25:36, August 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
32 | Jonas Bayer, Aleksey Gonus, Christoph Benzmüller, Dana S. Scott |
Category Theory in Isabelle/HOL as a Basis for Meta-logical Investigation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2306.09074, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
32 | Ata Keskin |
A Formalization of Martingales in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2311.06188, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
32 | Chelsea Edmonds, Lawrence C. Paulson |
Formal Probabilistic Methods for Combinatorial Structures in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2310.00513, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
32 | Leo Freitas |
Topologically sorting VDM-SL definitions for Isabelle/HOL translation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2304.15006, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
32 | Simon Foster 0001, Burkhart Wolff |
Automated Reasoning for Physical Quantities, Units, and Measurements in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2302.07629, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
32 | Terru Stübinger, Lars Hupel |
Extending Isabelle/HOL's Code Generator with support for the Go programming language. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2310.02704, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
32 | Stepán Starosta |
Infinite Words and Morphic Languages Formalized in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2303.11445, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
32 | Leo Freitas, Peter Gorm Larsen |
VDM recursive functions in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2303.17457, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
32 | Mnacho Echenim, Mehdi Mhalla |
A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2306.12535, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 67(1), pp. 2, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
32 | Richard Schmoetten, Jake E. Palmer, Jacques D. Fleuriot |
Correction: Towards Formalising Schutz' Axioms for Minkowski Spacetime in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 67(1), pp. 9, March 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Log. Comput. ![In: J. Log. Comput. 33(4), pp. 818-836, June 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
32 | Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato 0001 |
Program logic for higher-order probabilistic programs in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Sci. Comput. Program. ![In: Sci. Comput. Program. 230, pp. 102993, August 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
32 | Pasquale Noce |
Formal Verification of Cryptographic Protocols with Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Handb. Formal Anal. Verification Cryptogr. ![In: Handbook of Formal Analysis and Verification in Cryptography, pp. 153-212, 2023, CRC Press, 978-1-003-09005-2. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
32 | Achim D. Brucker, Amy Stell |
Verifying Feedforward Neural Networks for Classification in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FM ![In: Formal Methods - 25th International Symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, Proceedings, pp. 427-444, 2023, Springer, 978-3-031-27480-0. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
Displaying result #1 - #100 of 460 (100 per page; Change: ) Pages: [ 1][ 2][ 3][ 4][ 5][ >>] |
|