Search results for "HOL"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
16	Stephen H. Brackin, Shiu-Kai Chin	Server-Process Restrictiveness in HOL.	HUG	1993	DBLP DOI BibTeX RDF
16	Catia M. Angelo, Luc J. M. Claesen, Hugo De Man	Degrees of Formality in Shallow Embedding Hardware Description Languages in HOL.	HUG	1993	DBLP DOI BibTeX RDF
16	John Harrison 0001, Laurent Théry	Extending the HOL Theorem Prover with a Computer Algebra System to Reason about the Reals.	HUG	1993	DBLP DOI BibTeX RDF
16	John Van Tassel	Femto-VHDL : the semantics of a subset of VHDL and its embedding in the HOL proof assistant.		1993	RDF
16	Myla Archer, Jeffrey J. Joyce, Karl N. Levitt, Phillip J. Windley (eds.)	Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, August 1991, Davis, California, USA	TPHOLs	1992	DBLP BibTeX RDF
16	Richard J. Boulton, Andrew D. Gordon 0001, Michael J. C. Gordon, John Harrison 0001, John Herbert, John Van Tassel	Experience with Embedding Hardware Description Languages in HOL.	TPCD	1992	DBLP BibTeX RDF
16	Joakim von Wright, Jukka Hekanaho, P. Luostarinen, Thomas Långbacka	Mechanising some Advanced Refinement Concepts.	TPHOLs	1992	DBLP BibTeX RDF
16	Paul Loewenstein	A Formal Theory of Simulations Between Infinite Automata.	TPHOLs	1992	DBLP BibTeX RDF
16	Jing Pan, Karl N. Levitt, Myla Archer, Saraswati Kalvala	Towards a Formal Verification of a Floating Point Coprocessor and its Composition with a Central Processing Unit.	TPHOLs	1992	DBLP BibTeX RDF
16	Konrad Slind	Adding New Rules to an LCF-style Logic Implementation.	TPHOLs	1992	DBLP BibTeX RDF
16	Holger Busch	Unification Based Induction.	TPHOLs	1992	DBLP BibTeX RDF
16	Garrel Pottinger	A Classical Type Theory with Transfinite Types.	TPHOLs	1992	DBLP BibTeX RDF
16	Kees G. W. Goossens	Operational Semantics Based on Formal Symbolic Simulation.	TPHOLs	1992	DBLP BibTeX RDF
16	Richard J. Boulton	A Lazy Approach to Fully-Expansive Theorem Proving.	TPHOLs	1992	DBLP BibTeX RDF
16	Li-Guo Wang	Deriving a Correct Computer.	TPHOLs	1992	DBLP BibTeX RDF
16	Massimo Bombana, Patrizia Cavalloro, Giuseppe Zaza	Specification and Formal Synthesis of Digital Circuits.	TPHOLs	1992	DBLP BibTeX RDF
16	Nancy A. Day	A Comparison between Statecharts and State Transition Assertions.	TPHOLs	1992	DBLP BibTeX RDF
16	Ching-Tsun Chou	A Note on Interactive Theorem Proving with Theorem Continuation Functions.	TPHOLs	1992	DBLP BibTeX RDF
16	Klaus Schneider 0001, Ramayya Kumar, Thomas Kropf	Efficient Representation and Computation of Tableau Proofs.	TPHOLs	1992	DBLP BibTeX RDF
16	Mark D. Aagaard, Miriam Leeser	A Methodology for Reusable Hardware Proofs.	TPHOLs	1992	DBLP BibTeX RDF
16	Roger B. Hughes, M. D. Francis, Simon Finn, Gerry Musgrave	Formal Tools in Tri-State Design in Busses.	TPHOLs	1992	DBLP BibTeX RDF
16	Kelly M. Hall, Phillip J. Windley	Simulating Microprocessors from Formal Specifications.	TPHOLs	1992	DBLP BibTeX RDF
16	Michael McAllister	Machine Abstraction in Microprocessor Specification.	TPHOLs	1992	DBLP BibTeX RDF
16	Roger B. Hughes, Gerry Musgrave	Design-Flow Graph Partitioning.	TPHOLs	1992	DBLP BibTeX RDF
16	Paul Curzon	Deriving Correctness Properties of Compiled Code.	TPHOLs	1992	DBLP BibTeX RDF
16	Klaus Schneider 0001, Ramayya Kumar, Thomas Kropf	Modelling Generic Hardware Structures by Abstract Datatypes.	TPHOLs	1992	DBLP BibTeX RDF
16	John Van Tassel	A Formalisation of the VHDL Simulation Cycle.	TPHOLs	1992	DBLP BibTeX RDF
16	Klaus Schneider 0001, Ramayya Kumar, Thomas Kropf	Automating Most Parts of Hardware Proofs in HOL.	CAV	1991	DBLP DOI BibTeX RDF
16	Carl-Johan H. Seger, Jeffrey J. Joyce	A Two-Level Formal Verification Methodology using HOL and COSMOS.	CAV	1991	DBLP DOI BibTeX RDF
16	Per F. V. Hasle	Building a Temporal Logic for Natural Language Understanding with the HOL-system.	Natural Language Understanding and Logic Programming Workshop	1991	DBLP BibTeX RDF
16	E. Thomas Schubert	Verification of Composed Hardware Systems Using CCS.	TPHOLs	1991	DBLP BibTeX RDF
16	Paul Curzon	A Verified Compiler for a Structured Assembly Language.	TPHOLs	1991	DBLP BibTeX RDF
16	Roger Hale	Reasoning About Software.	TPHOLs	1991	DBLP BibTeX RDF
16	Shiu-Kai Chin, Graham M. Birtwistle	Implementing and Verifying Finite-State Machines Using Types in Higher-Order Logic.	TPHOLs	1991	DBLP BibTeX RDF
16	Jim Alves-Foss, Karl N. Levitt	Mechanical Verification of Secure Distributed Systems in Higher Order Logic.	TPHOLs	1991	DBLP BibTeX RDF
16	John Herbert	Dealing With Temporal Complexity in Hardware Verification.	TPHOLs	1991	DBLP BibTeX RDF
16	W. Wong	A Simple Graph Theory and Its Application in Railway Signalling.	TPHOLs	1991	DBLP BibTeX RDF
16	Rachel E. O. Roxas, Malcolm C. Newey	Proof of Program Transformations.	TPHOLs	1991	DBLP BibTeX RDF
16	E. Thomas Schubert	Verification of Integrated Subsystems.	TPHOLs	1991	DBLP BibTeX RDF
16	X. Wang, Edward P. Stabler	Formalization of VHDL Synthesis Procedure in Higher-Order Logic.	TPHOLs	1991	DBLP BibTeX RDF
16	Matt Kaufmann	An Informal Discussion of Issues in Mechanically-Assisted Reasoning.	TPHOLs	1991	DBLP BibTeX RDF
16	Phillip J. Windley	The Practical Verification of Microprocessor Designs.	TPHOLs	1991	DBLP BibTeX RDF
16	Simon Bainbridge, Albert John Camilleri, Roger Fleming	Industrial Application of Theorem Proving to System Level Design.	TPHOLs	1991	DBLP BibTeX RDF
16	Malcolm C. Newey	Proof Based Computation.	TPHOLs	1991	DBLP BibTeX RDF
16	John M. Rushby	Design Choices in Specification Languages and Verification Systems.	TPHOLs	1991	DBLP BibTeX RDF
16	Kurt Keutzer	The Need for Formal Verification in Hardware Design and What Formal Verification Has Not Done for Me Lately.	TPHOLs	1991	DBLP BibTeX RDF
16	Shiu-Kai Chin	Verifying Arithmetic Hardware in Higher-Order Logic.	TPHOLs	1991	DBLP BibTeX RDF
16	Albert John Camilleri	Reasoning in CSP via the HOL theorem prover.	Jerusalem Conference on Information Technology	1990	DBLP DOI BibTeX RDF
16	John E. Gaffney Jr.	The Impact on Software Development Costs of Using HOL's.	IEEE Trans. Software Eng.	1986	DBLP DOI BibTeX RDF
16	Harold W. Noffke	HOL-to-Microcode Compilers: An Air Force Perspective.	ER	1983	DBLP BibTeX RDF
16	William C. Nielsen	Design of an aerospace computer for direct HOL execution.	HLLCA	1973	DBLP DOI BibTeX RDF
10	Wihem Arsac, Luca Compagna, Samuel Paul Kaluvuri, Serena Elisa Ponta	Security validation tool for business processes.	SACMAT	2011	DBLP DOI BibTeX RDF
10	Achim D. Brucker, Burkhart Wolff	Semantics, calculi, and analysis for object-oriented specifications.	Acta Informatica	2009	DBLP DOI BibTeX RDF
10	Pan Li 0001, Hongqiang Zhai, Yuguang Fang	SDMAC: Selectively Directional MAC protocol for wireless mobile ad hoc networks.	Wirel. Networks	2009	DBLP DOI BibTeX RDF	MAC protocol, Directional antennas, Wireless mobile ad hoc networks
10	Jasmin Christian Blanchette	Proof Pearl: Mechanizing the Textbook Proof of Huffman's Algorithm.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Interactive theorem provers, Huffman coding, Higher-order logic
10	Harvey Tuch	Formal Verification of C Systems Code.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	C, Separation logic, Interactive theorem proving
10	Stefan Berghofer, Markus Reiter	Formalizing the Logic-Automaton Connection.	TPHOLs	2009	DBLP DOI BibTeX RDF
10	David A. Basin, Srdjan Capkun, Patrick Schaller, Benedikt Schmidt 0002	Let's Get Physical: Models and Methods for Real-World Security Protocols.	TPHOLs	2009	DBLP DOI BibTeX RDF
10	Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David A. Cock, Michael Norrish	Mind the Gap.	TPHOLs	2009	DBLP DOI BibTeX RDF
10	René Thiemann, Christian Sternagel	Certification of Termination Proofs Using CeTA.	TPHOLs	2009	DBLP DOI BibTeX RDF
10	Christoph Lüth, Dennis Walter	Certifiable Specification and Verification of C Programs.	FM	2009	DBLP DOI BibTeX RDF
10	Jade Alglave, Anthony C. J. Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli	The semantics of power and ARM multiprocessor machine code.	DAMP	2009	DBLP DOI BibTeX RDF	semantics, powerpc, arm, relaxed memory models
10	Levent Erkök, John Matthews	Pragmatic equivalence and safety checking in Cryptol.	PLPV	2009	DBLP DOI BibTeX RDF	sat/smt solving, size polymorphism, formal methods, cryptography, theorem proving, equivalence checking
10	Aditi Barthwal, Michael Norrish	Verified, Executable Parsing.	ESOP	2009	DBLP DOI BibTeX RDF
10	Javier de Dios, Ricardo Peña-Marí	A Certified Implementation on Top of the Java Virtual Machine.	FMICS	2009	DBLP DOI BibTeX RDF
10	Daniel Wasserrab, Denis Lohner, Gregor Snelting	On PDG-based noninterference and its modular proof.	PLAS	2009	DBLP DOI BibTeX RDF	modularity, program slicing, noninterference, correctness proof, program dependence graph
10	Miguel Alexandre Ferreira, José Nuno Oliveira	An Integrated Formal Methods Tool-Chain and Its Application to Verifying a File System Model.	SBMF	2009	DBLP DOI BibTeX RDF
10	Moritz Kleine, Björn Bartels, Thomas Göthel, Sabine Glesner	Verifying the Implementation of an Operating System Scheduler.	TASE	2009	DBLP DOI BibTeX RDF
10	Yun Han Bae, Kyung Jae Kim, Mi-Nam Moon, Bong Dae Choi	Analysis of IEEE 802.11 non-saturated DCF by matrix analytic methods.	Ann. Oper. Res.	2008	DBLP DOI BibTeX RDF
10	Paul Beekhuizen, Dee Denteneer, Jacques Resing	Reduction of a polling network to a single node.	Queueing Syst. Theory Appl.	2008	DBLP DOI BibTeX RDF	Mathematics Subject Classification (2000) 60K25, 90B15
10	Amine Chaieb, Tobias Nipkow	Proof Synthesis and Reflection for Linear Arithmetic.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Proof synthesis, Linear arithmetic, Reflection
10	Walenty Oniszczuk	An Intelligent Service Strategy in Linked Networks with Blocking and Feedback.	New Challenges in Applied Intelligence Technologies	2008	DBLP DOI BibTeX RDF	intelligent service strategy, network performance analysis, feedback and blocking, Markov chain
10	Eyad Alkassar, Mark A. Hillebrand	Formal Functional Verification of Device Drivers.	VSTTE	2008	DBLP DOI BibTeX RDF
10	Rafal Kolanski, Gerwin Klein	Mapped Separation Logic.	VSTTE	2008	DBLP DOI BibTeX RDF
10	Dhammika Elkaduwe, Gerwin Klein, Kevin Elphinstone	Verified Protection Model of the seL4 Microkernel.	VSTTE	2008	DBLP DOI BibTeX RDF
10	Michael Backes 0001, Matthias Berg, Dominique Unruh	A Formal Language for Cryptographic Pseudocode.	LPAR	2008	DBLP DOI BibTeX RDF
10	Stefan Berghofer, Christian Urban	Nominal Inversion Principles.	TPHOLs	2008	DBLP DOI BibTeX RDF
10	David A. Cock, Gerwin Klein, Thomas Sewell	Secure Microkernels, State Monads and Scalable Refinement.	TPHOLs	2008	DBLP DOI BibTeX RDF
10	Achim D. Brucker, Lukas Brügger, Burkhart Wolff	Model-Based Firewall Conformance Testing.	TestCom/FATES	2008	DBLP DOI BibTeX RDF	Model-based Testing, Firewall, Conformance Testing, Security Testing
10	Christoph Sprenger 0001, David A. Basin	Cryptographically-Sound Protocol-Model Abstractions.	CSF	2008	DBLP DOI BibTeX RDF	cryptographic soundness, formal methods, theorem proving, Cryptographic protocols, simulatability
10	Christian Urban, James Cheney, Stefan Berghofer	Mechanizing the Metatheory of LF.	LICS	2008	DBLP DOI BibTeX RDF	mechanized metatheory, logical frameworks, nominal logic
10	Ran Raz	A Counterexample to Strong Parallel Repetition.	FOCS	2008	DBLP DOI BibTeX RDF
10	Scott Owens	A Sound Semantics for OCamllight.	ESOP	2008	DBLP DOI BibTeX RDF
10	Cezary Kaliszyk, Freek Wiedijk	Merging Procedural and Declarative Proof.	TYPES	2008	DBLP DOI BibTeX RDF
10	Tom Maertens, Joris Walraevens, Herwig Bruneel	Performance Evaluation of a Gradual Differentiation Scheme for Telecommunication Networks.	ASMTA	2008	DBLP DOI BibTeX RDF
10	Bo Zhang	Specifying and Verifying Timing Properties of a Time-triggered Protocol for In-vehicle Communication.	SNPD	2008	DBLP DOI BibTeX RDF
10	Florian Kammüller, Henry Sudhof	Composing Safely - A Type System for Aspects.	SC@ETAPS	2008	DBLP DOI BibTeX RDF
10	Eyad Alkassar, Peter Böhm, Steffen Knapp	Formal Correctness of an Automotive Bus Controller Implementation at Gate-Level.	DIPES	2008	DBLP DOI BibTeX RDF
10	Sergey Tverdyshev, Eyad Alkassar	Efficient Bit-Level Model Reductions for Automated Hardware Verification.	TIME	2008	DBLP DOI BibTeX RDF
10	Christian Urban, Bozhi Zhu	Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof.	RTA	2008	DBLP DOI BibTeX RDF
10	Temesghen Kahsai, Marino Miculan	Implementing Spi Calculus Using Nominal Techniques.	CiE	2008	DBLP DOI BibTeX RDF
10	Cezary Kaliszyk	Automating Side Conditions in Formalized Partial Functions.	AISC/MKM/Calculemus	2008	DBLP DOI BibTeX RDF
10	Ming-che Lai, Lei Gao, Wei Shi, Zhiying Wang 0003	Escaping from Blocking: A Dynamic Virtual Channel for Pipelined Routers.	CISIS	2008	DBLP DOI BibTeX RDF
10	Bo Zhang	Formal Analysis of a Distributed Fault Tolerant Clock Synchronization Algorithm for Automotive Communication Systems.	EUROMICRO-SEAA	2008	DBLP DOI BibTeX RDF
10	Joan-Lluís Ferrer, Elvira Baydal, Antonio Robles, Pedro López 0001, José Duato	Congestion Management in MINs through Marked and Validated Packets.	PDP	2007	DBLP DOI BibTeX RDF
10	Vaidas Gasiunas, Mira Mezini, Klaus Ostermann	Dependent classes.	OOPSLA	2007	DBLP DOI BibTeX RDF	dependent classes, variability, dynamic dispatch, multimethods, multiple dispatch, virtual classes
10	John Harrison 0001	Verifying Nonlinear Real Formulas Via Sums of Squares.	TPHOLs	2007	DBLP DOI BibTeX RDF
10	Makarius Wenzel, Burkhart Wolff	Building Formal Method Tools in the Isabelle/Isar Framework.	TPHOLs	2007	DBLP DOI BibTeX RDF
10	Jeremy E. Dawson	Formalising Generalised Substitutions.	TPHOLs	2007	DBLP DOI BibTeX RDF	general correctness, generalised substitution
10	Matt Kaufmann, Konrad Slind	Proof Pearl: Wellfounded Induction on the Ordinals Up to epsilon 0.	TPHOLs	2007	DBLP DOI BibTeX RDF