Search results for "HOL theorem prover"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
2	Sa'ed Abed, Otmane Aït Mohamed	MDGs Reduction Technique Based on the HOL Theorem Prover.	ISMVL	2010	DBLP DOI BibTeX RDF	Soundness, Reduction Techniques, Multiway Decision Graphs, HOL Theorem Prover
2	Osman Hasan, Sofiène Tahar	Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Real-time systems, Communication protocols, Higher-order-logic, Probability theory, HOL theorem prover
2	Sa'ed Abed, Otmane Aït Mohamed, Ghiath Al Sammane	An Abstract Reachability Approach by Combining HOL Induction and Multiway Decision Graphs.	J. Comput. Sci. Technol.	2009	DBLP DOI BibTeX RDF	correctness, reachability analysis, multiway decision graphs, HOL theorem prover
2	Sa'ed Abed, Otmane Aït Mohamed, Ghiath Al Sammane	Reachability analysis using multiway decision graphs in the HOL theorem prover.	SAC	2008	DBLP DOI BibTeX RDF	reachability analysis, HOL, multiway decision graphs
2	Osman Hasan, Sofiène Tahar	Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Coupon collector’s problem, Probabilistic analysis, Higher-order-logic, Probability theory, Statistical properties, HOL theorem prover
2	Ramayya Kumar, Thomas Kropf, Klaus Schneider	Formal synthesis of circuits with a simple handshake protocol.	VLSI Design	1995	DBLP DOI BibTeX RDF	formal circuit synthesis, preproven building blocks, higher-order temporal operators, parametrized data signals, sequentially composed modules, parallel module composition, protocols, high level synthesis, logic design, operator semantics, template, formal logic, correctness proofs, synchronous circuits, handshake protocol, HOL theorem prover
1	Tjark Weber	SMT solvers: new oracles for the HOL theorem prover.	STTT	2011	DBLP DOI BibTeX RDF
1	Moritz Kleine, Björn Bartels, Thomas Göthel, Sabine Glesner	Verifying the Implementation of an Operating System Scheduler.	TASE	2009	DBLP DOI BibTeX RDF
1	Peter V. Homeier	The HOL-Omega Logic.	TPHOLs	2009	DBLP DOI BibTeX RDF
1	Thomas Tuerk	A Formalisation of Smallfoot in HOL.	TPHOLs	2009	DBLP DOI BibTeX RDF
1	Harvey Tuch	Formal Verification of C Systems Code.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	C, Separation logic, Interactive theorem proving
1	Sa'ed Abed, Otmane Aït Mohamed, Ghiath Al Sammane	The Performance of Combining Multiway Decision Graphs and HOL Theorem Prover.	FDL	2008	DBLP DOI BibTeX RDF
1	Sergey Tverdyshev, Eyad Alkassar	Efficient Bit-Level Model Reductions for Automated Hardware Verification.	TIME	2008	DBLP DOI BibTeX RDF
1	Guodong Li, Konrad Slind	Trusted Source Translation of a Total Function Language.	TACAS	2008	DBLP DOI BibTeX RDF
1	Rafal Kolanski, Gerwin Klein	Mapped Separation Logic.	VSTTE	2008	DBLP DOI BibTeX RDF
1	Julien Schmaltz	A Formal Model of Clock Domain Crossing and Automated Verification of Time-Triggered Hardware.	FMCAD	2007	DBLP DOI BibTeX RDF
1	Osman Hasan, Sofiène Tahar	Formalization of Continuous Probability Distributions.	CADE	2007	DBLP DOI BibTeX RDF
1	Osman Hasan, Sofiène Tahar	Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function.	IFM	2007	DBLP DOI BibTeX RDF	Higher-Order-Logic, Interactive Theorem Proving, HOL, Probabilistic Systems, Cumulative Distribution Function
1	Jeremy E. Dawson	Formalising Generalised Substitutions.	TPHOLs	2007	DBLP DOI BibTeX RDF	general correctness, generalised substitution
1	Osman Hasan, Sofiène Tahar	Verification of Expectation Properties for Discrete Random Variables in HOL.	TPHOLs	2007	DBLP DOI BibTeX RDF
1	Behzad Akbarpour, Sofiène Tahar	An approach for the formal verification of DSP designs using Theorem proving.	IEEE Trans. on CAD of Integrated Circuits and Systems	2006	DBLP DOI BibTeX RDF
1	Thomas Tuerk, Klaus Schneider, Mike Gordon	Model Checking PSL Using HOL and SMV.	Haifa Verification Conference	2006	DBLP DOI BibTeX RDF
1	Orieta Celiku	Quantitative Temporal Logic Mechanized in HOL.	ICTAC	2005	DBLP DOI BibTeX RDF
1	Thumrongsak Kosiyatrakul, Susan Older, Shiu-Kai Chin	A Modal Logic for Role-Based Access Control.	MMM-ACNS	2005	DBLP DOI BibTeX RDF
1	Thomas Tuerk, Klaus Schneider	From PSL to LTL: A Formal Validation in HOL.	TPHOLs	2005	DBLP DOI BibTeX RDF
1	Morten P. Lindegaard, Anne Elisabeth Haxthausen	Proof Support for RAISE by a Reuse Approach Based on Institutions.	AMAST	2004	DBLP DOI BibTeX RDF	proof support, Institutions, algebraic semantics, HOL, RSL
1	Tarek Mhamdi, Sofiène Tahar	Providing Automated Verification in HOL Using MDGs.	ATVA	2004	DBLP DOI BibTeX RDF
1	Behzad Akbarpour, Sofiène Tahar	A Methodology for the Formal Verification of FFT Algorithms in HOL.	FMCAD	2004	DBLP DOI BibTeX RDF
1	Juan Carlos López Pimentel, Raul Monroy	A Rippling-Based Difference Reduction Technique to Automatically Prove Security Protocol Goals.	IBERAMIA	2004	DBLP DOI BibTeX RDF
1	Behzad Akbarpour, Sofiène Tahar	Error Analysis of Digital Filters Using Theorem Proving.	TPHOLs	2004	DBLP DOI BibTeX RDF
1	Ali Habibi, Sofiène Tahar, Adel Ghazel	Formal Verification of a DSP Chip Using an Iterative Approach.	DSD	2002	DBLP DOI BibTeX RDF
1	Keith Wansbrough, Michael Norrish, Peter Sewell, Andrei Serjantov	Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures.	ESOP	2002	DBLP DOI BibTeX RDF
1	Richard J. Boulton, Konrad Slind	Automatic Derivation and Application of Induction Schemes for Mutually Recursive Functions.	Computational Logic	2000	DBLP DOI BibTeX RDF
1	Sae Hwan Kim, Shiu-Kai Chin	Formal Verification of Tree-Structured Carry-Lookahead Adders.	Great Lakes Symposium on VLSI	1999	DBLP DOI BibTeX RDF
1	Christine Röckl, Javier Esparza	Proof-Checking Protocols Using Bisimulations.	CONCUR	1999	DBLP DOI BibTeX RDF
1	Dan Zhou, Shiu-Kai Chin	Formal Analysis of a Secure Communication Channel: Secure Core-Email Protocol.	World Congress on Formal Methods	1999	DBLP DOI BibTeX RDF
1	Klaus Schneider, Dirk W. Hoffmann	A HOL Conversion for Translating Linear Time Temporal Logic to omega-Automata.	TPHOLs	1999	DBLP DOI BibTeX RDF
1	Annette Bunker, Trent N. Larson, Michael D. Jones, Phillip J. Windley	Alexandria: A Tool for Hierarchical Verification.	FMCAD	1998	DBLP DOI BibTeX RDF
1	Richard J. Boulton	Generating Embeddings from Denotational Descriptions.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Peter V. Homeier, David F. Martin	Mechanical Verification of Total Correctness through Diversion Verification Conditions.	TPHOLs	1998	DBLP DOI BibTeX RDF
1	Shiu-Kai Chin, John Faust, Joseph Giordano	Formal Methods Applied to Secure Network Engineering.	ICECCS	1996	DBLP DOI BibTeX RDF
1	Anand Chavan, Shiu-Kai Chin, Shahid Ikram, Jang Dae Kim, Juin-Yeu Zu	Extending VLSI design with higher-order logic. (PDF / PS)	ICCD	1995	DBLP DOI BibTeX RDF	Cambridge Higher-Order Logic theorem-prover, microprogram sequencer, Am2910, VLSI, formal verification, formal verification, logic testing, theorem proving, logic design, logic CAD, VLSI design, higher-order logic, theorem-prover, design environment, instruction-set architecture, VLSI CAD
1	Paul Loewenstein	Formal Verification of Counterflow Pipeline Architecture.	TPHOLs	1995	DBLP DOI BibTeX RDF
1	Thomas Långbacka	A HOL Formalisation of the Temporal Logic of Actions.	TPHOLs	1994	DBLP DOI BibTeX RDF
1	Savi Maharaj, Elsa L. Gunter	Studying the ML Module System in Hol.	TPHOLs	1994	DBLP DOI BibTeX RDF
1	John Harrison, Laurent Théry	Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals.	HUG	1993	DBLP DOI BibTeX RDF
1	Jeffrey J. Joyce, Carl-Johan H. Seger	The HOL-Voss System: Model-Checking inside a General-Purpose Theorem-Prover.	HUG	1993	DBLP DOI BibTeX RDF
1	Sreeranga P. Rajan, Jeffrey J. Joyce, Carl-Johan H. Seger	From Abstract Data Types to Shift Registers: A Case Study in Formal Specification and Verification at Differing Levels of Abstraction using Theorem Proving and Symbolic Simulation.	HUG	1993	DBLP DOI BibTeX RDF
1	Wai Wong	Modelling Bit Vectors in HOL: the word library.	HUG	1993	DBLP DOI BibTeX RDF
1	Monica Nesi	Formalizing a Modal Logic for CSS in the HOL Theorem Prover.	TPHOLs	1992	DBLP BibTeX RDF
1	Shiu-Kai Chin	Verified functions for generating signed-binary arithmetic hardware.	IEEE Trans. on CAD of Integrated Circuits and Systems	1992	DBLP DOI BibTeX RDF
1	Joakim von Wright, Thomas Långbacka	Using a Theorem Prover for Reasoning about Concurrent Algorithms.	CAV	1992	DBLP DOI BibTeX RDF
1	Paul Loewenstein	Reasoning about State Machines in Higher-Order Logic.	Hardware Specification, Verification and Synthesis	1989	DBLP DOI BibTeX RDF