Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
16 | Johannes Åman Pohjola, Arve Gengelbach |
A Mechanised Semantics for HOL with Ad-hoc Overloading. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020., pp. 498-515, 2020, EasyChair. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Andreas Lochbihler, Ognjen Maric |
Authenticated Data Structures as Functors in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMBC@CAV ![In: 2nd Workshop on Formal Methods for Blockchains, FMBC@CAV 2020, July 20-21, 2020, Los Angeles, California, USA (Virtual Conference)., pp. 6:1-6:15, 2020, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-169-6. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Arve Gengelbach, Tjark Weber |
Proof-Theoretic Conservative Extension of HOL with Ad-hoc Overloading. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICTAC ![In: Theoretical Aspects of Computing - ICTAC 2020 - 17th International Colloquium, Macau, China, November 30 - December 4, 2020, Proceedings, pp. 23-42, 2020, Springer, 978-3-030-64275-4. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Maria Ribeiro, Pedro Adão, Paulo Mateus |
Formal Verification of Ethereum Smart Contracts Using Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Logic, Language, and Security ![In: Logic, Language, and Security - Essays Dedicated to Andre Scedrov on the Occasion of His 65th Birthday, pp. 71-97, 2020, Springer, 978-3-030-62076-9. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Sebastian Reiche, Christoph Benzmüller |
Public Announcement Logic in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
DaLí ![In: Dynamic Logic. New Trends and Applications - Third International Workshop, DaLí 2020, Prague, Czech Republic, October 9-10, 2020, Revised Selected Papers, pp. 222-238, 2020, Springer, 978-3-030-65839-7. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Paulo Emílio de Vilhena, Lawrence C. Paulson |
Algebraically Closed Fields in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR (2) ![In: Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, pp. 204-220, 2020, Springer, 978-3-030-51053-4. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Walter Guttmann |
Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR (2) ![In: Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, pp. 236-253, 2020, Springer, 978-3-030-51053-4. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | 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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICSOFT (Selected Papers) ![In: Software Technologies - 15th International Conference, ICSOFT 2020, Online Event, July 7-9, 2020, Revised Selected Papers, pp. 227-241, 2020, Springer, 978-3-030-83006-9. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | 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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICSOFT ![In: Proceedings of the 15th International Conference on Software Technologies, ICSOFT 2020, Lieusaint, Paris, France, July 7-9, 2020., pp. 250-259, 2020, ScitePress, 978-989-758-443-5. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Fabian Immler, Yong Kiam Tan |
The Poincaré-Bendixson theorem in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020., pp. 338-352, 2020, ACM, 978-1-4503-7097-4. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Ralph Bottesch, Max W. Haslbeck, Alban Reynaud, René Thiemann |
Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
NFM ![In: NASA Formal Methods - 12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11-15, 2020, Proceedings, pp. 233-250, 2020, Springer, 978-3-030-55753-9. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Yutaka Nagashima |
Smart Induction for Isabelle/HOL (Tool Paper). ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMCAD ![In: 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, September 21-24, 2020, pp. 245-254, 2020, IEEE, 978-3-85448-042-6. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Jonathan Julián Huerta y Munive |
Affine Systems of ODEs in Isabelle/HOL for Hybrid-Program Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SEFM ![In: Software Engineering and Formal Methods - 18th International Conference, SEFM 2020, Amsterdam, The Netherlands, September 14-18, 2020, Proceedings, pp. 77-92, 2020, Springer, 978-3-030-58767-3. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar |
A Framework for Formal Dynamic Dependability Analysis Using HOL Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CICM ![In: Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings, pp. 105-122, 2020, Springer, 978-3-030-53517-9. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Laura Kovács, Hanna Lachnitt, Stefan Szeider |
Formalizing Graph Trail Properties in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CICM ![In: Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings, pp. 190-205, 2020, Springer, 978-3-030-53517-9. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Yutaka Nagashima |
Simple Dataset for Proof Method Recommendation in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CICM ![In: Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings, pp. 297-302, 2020, Springer, 978-3-030-53517-9. The full citation details ...](Pics/full.jpeg) |
2020 |
DBLP DOI BibTeX RDF |
|
16 | Mathias Fleury |
Formalization of logical calculi in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2020 |
RDF |
|
16 | Jonathan Julián Huerta y Munive |
Algebraic verification of hybrid systems in Isabelle/HOL ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2020 |
RDF |
|
16 | Wilayat Khan, David Sanán, Zhe Hou, Yang Liu 0003 |
On embedding a hardware description language in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Des. Autom. Embed. Syst. ![In: Des. Autom. Embed. Syst. 23(3-4), pp. 123-151, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Lars Hupel |
Certifying Dictionary Construction in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Fundam. Informaticae ![In: Fundam. Informaticae 170(1-3), pp. 177-205, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Jingzhi Zhang, Guohui Wang, Zhiping Shi 0002, Yong Guan, Yongdong Li |
Formalization of functional variation in HOL Light. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Log. Algebraic Methods Program. ![In: J. Log. Algebraic Methods Program. 106, pp. 29-38, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Thomas Bittner |
On the computational realization of formal ontologies: Formalizing an ontology of instantiation in spacetime using Isabelle/HOL as a case study. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Appl. Ontology ![In: Appl. Ontology 14(3), pp. 251-292, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar |
A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Access ![In: IEEE Access 7, pp. 136176-136192, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Christoph Benzmüller, Ali Farjami, Paul Meder, Xavier Parent |
I/O Logic in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FLAP ![In: FLAP 6(5), pp. 715-732, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Yassmeen Elderhalli, Waqar Ahmad, Osman Hasan, Sofiène Tahar |
Probabilistic Analysis of Dynamic Fault Trees using HOL Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FLAP ![In: FLAP 6(3), pp. 469-512, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Christoph Benzmüller, Ali Farjami, Xavier Parent |
åqvist's Dyadic Deontic Logic E in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FLAP ![In: FLAP 6(5), pp. 733-754, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel |
From LCF to Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1907.02836, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Yutaka Nagashima |
Towards Evolutionary Theorem Proving for Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1904.08468, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Yutaka Nagashima |
LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1906.08084, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Jonathan Julián Huerta y Munive, Georg Struth |
Predicate Transformer Semantics for Hybrid Systems: Verification Components for Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1909.05618, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Simon Foster 0001, Jonathan Julián Huerta y Munive, Georg Struth |
Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1910.13554, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Waqar Ahmed, Shahid Ali Murtza, Osman Hasan, Sofiène Tahar |
On the Formalization of Importance Measures using HOL Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1904.01605, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Mathias Fleury, Hans-Jörg Schurr |
Reconstructing veriT Proofs in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PxTP ![In: Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019., pp. 36-50, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar |
Dynamic Dependability Analysis of Shuffle-exchange Networks using HOL Theorem Proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1910.11203, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar |
A Formally Verified HOL Algebra for Dynamic Reliability Block Diagrams. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1908.01930, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Safouan Taha, Lina Ye, Burkhart Wolff |
HOL-CSP Version 2.0. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2019, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Peter Lammich, Simon Wimmer 0001 |
IMP2 - Simple Program Verification in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2019, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Lars Hupel |
A Verified Code Generator from Isabelle/HOL to CakeML. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2019, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP BibTeX RDF |
|
16 | Li-Ming Li, Zhi-Ping Shi 0002, Yong Guan, Qianying Zhang, Yong-Dong Li |
Formalization of Geometric Algebra in HOL Light. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 63(3), pp. 787-808, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Ondrej Kuncar, Andrei Popescu 0001 |
A Consistent Foundation for Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 62(4), pp. 531-555, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Peter Lammich |
Refinement to Imperative HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 62(4), pp. 481-503, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Wenda Li, Grant Olney Passmore, Lawrence C. Paulson |
Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 62(1), pp. 69-91, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Mohammad Abdulaziz, Lawrence C. Paulson |
An Isabelle/HOL Formalisation of Green's Theorem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 63(3), pp. 763-786, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Peter Lammich, S. Reza Sefidgar |
Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 62(2), pp. 261-280, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel |
From LCF to Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 31(6), pp. 675-698, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Said Meghzili, Allaoua Chaoui, Martin Strecker, Elhillali Kerkouche |
Verification of Model Transformations Using Isabelle/HOL and Scala. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Inf. Syst. Frontiers ![In: Inf. Syst. Frontiers 21(1), pp. 45-65, 2019. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Yutaka Nagashima |
LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
APLAS ![In: Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings, pp. 266-287, 2019, Springer, 978-3-030-34174-9. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Yutaka Nagashima |
Towards evolutionary theorem proving for isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
GECCO (Companion) ![In: Proceedings of the Genetic and Evolutionary Computation Conference Companion, GECCO 2019, Prague, Czech Republic, July 13-17, 2019., pp. 419-420, 2019, ACM, 978-1-4503-6748-6. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Peter Lammich |
Generating Verified LLVM from Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 22:1-22:19, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Manuel Eberl |
Nine Chapters of Analytic Number Theory in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 16:1-16:19, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Maximilian P. L. Haslbeck, Peter Lammich |
Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA., pp. 20:1-20:18, 2019, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-122-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Wenda Li, Lawrence C. Paulson |
Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pp. 52-64, 2019, ACM, 978-1-4503-6222-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Bertram Felgenhauer, Aart Middeldorp, T. V. H. Prathamesh, Franziska Rapp |
A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pp. 132-143, 2019, ACM, 978-1-4503-6222-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Jasmin Christian Blanchette |
Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pp. 1-13, 2019, ACM, 978-1-4503-6222-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Fabian Immler, Bohua Zhan |
Smooth manifolds and types to sets for linear algebra in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pp. 65-77, 2019, ACM, 978-1-4503-6222-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Waqar Ahmad, Shahid Ali Murtza, Osman Hasan, Sofiène Tahar |
On the formalization of importance measures using HOL theorem proving. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FormaliSE@ICSE ![In: Proceedings of the 7th International Workshop on Formal Methods in Software Engineering, FormaliSE@ICSE 2019, Montreal, QC, Canada, May 27, 2019., pp. 109-118, 2019, IEEE / ACM, 978-1-7281-3373-7. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Andreas Lööw, Magnus O. Myreen |
A proof-producing translator for verilog development in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FormaliSE@ICSE ![In: Proceedings of the 7th International Workshop on Formal Methods in Software Engineering, FormaliSE@ICSE 2019, Montreal, QC, Canada, May 27, 2019., pp. 99-108, 2019, IEEE / ACM, 978-1-7281-3373-7. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Ralph Bottesch, Max W. Haslbeck, René Thiemann |
Verifying an Incremental Theory Solver for Linear Arithmetic in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FroCos ![In: Frontiers of Combining Systems - 12th International Symposium, FroCoS 2019, London, UK, September 4-6, 2019, Proceedings, pp. 223-239, 2019, Springer, 978-3-030-29006-1. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Yuhan Nie, Zhiping Shi 0002, Aixuan Wu, Ximeng Li 0003, Guohui Wang, Yong Guan |
A HOL Theory of the Differential for Matrix Functions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TASE ![In: 2019 International Symposium on Theoretical Aspects of Software Engineering, TASE 2019, Guilin, China, July 29-31, 2019, pp. 121-127, 2019, IEEE, 978-1-7281-3342-3. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Manuel Eberl |
Verified Real Asymptotics in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISSAC ![In: Proceedings of the 2019 on International Symposium on Symbolic and Algebraic Computation, ISSAC 2019, Beijing, China, July 15-18, 2019., pp. 147-154, 2019, ACM, 978-1-4503-6084-5. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Alexander Maletzky |
Formalization of Dubé's Degree Bounds for Gröbner Bases in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CICM ![In: Intelligent Computer Mathematics - 12th International Conference, CICM 2019, Prague, Czech Republic, July 8-12, 2019, Proceedings, pp. 155-170, 2019, Springer, 978-3-030-23249-8. The full citation details ...](Pics/full.jpeg) |
2019 |
DBLP DOI BibTeX RDF |
|
16 | Lars Hupel |
Verified Code Generation from Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2019 |
RDF |
|
16 | Yiming Ouyang, Jianfeng Yang, Kun Xing, Zhengfeng Huang, Huaguo Liang |
An improved communication scheme for non-HOL-blocking wireless NoC. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Integr. ![In: Integr. 60, pp. 240-247, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Alexander Birch Jensen, John Bruntse Larsen, Anders Schlichtkrull, Jørgen Villadsen |
Programming and verifying a declarative first-order prover in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AI Commun. ![In: AI Commun. 31(3), pp. 281-299, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Adnan Rashid, Osman Hasan |
Formalization of Lerch's Theorem using HOL Light. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FLAP ![In: FLAP 5(8), pp. 1623-1652, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
16 | Sumayya Shiraz, Osman Hasan |
A Library for Combinational Circuit Verification Using the HOL Theorem Prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. ![In: IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 37(2), pp. 512-516, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
16 | François Thiré |
Sharing a Library between Proof Assistants: Reaching out to the HOL Family. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFMTP@FSCD ![In: Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2018, Oxford, UK, 7th July 2018., pp. 57-71, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Christoph Benzmüller, Xavier Parent |
I/O Logic in HOL - First Steps. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1803.09681, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
16 | Christoph Benzmüller, Ali Farjami, Xavier Parent |
Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1802.08454, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
16 | Jacques Carette, William M. Farmer, Patrick Laskowski |
HOL Light QE. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1802.00405, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
16 | Wenda Li, Lawrence C. Paulson |
Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1804.03922, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
16 | Wenda Li, Lawrence C. Paulson |
Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1811.11093, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
16 | Adnan Rashid, Osman Hasan |
Formalization of Lerch's Theorem using HOL Light. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1806.03049, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
16 | Alexander Maletzky, Fabian Immler |
Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1805.00304, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
16 | Yutaka Nagashima, Julian Parsert |
Goal-Oriented Conjecturing for Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1806.04774, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
16 | Artem Yushkovskiy, Stavros Tripakis |
Comparison of Two Theorem Provers: Isabelle/HOL and Coq. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1808.09701, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
16 | Yu Zhang, Yongwang Zhao, David Sanán |
A Verified Timsort C Implementation in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1812.03318, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
16 | Mnacho Echenim, Hervé Guiol, Nicolas Peltier |
Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1807.09873, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
16 | Ramana Kumar, Magnus O. Myreen |
Clocked Definitions in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1803.03417, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
16 | Yutaka Nagashima, Yilun He |
PaMpeR: Proof Method Recommendation System for Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1806.07239, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
16 | Chun Tian 0001, Davide Sangiorgi |
Unique Solutions of Contractions, CCS, and their HOL Formalisation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
EXPRESS/SOS ![In: Proceedings Combined 25th International Workshop on Expressiveness in Concurrency and 15th Workshop on Structural Operational Semantics, EXPRESS/SOS 2018, Beijing, China, September 3, 2018., pp. 122-139, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Oliver Bracevac, Richard Gay, Sylvia Grewe, Heiko Mantel, Henning Sudbrock, Markus Tasch |
An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2018, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
16 | Andreas Lochbihler, S. Reza Sefidgar |
Constructive Cryptography in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2018, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
16 | Mohammad Abdulaziz, Lawrence C. Paulson |
An Isabelle/HOL formalisation of Green's Theorem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2018, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
16 | David Fuenmayor, Christoph Benzmüller |
Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2018, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
16 | Marco Maggesi |
A Formalization of Metric Spaces in HOL Light. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 60(2), pp. 237-254, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Stefan Hallerstede |
Tobias Nipkow and Gerwin Klein: Concrete Semantics with Isabelle/HOL - Springer Verlag, 2014, x + 289 pp, € 63, 29 (Hardback), ISBN 978-3-319-10542-0, http: //www.concrete-semantics.org/. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 30(3-4), pp. 491-492, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Guohui Wang, Yong Guan, Zhiping Shi 0002, Qianying Zhang, Xiaojuan Li, Yongdong Li |
Formalization of Symplectic Geometry in HOL-Light. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFEM ![In: Formal Methods and Software Engineering - 20th International Conference on Formal Engineering Methods, ICFEM 2018, Gold Coast, QLD, Australia, November 12-16, 2018, Proceedings, pp. 270-283, 2018, Springer, 978-3-030-02449-9. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Diego Marmsoler |
A Framework for Interactive Verification of Architectural Design Patterns in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFEM ![In: Formal Methods and Software Engineering - 20th International Conference on Formal Engineering Methods, ICFEM 2018, Gold Coast, QLD, Australia, November 12-16, 2018, Proceedings, pp. 251-269, 2018, Springer, 978-3-030-02449-9. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Achim D. Brucker, Michael Herzberg |
A Formal Semantics of the Core DOM in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
WWW (Companion Volume) ![In: Companion of the The Web Conference 2018 on The Web Conference 2018, WWW 2018, Lyon , France, April 23-27, 2018, pp. 741-749, 2018, ACM. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Cheikh Salmi, Mohamed Chaabani, Mohamed Mezghiche |
A Formalized Procedure for Database Horizontal Fragmentation in Isabelle/HOL Proof Assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MEDI ![In: Model and Data Engineering - 8th International Conference, MEDI 2018, Marrakesh, Morocco, October 24-26, 2018, Proceedings, pp. 346-353, 2018, Springer, 978-3-030-00855-0. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Lars Hupel, Tobias Nipkow |
A Verified Compiler from Isabelle/HOL to CakeML. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ESOP ![In: 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, pp. 999-1026, 2018, Springer, 978-3-319-89883-4. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus O. Myreen, Yong Kiam Tan, Michael Norrish |
Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: 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, pp. 646-662, 2018, Springer, 978-3-319-94204-9. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Chantal Keller |
Tactic Program-Based Testing and Bounded Verification in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TAP@STAF ![In: Tests and Proofs - 12th International Conference, TAP@STAF 2018, Toulouse, France, June 27-29, 2018, Proceedings, pp. 103-119, 2018, Springer, 978-3-319-92993-4. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Rachid Darbali-Zamora, Nicolas Cobo-Yepes, Eduardo I. Ortiz-Rivera, Erick E. Aponte-Bezares, Amilcar A. Rincon-Charris |
Applying HOL/PBL to Prepare Undergraduate Students into Graduate Level Studies in the Field of Aerospace Engineering Using the Puerto Rico CubeSat Project Initiative. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FIE ![In: IEEE Frontiers in Education Conference, FIE 2018, San Jose, CA, USA, October 3-6, 2018, pp. 1-8, 2018, IEEE, 978-1-5386-1174-6. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Reto Achermann, Lukas Humbel, David A. Cock, Timothy Roscoe |
Physical Addressing on Real Hardware in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 1-19, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Andreas Lochbihler |
Fast Machine Words in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 388-410, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Jacques Carette, William M. Farmer, Patrick Laskowski |
HOL Light QE. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: 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, pp. 215-234, 2018, Springer, 978-3-319-94820-1. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Sidney Amani, Myriam Bégel, Maksym Bortin, Mark Staples |
Towards verifying ethereum smart contract bytecode in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018, pp. 66-77, 2018, ACM, 978-1-4503-5586-5. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|
16 | Mathias Fleury, Jasmin Christian Blanchette, Peter Lammich |
A verified SAT solver with watched literals using imperative HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CPP ![In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018, pp. 158-171, 2018, ACM, 978-1-4503-5586-5. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP DOI BibTeX RDF |
|