Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
16 | Hamdi Yahyaoui, Mourad Debbabi, Nadia Tawbi |
A Denotational Semantic Model for Validating JVML/CLDC Optimizations under Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
QSIC ![In: Seventh International Conference on Quality Software (QSIC 2007), 11-12 October 2007, Portland, Oregon, USA, pp. 348-355, 2007, IEEE Computer Society. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
16 | Juliano Manabu Iyoda |
Translating HOL functions to hardware. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2007 |
RDF |
|
16 | Cheng Wang, Ross D. Murch |
Optimal downlink multi-user MIMO cross-layer scheduling using HOL packet waiting time. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Wirel. Commun. ![In: IEEE Trans. Wirel. Commun. 5(10), pp. 2856-2862, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
16 | Rabeb Mizouni, Sofiène Tahar, Paul Curzon |
Hybrid verification integrating HOL theorem proving with MDG model checking. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Microelectron. J. ![In: Microelectron. J. 37(11), pp. 1200-1207, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
16 | Tom Ridge |
Craig's Interpolation Theorem formalised and mechanised in Isabelle/HOL ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/cs/0607058, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP BibTeX RDF |
|
16 | J. Nathan Foster, Dimitrios Vytiniotis |
A Theory of Featherweight Java in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2006, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP BibTeX RDF |
|
16 | Norbert Schirmer |
Verification of sequential imperative programs in Isabelle-HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2006 |
RDF |
|
16 | Sean McLaughlin, Clark W. Barrett, Yeting Ge |
Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PDPAR@CAV ![In: Proceedings of the Third Workshop on Pragmatics of Decision Procedures in Automated Reasoning, PDPAR@CAV 2005, Edinburgh, UK, July 12, 2005, pp. 43-51, 2005, Elsevier. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
16 | Jan Olaf Blech, Sabine Glesner, Johannes Leitner, Steffen Mülling |
Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
COCV@ETAPS ![In: Proceedings of the Fourth International Workshop on Compiler Optimization meets Compiler Verification, COCV@ETAPS 2005, Edinburgh, UK, April 3, 2005, pp. 33-51, 2005, Elsevier. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
16 | Joe Hurd, Annabelle McIver, Carroll Morgan |
Probabilistic guarded commands mechanized in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Theor. Comput. Sci. ![In: Theor. Comput. Sci. 346(1), pp. 96-112, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
16 | Joris Walraevens, Bart Steyaert, Marc Moeneclaey, Herwig Bruneel |
Delay Analysis of a HOL Priority Queue. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Telecommun. Syst. ![In: Telecommun. Syst. 30(1-3), pp. 81-98, 2005. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
discrete-time priority queue, multimedia |
16 | Steven Obua |
Proving Bounds for Real Linear Programs in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Mathematics, Algorithms, Proofs ![In: Mathematics, Algorithms, Proofs, 9.-14. January 2005, 2005, Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP BibTeX RDF |
|
16 | Joris Walraevens, Bart Steyaert, Marc Moeneclaey, Herwig Bruneel |
A Discrete-Time HOL Priority Queue with Multiple Traffic Classes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICN (1) ![In: Networking - ICN 2005, 4th International Conference on Networking, ReunionIsland, France, April 17-21, 2005, Proceedings, Part I, pp. 620-627, 2005, Springer, 3-540-25339-4. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
16 | Anthony C. J. Fox |
An Algebraic Framework for Verifying the Correctness of Hardware with Input and Output: A Formalization in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CALCO ![In: Algebra and Coalgebra in Computer Science: First International Conference, CALCO 2005, Swansea, UK, September 3-6, 2005, Proceedings, pp. 157-174, 2005, Springer, 3-540-28620-9. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
16 | Sergey Tverdyshev |
Combination of Isabelle/HOL with Automatic Tools. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FroCoS ![In: Frontiers of Combining Systems, 5th International Workshop, FroCoS 2005, Vienna, Austria, September 19-21, 2005, Proceedings, pp. 302-309, 2005, Springer, 3-540-29051-6. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
16 | Daniel Hausmann 0001, Till Mossakowski, Lutz Schröder |
Iterative Circular Coinduction for CoCasl in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FASE ![In: Fundamental Approaches to Software Engineering, 8th International Conference, FASE 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings, pp. 341-356, 2005, Springer, 3-540-25420-X. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
16 | Joe Hurd, Annabelle McIver, Carroll Morgan |
Probabilistic Guarded Commands Mechanized in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
QAPL ![In: Proceedings of the Second Workshop on Quantitative Aspects of Programming Languages, QAPL 2004, Barcelona, Spain, March 27-28, 2004, pp. 95-111, 2004, Elsevier. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
16 | Tjark Weber |
Bounded Model Generation for Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
D/PDPAR@IJCAR ![In: Selected Papers from the Workshops on Disproving, D@IJCAR 2004, and the Second International Workshop on Pragmatics of Decision Procedures, PDPAR@IJCAR 2004, Cork, Ireland, July 2004, pp. 103-116, 2004, Elsevier. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
16 | Norbert Schirmer |
Analysing the Java package/access concepts in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Concurr. Pract. Exp. ![In: Concurr. Pract. Exp. 16(7), pp. 689-706, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
16 | Jonathan P. Seldin |
Interpreting HOL in the calculus of constructions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Appl. Log. ![In: J. Appl. Log. 2(2), pp. 173-189, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
16 | Orieta Celiku, Annabelle McIver |
Cost-Based Analysis of Probabilistic Programs Mechanised in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Nord. J. Comput. ![In: Nord. J. Comput. 11(2), pp. 102-128, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP BibTeX RDF |
|
16 | John Longley, Randy Pollack |
Reasoning About CBV Functional Programs in Isabelle/HOL. ![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. 201-216, 2004, Springer, 3-540-23017-3. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
16 | Jan Olaf Blech, Sabine Glesner |
A Formal Correctness Proof for Code Generation from SSA Form in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
GI Jahrestagung (2) ![In: 34. Jahrestagung der Gesellschaft für Informatik, Informatik verbindet, INFORMATIK 2004, Ulm, Germany, September 20-24, 2004, Band 2, pp. 449-458, 2004, GI, 3-88579-380-6. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP BibTeX RDF |
|
16 | Kenro Yatake, Toshiaki Aoki, Takuya Katayama |
Collaboration-based verification of Object-Oriented models in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
VVEIS ![In: Verification and Validation of Enterprise Information Systems, Proceedings of the 2nd International Workshop on Verification and Validation of Enterprise Information Systems, VVEIS 2004, In conjunction with ICEIS 2004, Porto, Portugal, April 2004, pp. 78-80, 2004, INSTICC Press, 972-8865-03-1. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP BibTeX RDF |
|
16 | Stefan Berghofer, Tobias Nipkow |
Random Testing in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SEFM ![In: 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 28-30 September 2004, Beijing, China, pp. 230-239, 2004, IEEE Computer Society, 0-7695-2222-X. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
16 | Nicole Rauch, Burkhart Wolff |
Formalizing Java's Two's-Complement Integral Type in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMICS ![In: Eighth International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2003, Roros, Norway, June 5-7, 2003, pp. 41-58, 2003, Elsevier. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
16 | Achim D. Brucker, Frank Rittinger, Burkhart Wolff |
HOL-Z 2.0: A Proof Environment for Z-Specifications. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Univers. Comput. Sci. ![In: J. Univers. Comput. Sci. 9(2), pp. 152-172, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
16 | Christine Röckl, Daniel Hirschkoff |
A fully adequate shallow embedding of the [pi]-calculus in Isabelle/HOL with mechanized syntax analysis. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Funct. Program. ![In: J. Funct. Program. 13(2), pp. 415-451, 2003. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
16 | Thumrongsak Kosiyatrakul, Susan Older, Polar Humenn, Shiu-Kai Chin |
Implementing a Calculus for Distributed Access Control in Higher Order Logic and HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MMM-ACNS ![In: Computer Network Security, Second International Workshop on Mathematical Methods, Models, and Architectures for Computer Network Security, MMM-ACNS 2003, St. Petersburg, Russia, September 21-23, 2003, Proceedings, pp. 32-46, 2003, Springer, 3-540-40797-9. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
16 | Haykal Tej |
HOL-CSP: mechanised formal devlopment mof concurrent processes. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2003 |
RDF |
|
16 | Sylvain Delas, Ravi Mazumdar, Catherine Rosenberg |
Tail Asymptotics for HOL Priority Queues Handling a Large Number of Independent Stationary Sources. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Queueing Syst. Theory Appl. ![In: Queueing Syst. Theory Appl. 40(2), pp. 183-204, 2002. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
16 | Michael Norrish, Konrad Slind |
A Thread of HOL Development. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Comput. J. ![In: Comput. J. 45(1), pp. 37-45, 2002. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
16 | Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel 0001 |
Isabelle/HOL - A Proof Assistant for Higher-Order Logic ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2002 |
DOI RDF |
|
16 | Achim D. Brucker, Burkhart Wolff |
HOL-OCL: Experiences, Consequences and Design Choices. ![Search on Bibsonomy](Pics/bibsonomy.png) |
UML ![In: UML 2002 - The Unified Modeling Language, 5th International Conference, Dresden, Germany, September 30 - October 4, 2002, Proceedings, pp. 196-211, 2002, Springer, 3-540-44254-5. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
refinement, OCL, formal semantics, constraint languages |
16 | Achim D. Brucker, Burkhart Wolff |
A Proposal for a Formal OCL Semantics in Isabelle/HOL. ![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. 99-114, 2002, Springer, 3-540-44039-9. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
shallow embedding, UML, testing, OCL, Isabelle |
16 | Tobias Nipkow |
Structured Proofs in Isar/HOL. ![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. 259-278, 2002, Springer, 3-540-14031-X. The full citation details ...](Pics/full.jpeg) |
2002 |
DBLP DOI BibTeX RDF |
|
16 | Leonor Prensa Nieto |
Verification of parallel programs with the Owicki-Gries and Rely-Guarantee methods in Isabelle, HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2002 |
RDF |
|
16 | Haiyan Xiong |
Providing a formal linkage between MDG and HOL based on a verified MDG system. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2002 |
RDF |
|
16 | David von Oheimb |
Hoare logic for Java in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Concurr. Comput. Pract. Exp. ![In: Concurr. Comput. Pract. Exp. 13(13), pp. 1173-1214, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
16 | Gilles Dowek, Thérèse Hardin, Claude Kirchner |
HOL-λσ: an intentional first-order expression of higher-order logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Math. Struct. Comput. Sci. ![In: Math. Struct. Comput. Sci. 11(1), pp. 21-45, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP BibTeX RDF |
|
16 | Christine Röckl |
A First-Order Syntax for the Pi-Calculus in Isabelle/HOL using Permutations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Mechanized Reasoning about Languages with Variable Binding, MERLIN 2001, in connection with IJCAR 2001, Siena, Italy, June 18, 2001, pp. 1-17, 2001, Elsevier. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
16 | Yasuhiko Minamide, Koji Okuma |
Verifying the CPS Transformation in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
APLAS ![In: The Second Asian Workshop on Programming Languages and Systems, APLAS'01, Korea Advanced Institute of Science and Technology, Daejeon, Korea, December 17-18, 2001, Proceedings, pp. 29-37, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP BibTeX RDF |
|
16 | David von Oheimb |
Analyzing Java in Isabelle-HOL: formalization, type safety and Hoare logic. (PDF / PS) ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2001 |
RDF |
|
16 | John Harrison 0001 |
Floating Point Verification in HOL Light: The Exponential Function. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Methods Syst. Des. ![In: Formal Methods Syst. Des. 16(3), pp. 271-305, 2000. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
16 | Mike Gordon |
From LCF to HOL: a short history. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proof, Language, and Interaction ![In: Proof, Language, and Interaction, Essays in Honour of Robin Milner, pp. 169-186, 2000, The MIT Press, 978-0-262-16188-6. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP BibTeX RDF |
|
16 | Christine Röckl |
Proving Write Invalidate Cache Coherence with Bisimulations in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FBT ![In: Formale Beschreibungstechniken für verteilte Systeme, 10. GI/ITG-Fachgespräch, Lübeck, Juni 2000, pp. 69-78, 2000, Verlag Shaker, 3-8265-7491-5. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP BibTeX RDF |
|
16 | Wai Wong |
Validation of HOL Proofs by Proof Checking. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Methods Syst. Des. ![In: Formal Methods Syst. Des. 14(2), pp. 193-212, 1999. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
16 | Sofiène Tahar, Paul Curzon |
Comparing HOL and MDG: a Case Study on the Verification of an ATM Switch Fabric. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Nord. J. Comput. ![In: Nord. J. Comput. 6(4), pp. 372-402, 1999. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP BibTeX RDF |
|
16 | Wolfgang Naraschewski, Tobias Nipkow |
Type Inference Verified: Algorithm W in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 23(3-4), pp. 299-318, 1999. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
16 | Olaf Müller, Tobias Nipkow, David von Oheimb, Oscar Slotosch |
HOLCF=HOL+LCF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Funct. Program. ![In: J. Funct. Program. 9(2), pp. 191-223, 1999. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
16 | Stefan Berghofer, Markus Wenzel 0001 |
Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering. ![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. 19-36, 1999, Springer, 3-540-66463-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
16 | Gilles Dowek, Thérèse Hardin, Claude Kirchner |
HOL-lambdasigma: An Intentional First-Order Expression of Higher-Order Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
RTA ![In: Rewriting Techniques and Applications, 10th International Conference, RTA-99, Trento, Italy, July 2-4, 1999, Proceedings, pp. 317-331, 1999, Springer, 3-540-66201-4. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
16 | Tobias Nipkow, Leonor Prensa Nieto |
Owicki/Gries in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FASE ![In: Fundamental Approaches to Software Engineering, Second Internationsl Conference, FASE'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. 188-203, 1999, Springer, 3-540-65718-5. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
16 | Michael Norrish |
C formalised in HOL ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
1999 |
RDF |
|
16 | John Harrison 0001, Laurent Théry |
A Skeptic's Approach to Combining HOL and Maple. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 21(3), pp. 279-294, 1998. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
16 | Norbert Völker |
Ein Rahmen zur Verifikation von SPS-Funktionsbausteinen in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
1998 |
RDF |
|
16 | W. O. David Griffioen, Marieke Huisman |
A Comparison of PVS and Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings, pp. 123-142, 1998, Springer, 3-540-64987-5. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
16 | Demetres D. Kouvatsos, Irfan-Ullah Awan |
Approximate Analysis of Arbitrary Open Networks with HOL Priorities and PBS Scheme. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ESM ![In: 12th European Simulation Multiconference - Simulation - Past, Present and Future, June 16-19, 1998, Machester, United Kingdom, pp. 741-746, 1998, SCS Europe, 1-56555-148-6. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP BibTeX RDF |
|
16 | Thomas Santen |
On the Semantic Relation of Z and HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ZUM ![In: ZUM '98: The Z Formal Specification Notation, 11th International Conference of Z Users, Berlin, Germany, September 24-26, 1998, Proceedings, pp. 96-115, 1998, Springer, 3-540-65070-9. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
16 | Christoph Lüth, Einar W. Karlsen, Kolyang 0001, Stefan Westmeier, Burkhart Wolff |
HOL-Z in the UniForM-Wokbench - A Case Study in Tool Integration for Z. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ZUM ![In: ZUM '98: The Z Formal Specification Notation, 11th International Conference of Z Users, Berlin, Germany, September 24-26, 1998, Proceedings, pp. 116-134, 1998, Springer, 3-540-65070-9. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
16 | David A. Basin, Stefan Friedrich 0001 |
Combining WS1S and HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FroCoS ![In: Frontiers of Combining Systems, Second International Workshop, FroCoS 1998, Amsterdam, The Netherlands, October 2-4, 1998, Proceedings, pp. 39-56, 1998, Research Studies Press/Wiley. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP BibTeX RDF |
|
16 | Jim Grundy, Thomas Långbacka |
Recording HOL Proofs in a Structured Browsable Format. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AMAST ![In: Algebraic Methodology and Software Technology, 6th International Conference, AMAST '97, Sydney, Australia, December 13-17, 1997, Proceedings, pp. 567-571, 1997, Springer, 3-540-63888-1. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
16 | John Harrison 0001 |
Floating Point Verification in HOL Light: The Exponential Function. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AMAST ![In: Algebraic Methodology and Software Technology, 6th International Conference, AMAST '97, Sydney, Australia, December 13-17, 1997, Proceedings, pp. 246-260, 1997, Springer, 3-540-63888-1. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
16 | Matthias Mutz |
Automatic post-synthesis verification support for a high level synthesis step by using the HOL theorem proving system. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CHARME ![In: Advances in Hardware Design and Verification, IFIP WG 10.5 International Conference on Correct Hardware Design and Verification Methods, 16-18 October 1997, Montréal, Québec, Canada, pp. 291-308, 1997, Chapman & Hall, 0-412-81330-0. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP BibTeX RDF |
|
16 | Monica Nesi |
Mechanising a modal logic for value-passing agents in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
INFINITY ![In: First International Workshop on Verification of Infinite State Systems, Infinity 1996, Università di Pisa, Pisa, Italy, August 30-31, 1996, pp. 31-46, 1996, Elsevier. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
16 | Vincent Zammit |
A Mechanisation of Computability Theory in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings, pp. 431-446, 1996, Springer, 3-540-61587-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
16 | John Harrison 0001 |
Stålmarck's Algorithm as a HOL Derived Rule. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings, pp. 221-234, 1996, Springer, 3-540-61587-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
16 | Dirk Eisenbiegler, Christian Blumenröhr, Ramayya Kumar |
Implementation Issues About the Embedding of Existing High Level Synthesis Algorithms in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings, pp. 157-172, 1996, Springer, 3-540-61587-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
16 | Stephen H. Brackin |
Deciding Cryptographic Protocol Adequacy with HOL: The Implementation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings, pp. 61-76, 1996, Springer, 3-540-61587-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
16 | John Harrison 0001 |
A Mizar Mode for HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings, pp. 203-220, 1996, Springer, 3-540-61587-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
16 | Sofiène Tahar, Paul Curzon |
A Comparison of MDG and HOL for Hardware Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings, pp. 415-430, 1996, Springer, 3-540-61587-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
16 | Sten Agerholm, Ilya Beylin, Peter Dybjer |
A Comparison of HOL and ALF Formalizations of a Categorical Coherence Theorem. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings, pp. 17-32, 1996, Springer, 3-540-61587-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
16 | Douglas J. Howe |
Importing Mathematics from HOL into Nuprl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings, pp. 267-281, 1996, Springer, 3-540-61587-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
16 | Kolyang 0001, Thomas Santen, Burkhart Wolff |
A Structure Preserving Encoding of Z in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings, pp. 283-298, 1996, Springer, 3-540-61587-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
16 | Douglas J. Howe |
Semantic Foundations for Embedding HOL in Nuprl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AMAST ![In: Algebraic Methodology and Software Technology, 5th International Conference, AMAST '96, Munich, Germany, July 1-5, 1996, Proceedings, pp. 85-101, 1996, Springer, 3-540-61463-X. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
16 | Wolfgang Naraschewski, Tobias Nipkow |
Type Inference Verified: Algorithm W in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop TYPES'96, Aussois, France, December 15-19, 1996, Selected Papers, pp. 317-332, 1996, Springer, 3-540-65137-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
16 | M. Vishnu, Jon W. Mark |
HOL-EDD: A Flexible Service Scheduling Scheme for ATM Networks. ![Search on Bibsonomy](Pics/bibsonomy.png) |
INFOCOM ![In: Proceedings IEEE INFOCOM '96, The Conference on Computer Communications, Fifteenth Annual Joint Conference of the IEEE Computer and Communications Societies, Networking the Next Generation, San Francisco, CA, USA, March 24-28, 1996, pp. 647-654, 1996, IEEE Computer Society, 0-8186-7292-7. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
16 | John Harrison 0001 |
HOL Light: A Tutorial Introduction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMCAD ![In: Formal Methods in Computer-Aided Design, First International Conference, FMCAD '96, Palo Alto, California, USA, November 6-8, 1996, Proceedings, pp. 265-269, 1996, Springer, 3-540-61937-2. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
16 | Ralf Reetz, Thomas Kropf |
A Flowgraph Semantics of VHDL: Toward a VHDL Verification Workbench in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Methods Syst. Des. ![In: Formal Methods Syst. Des. 7(1/2), pp. 73-99, 1995. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
16 | Jonathan P. Bowen, Mike Gordon |
A shallow embedding of Z in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Inf. Softw. Technol. ![In: Inf. Softw. Technol. 37(5-6), pp. 269-276, 1995. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
16 | John Harrison 0001 |
Binary Decision Diagrams as a HOL Derived Rule. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Comput. J. ![In: Comput. J. 38(2), pp. 162-170, 1995. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
16 | Elsa L. Gunter, Savi Maharaj |
Studying the ML Module System in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Comput. J. ![In: Comput. J. 38(2), pp. 142-151, 1995. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
16 | Sten Agerholm |
LCF Examples in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Comput. J. ![In: Comput. J. 38(2), pp. 121-130, 1995. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
16 | Joakim von Wright |
Representing Higher-Order Logic Proofs in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Comput. J. ![In: Comput. J. 38(2), pp. 171-179, 1995. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
16 | Rachel Cardell-Oliver |
HTTDs and HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Development of Reactive Systems ![In: Formal Development of Reactive Systems - Case Study Production Cell, pp. 261-276, 1995, Springer, 3-540-58867-1. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
16 | Rix Groenboom, Chris Hendriks, Indra Polak, Jan Terlouw, Jan Tijmen Udding |
Algebraic Proof Assistants in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MPC ![In: Mathematics of Program Construction, MPC'95, Kloster Irsee, Germany, July 17-21, 1995, Proceedings, pp. 304-321, 1995, Springer, 3-540-60117-1. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
|
16 | Catia M. Angelo, Luc J. M. Claesen, Hugo De Man |
Modeling Multi-rate DSP Specification Semantics for Formal Transformational Design in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Methods Syst. Des. ![In: Formal Methods Syst. Des. 5(1/2), pp. 61-94, 1994. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
16 | John Harrison 0001 |
Constructing the Real Numbers in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Methods Syst. Des. ![In: Formal Methods Syst. Des. 5(1/2), pp. 35-59, 1994. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
16 | Thomas F. Melham |
A Mechanized Theory of the Pi-Calculus in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Nord. J. Comput. ![In: Nord. J. Comput. 1(1), pp. 50-76, 1994. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP BibTeX RDF |
|
16 | Graham Hutton |
Book Review: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic by Mike Gordon and Tom Melham (eds.), Cambridge University Press, 1993, ISBN 0-521-44189-7. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Funct. Program. ![In: J. Funct. Program. 4(4), pp. 557-559, 1994. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
16 | Thomas Forster |
Weak Systems of Set Theory Related to HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, Valletta, Malta, September 19-22, 1994, Proceedings, pp. 193-204, 1994, Springer, 3-540-58450-1. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
16 | Jean-Paul Bodeveix, Mamoun Filali, P. Roche |
Towards a HOL Theory and Memory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, Valletta, Malta, September 19-22, 1994, Proceedings, pp. 49-64, 1994, Springer, 3-540-58450-1. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
16 | Tobias Nipkow, Konrad Slind |
I/Q Automata in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop TYPES'94, Båstad, Sweden, June 6-10, 1994, Selected Papers, pp. 101-119, 1994, Springer, 3-540-60579-7. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
16 | Jonathan P. Bowen, Michael J. C. Gordon |
Z and HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Z User Workshop ![In: Z User Workshop, Cambridge, UK, 29-30 June 1994, Proceedings, pp. 141-167, 1994, Springer/BCS, 3-540-19884-9. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
16 | Franz Regensburger |
HOLCF: eine konservative Erweiterung von HOL um LCF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
1994 |
RDF |
|
16 | Catia M. Angelo, Diederik Verkest, Luc J. M. Claesen, Hugo De Man |
On the Comparison of HOL and Boyer-Moore for Formal Hardware Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Methods Syst. Des. ![In: Formal Methods Syst. Des. 2(1), pp. 45-72, 1993. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
16 | Roger Hale, Rachel Cardell-Oliver, John Herbert |
An Embedding of Timed Transition Systems in HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Methods Syst. Des. ![In: Formal Methods Syst. Des. 3(1/2), pp. 151-174, 1993. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
16 | Thomas F. Melham |
The HOL Logic Extended with Quantification over Type Variables. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Methods Syst. Des. ![In: Formal Methods Syst. Des. 3(1/2), pp. 7-24, 1993. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
16 | John Harrison 0001, Laurent Théry |
Reasoning About the Reals: The Marriage of HOL and Maple. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic Programming and Automated Reasoning,4th International Conference, LPAR'93, St. Petersburg, Russia, July 13-20, 1993, Proceedings, pp. 351-353, 1993, Springer, 3-540-56944-8. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
16 | Luc J. M. Claesen, Michael J. C. Gordon (eds.) |
Higher Order Logic Theorem Proving and its Applications, Proceedings of the IFIP TC10/WG10.2 Workshop HOL'92, Leuven, Belgium, 21-24 September 1992 ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![North-Holland/Elsevier, 0-444-89880-8 The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP BibTeX RDF |
|