BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Used together with:
isabell (20)
formal (9)
test (8)
use (8)
proof (6)

Stem hol$ (all stems)

46 papers:

CADECADE-2015-MaricJM #correctness #higher-order #proving #using
Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3 (FM, PJ, MM), pp. 256–271.
SEFMSEFM-2014-ArmstrongGS #higher-order #lightweight #tool support #verification
Lightweight Program Construction and Verification Tools in Isabelle/HOL (AA, VBFG, GS), pp. 5–19.
DATEDATE-2013-HasanA #analysis #fault #feedback #formal method #using
Formal analysis of steady state errors in feedback control systems using HOL-light (OH, MA), pp. 1423–1426.
CADECADE-2013-KaliszykU #named #proving #re-engineering
PRocH: Proof Reconstruction for HOL Light (CK, JU), pp. 267–274.
SACSAC-2011-KaliszykU #higher-order
Quotients revisited for Isabelle/HOL (CK, CU), pp. 1639–1644.
SACSAC-2010-VermolenHL #consistency #modelling #proving #using
Proving consistency of VDM models using HOL (SV, JH, PGL), pp. 2503–2510.
PLEASEPLEASE-2010-KammullerRR #higher-order #variability
Feature link propagation across variability representations with Isabelle/HOL (FK, AR, MOR), pp. 48–53.
CSLCSL-2010-BarthwalN #context-free grammar #formal method #normalisation
A Formalisation of the Normal Forms of Context-Free Grammars in HOL4 (AB, MN), pp. 95–109.
FASEFASE-2009-BruckerW #higher-order
hol-TestGen (ADB, BW), pp. 417–420.
PPDPPPDP-2009-KaiserL #higher-order #traversal
An Isabelle/HOL-based model of stratego-like traversal strategies (MK, RL), pp. 93–104.
FASEFASE-2008-BruckerW #higher-order #named #ocl #proving #uml
HOL-OCL: A Formal Proof Environment for UML/OCL (ADB, BW), pp. 97–100.
SACSAC-2008-AbedMS #analysis #graph #multi #proving #reachability #theorem proving #using
Reachability analysis using multiway decision graphs in the HOL theorem prover (SA, OAM, GAS), pp. 333–338.
IFMIFM-2007-HasanT #cumulative #probability #using #verification
Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function (OH, ST), pp. 333–352.
TAPTAP-2007-BruckerW #generative #higher-order #testing
Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing (ADB, BW), pp. 149–168.
POPLPOPL-2006-BishopFNSSW #implementation #logic #specification #testing
Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations (SB, MF, MN, PS, MS, KW), pp. 55–66.
IJCARIJCAR-2006-ConstableM #proving #semantics #source code
Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics (RLC, WM), pp. 162–176.
IJCARIJCAR-2006-Harrison #self #towards
Towards Self-verification of HOL Light (JH), pp. 177–191.
IJCARIJCAR-2006-McLaughlin #higher-order
An Interpretation of Isabelle/HOL in HOL Light (SM), pp. 192–204.
IJCARIJCAR-2006-ObuaS #higher-order
Importing HOL into Isabelle/HOL (SO, SS), pp. 298–302.
IJCARIJCAR-2006-UrbanB #combinator #data type #higher-order #recursion
A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL (CU, SB), pp. 498–512.
FASEFASE-2005-HausmannMS #higher-order #induction
Iterative Circular Coinduction for CoCasl in Isabelle/HOL (DH, TM, LS), pp. 341–356.
FMFM-2005-BasinKTW #architecture #verification
Verification of a Signature Architecture with HOL-Z (DAB, HK, KT, BW), pp. 269–285.
SEFMSEFM-2005-BlechGG #higher-order #verification
Formal Verification of Dead Code Elimination in Isabelle/HOL (JOB, LG, SG), pp. 200–209.
QAPLQAPL-2004-HurdMM05 #probability
Probabilistic Guarded Commands Mechanized in HOL (JH, AM, CM), pp. 95–111.
COCVCOCV-J-2005-BlechGLM #code generation #comparison #correctness #higher-order #optimisation #proving
Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL (JOB, SG, JL, SM), pp. 33–51.
CADECADE-2005-UrbanT #higher-order
Nominal Techniques in Isabelle/HOL (CU, CT), pp. 38–53.
FATESFATES-2005-BruckerW #higher-order #interactive #testing
Interactive Testing with HOL-TestGen (ADB, BW), pp. 87–102.
SEFMSEFM-2004-BerghoferN #higher-order #random testing #testing
Random Testing in Isabelle/HOL (SB, TN), pp. 230–239.
IJCARIJCAR-2004-AvigadD #formal method #higher-order
Formalizing O Notation in Isabelle/HOL (JA, KD), pp. 357–371.
ESOPESOP-2003-Nieto #higher-order
The Rely-Guarantee Method in Isabelle/HOL (LPN), pp. 348–362.
IFMIFM-2002-AkbarpourDT #fixpoint #formal method
Formalization of Cadence SPW Fixed-Point Arithmetic in HOL (BA, AD, ST), pp. 185–204.
IFMIFM-2002-XiongCTB
Formally Linking MDG and HOL Based on a Verified MDG System (HX, PC, ST, AB), pp. 205–224.
UMLUML-2002-BruckerW #case study #design #experience #higher-order #named #ocl
HOL-OCL: Experiences, Consequences and Design Choices (ADB, BW), pp. 196–211.
CADECADE-2002-Hurd #first-order #interface #logic
An LCF-Style Interface between HOL and First-Order Logic (JH), pp. 134–138.
FoSSaCSFoSSaCS-2001-RocklHB #formal method #higher-order #induction #syntax #π-calculus
Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the π-Calculus and Mechanizing the Theory of Contexts (CR, DH, SB), pp. 364–378.
FASEFASE-1999-NipkowN #higher-order
Owicki/Gries in Isabelle/HOL (TN, LPN), pp. 188–203.
TACASTACAS-1999-Pusch #bytecode #higher-order #java #proving #specification #verification
Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL (CP), pp. 89–103.
RTARTA-1999-DowekHK #first-order #higher-order #logic #named
HOL-λσ: An Intentional First-Order Expression of Higher-Order Logic (GD, TH, CK), pp. 317–331.
CADECADE-1998-SlindGBB #interface
System Description: An Interface Between CLAM and HOL (KS, MJCG, RJB, AB), pp. 134–138.
FMFME-1997-TejW #csp #higher-order
A Corrected Failure Divergence Model for CSP in Isabelle/HOL (HT, BW), pp. 318–337.
CADECADE-1997-FeltyH #hybrid #interactive #proving #theorem proving #using
Hybrid Interactive Theorem Proving Using Nuprl and HOL (APF, DJH), pp. 351–365.
CADECADE-1996-Nipkow #higher-order #proving
More Church-Rosser Proofs (in Isabelle/HOL) (TN), pp. 733–747.
CADECADE-1992-Blackburn
A Report in ICL HOL (KB), pp. 743–747.
CAVCAV-1991-Mutz #behaviour #correctness #proving #term rewriting #using
Using the HOL Prove Assistant for proving the Correctness of term Rewriting Rules reducing Terms of Sequential Behavior (MM), pp. 277–287.
CAVCAV-1991-SchneiderKK #automation #hardware #proving
Automating Most Parts of Hardware Proofs in HOL (KS, RK, TK), pp. 365–375.
CAVCAV-1991-SegerJ #using #verification
A Two-Level Formal Verification Methodology using HOL and COSMOS (CJHS, JJJ), pp. 299–309.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.