46 papers:
CADE-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.
SEFM-2014-ArmstrongGS #higher-order #lightweight #tool support #verification- Lightweight Program Construction and Verification Tools in Isabelle/HOL (AA, VBFG, GS), pp. 5–19.
DATE-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.
- CADE-2013-KaliszykU #named #proving #re-engineering
- PRocH: Proof Reconstruction for HOL Light (CK, JU), pp. 267–274.
SAC-2011-KaliszykU #higher-order- Quotients revisited for Isabelle/HOL (CK, CU), pp. 1639–1644.
- SAC-2010-VermolenHL #consistency #modelling #proving #using
- Proving consistency of VDM models using HOL (SV, JH, PGL), pp. 2503–2510.
PLEASE-2010-KammullerRR #higher-order #variability- Feature link propagation across variability representations with Isabelle/HOL (FK, AR, MOR), pp. 48–53.
CSL-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.
FASE-2009-BruckerW #higher-order- hol-TestGen (ADB, BW), pp. 417–420.
PPDP-2009-KaiserL #higher-order #traversal- An Isabelle/HOL-based model of stratego-like traversal strategies (MK, RL), pp. 93–104.
- FASE-2008-BruckerW #higher-order #named #ocl #proving #uml
- HOL-OCL: A Formal Proof Environment for UML/OCL (ADB, BW), pp. 97–100.
- SAC-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.
IFM-2007-HasanT #cumulative #probability #using #verification- Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function (OH, ST), pp. 333–352.
TAP-2007-BruckerW #generative #higher-order #testing- Test-Sequence Generation with Hol-TestGen with an Application to Firewall Testing (ADB, BW), pp. 149–168.
POPL-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.
IJCAR-2006-ConstableM #proving #semantics #source code- Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics (RLC, WM), pp. 162–176.
- IJCAR-2006-Harrison #self #towards
- Towards Self-verification of HOL Light (JH), pp. 177–191.
- IJCAR-2006-McLaughlin #higher-order
- An Interpretation of Isabelle/HOL in HOL Light (SM), pp. 192–204.
- IJCAR-2006-ObuaS #higher-order
- Importing HOL into Isabelle/HOL (SO, SS), pp. 298–302.
- IJCAR-2006-UrbanB #combinator #data type #higher-order #recursion
- A Recursion Combinator for Nominal Datatypes Implemented in Isabelle/HOL (CU, SB), pp. 498–512.
- FASE-2005-HausmannMS #higher-order #induction
- Iterative Circular Coinduction for CoCasl in Isabelle/HOL (DH, TM, LS), pp. 341–356.
FM-2005-BasinKTW #architecture #verification- Verification of a Signature Architecture with HOL-Z (DAB, HK, KT, BW), pp. 269–285.
- SEFM-2005-BlechGG #higher-order #verification
- Formal Verification of Dead Code Elimination in Isabelle/HOL (JOB, LG, SG), pp. 200–209.
QAPL-2004-HurdMM05 #probability- Probabilistic Guarded Commands Mechanized in HOL (JH, AM, CM), pp. 95–111.
COCV-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.
- CADE-2005-UrbanT #higher-order
- Nominal Techniques in Isabelle/HOL (CU, CT), pp. 38–53.
FATES-2005-BruckerW #higher-order #interactive #testing- Interactive Testing with HOL-TestGen (ADB, BW), pp. 87–102.
- SEFM-2004-BerghoferN #higher-order #random testing #testing
- Random Testing in Isabelle/HOL (SB, TN), pp. 230–239.
- IJCAR-2004-AvigadD #formal method #higher-order
- Formalizing O Notation in Isabelle/HOL (JA, KD), pp. 357–371.
ESOP-2003-Nieto #higher-order- The Rely-Guarantee Method in Isabelle/HOL (LPN), pp. 348–362.
- IFM-2002-AkbarpourDT #fixpoint #formal method
- Formalization of Cadence SPW Fixed-Point Arithmetic in HOL (BA, AD, ST), pp. 185–204.
- IFM-2002-XiongCTB
- Formally Linking MDG and HOL Based on a Verified MDG System (HX, PC, ST, AB), pp. 205–224.
UML-2002-BruckerW #case study #design #experience #higher-order #named #ocl- HOL-OCL: Experiences, Consequences and Design Choices (ADB, BW), pp. 196–211.
- CADE-2002-Hurd #first-order #interface #logic
- An LCF-Style Interface between HOL and First-Order Logic (JH), pp. 134–138.
FoSSaCS-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.
- FASE-1999-NipkowN #higher-order
- Owicki/Gries in Isabelle/HOL (TN, LPN), pp. 188–203.
TACAS-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.
RTA-1999-DowekHK #first-order #higher-order #logic #named- HOL-λσ: An Intentional First-Order Expression of Higher-Order Logic (GD, TH, CK), pp. 317–331.
- CADE-1998-SlindGBB #interface
- System Description: An Interface Between CLAM and HOL (KS, MJCG, RJB, AB), pp. 134–138.
- FME-1997-TejW #csp #higher-order
- A Corrected Failure Divergence Model for CSP in Isabelle/HOL (HT, BW), pp. 318–337.
- CADE-1997-FeltyH #hybrid #interactive #proving #theorem proving #using
- Hybrid Interactive Theorem Proving Using Nuprl and HOL (APF, DJH), pp. 351–365.
- CADE-1996-Nipkow #higher-order #proving
- More Church-Rosser Proofs (in Isabelle/HOL) (TN), pp. 733–747.
- CADE-1992-Blackburn
- A Report in ICL HOL (KB), pp. 743–747.
CAV-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.
- CAV-1991-SchneiderKK #automation #hardware #proving
- Automating Most Parts of Hardware Proofs in HOL (KS, RK, TK), pp. 365–375.
- CAV-1991-SegerJ #using #verification
- A Two-Level Formal Verification Methodology using HOL and COSMOS (CJHS, JJJ), pp. 299–309.
