BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Hoare
Google Hoare

Tag #hoare

54 papers:

PLDIPLDI-2019-ZhouYY #logic #quantum
An applied quantum Hoare logic (LZ, NY, MY), pp. 1149–1162.
POPLPOPL-2019-Unruh #logic #quantum #relational
Quantum relational Hoare logic (DU), p. 31.
CAVCAV-2019-LiuZWYLLYZ #algorithm #logic #quantum #using #verification
Formal Verification of Quantum Algorithms Using Quantum Hoare Logic (JL, BZ, SW, SY, TL, YL, MY, NZ), pp. 187–207.
IFM-2017-OweRF #contract #multi #reasoning
Hoare-Style Reasoning from Multiple Contracts (OO, TR, EF), pp. 263–278.
OOPSLAOOPSLA-2016-SergeyNBD #concurrent #correctness #specification
Hoare-style specifications as correctness conditions for non-linearizable concurrent objects (IS, AN, AB0, GAD), pp. 92–110.
PLDIPLDI-2016-SousaD #logic #verification
Cartesian hoare logic for verifying k-safety properties (MS, ID), pp. 57–69.
SOSPSOSP-2015-ChenZCCKZ #file system #logic #using
Using Crash Hoare logic for certifying the FSCQ file system (HC, DZ, TC, AC, MFK, NZ), pp. 18–37.
FoSSaCSFoSSaCS-2015-Mamouras #logic #nondeterminism #synthesis
Synthesis of Strategies and the Hoare Logic of Angelic Nondeterminism (KM), pp. 25–40.
SEFMSEFM-2014-SznukS #education #logic #tool support
Tool Support for Teaching Hoare Logic (TS, AS), pp. 332–346.
LICSLICS-CSL-2014-Mamouras #monad #on the #recursion
On the Hoare theory of monadic recursion schemes (KM), p. 10.
ICFPICFP-2013-Chlipala #generative #logic #metaprogramming #verification
The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier (AC), pp. 391–402.
ICFPICFP-2013-DelbiancoN #algebra #continuation #reasoning
Hoare-style reasoning with (algebraic) continuations (GAD, AN), pp. 363–376.
ICFPICFP-2013-TuronDB #concurrent #higher-order #logic #reasoning #refinement
Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency (AT, DD, LB), pp. 377–390.
LICSLICS-2013-GoncharovS #logic
A Relatively Complete Generic Hoare Logic for Order-Enriched Effects (SG, LS), pp. 273–282.
FMFM-2012-RosuS #logic #reachability
From Hoare Logic to Matching Logic Reachability (GR, AS), pp. 387–402.
POPLPOPL-2012-BlackO #perspective
Presentation of the SIGPLAN distinguished achievement award to Sir Charles Antony Richard Hoare, FRS, FREng, FBCS; and interview (APB, PWO), pp. 1–2.
SEFMSEFM-2011-VriesK #logic
Reverse Hoare Logic (EdV, VK), pp. 155–171.
ICGTICGT-2010-PoskittP #calculus #graph #source code
A Hoare Calculus for Graph Programs (CMP, DP), pp. 139–154.
ESOPESOP-2010-NakataU #induction #logic #semantics
A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While (KN, TU), pp. 488–506.
CSLCSL-2009-SchwinghammerBRY #higher-order
Nested Hoare Triples and Frame Rules for Higher-Order Store (JS, LB, BR, HY), pp. 440–454.
PODSPODS-2008-GardnerSWZ #reasoning
Local Hoare reasoning about DOM (PG, GS, MJW, UZ), pp. 261–270.
ESOPESOP-2008-PetersenBNM #type system
A Realizability Model for Impredicative Hoare Type Theory (RLP, LB, AN, GM), pp. 337–352.
WRLAWRLA-2006-SasseM07 #algebra #java #logic #semantics #verification
Java+ITP: A Verification Tool Based on Hoare Logic and Algebraic Semantics (RS, JM), pp. 29–46.
ESOPESOP-2007-NanevskiAMB #data type #type system
Abstract Predicates and Mutable ADTs in Hoare Type Theory (AN, AA, GM, LB), pp. 189–204.
TACASTACAS-2007-MyreenG #logic
Hoare Logic for Realistically Modelled Machine Code (MOM, MJCG), pp. 568–582.
ICALPICALP-v2-2006-CorinH #encryption #game studies #logic #probability #proving
A Probabilistic Hoare-style Logic for Game-Based Cryptographic Proofs (RC, JdH), pp. 252–263.
ICFPICFP-2006-NanevskiMB #morphism #polymorphism #type system
Polymorphism and separation in hoare type theory (AN, GM, LB), pp. 62–73.
CSLCSL-2006-MartinMO #logic
Hoare Logic in the Abstract (UM, EAM, PO), pp. 501–515.
LICSLICS-2006-ParkinsonBC #logic
Variables as Resource in Hoare Logics (MJP, RB, CC), pp. 137–146.
ICALPICALP-2005-ReusS #higher-order #logic
About Hoare Logics for Higher-Order Store (BR, TS), pp. 1337–1348.
FASEFASE-2003-SchroderM #independence #logic
Monad-Independent Hoare Logic in HASCASL (LS, TM), pp. 261–277.
FMFME-2002-OheimbN #logic #revisited
Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited (DvO, TN), pp. 89–105.
CSLCSL-2002-Nipkow #bound #logic #nondeterminism #recursion
Hoare Logics for Recursive Procedures and Unbounded Nondeterminism (TN), pp. 103–119.
FASEFASE-2001-ReusWH #calculus #design #java #modelling #ocl #verification
A Hoare Calculus for Verifying Java Realizations of OCL-Constrained Design Models (BR, MW, RH), pp. 300–317.
PPDPPPDP-2000-CalcagnoIO #alias #analysis #logic #pointer #semantics
Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic351292 (CC, SSI, PWO), pp. 190–201.
FASEFASE-2000-HuismanJ #java #logic #termination #verification
Java Program Verification via a Hoare Logic with Abrupt Termination (MH, BJ), pp. 284–303.
LICSLICS-1999-Kozen #algebra #logic #on the #testing
On Hoare Logic and Kleene Algebra with Tests (DK), pp. 167–172.
SEKESEKE-1994-Pliuskeviciene #logic #recursion
Specialization of derivations in Hoare-like logic with recursive procedures (AP), pp. 124–130.
LICSLICS-1991-Hungar #bound #complexity #proving
Complexity Bounds of Hoare-style Proof Systems (HH), pp. 120–126.
LICSLICS-1988-GrabowskiH #effectiveness #logic #on the
On the Existence of Effective Hoare Logics (MG, HH), pp. 428–435.
LICSLICS-1987-Goerdt #imperative #logic
Hoare Logic for λ-Terms as Basis of Hoare Logic for Imperative Languages (AG), pp. 293–299.
LICSLICS-1986-Meyer #logic #semantics
Floyd-Hoare Logic Defines Semantics: Preliminary Version (ARM), pp. 44–48.
ICALPICALP-1985-Hortala-GonzalezR #logic #nondeterminism #source code #standard #theorem
Hoare’s Logic for Nondeterministic Regular Programs: A Nonstandard Completeness Theorem (MTHG, MRA), pp. 270–280.
POPLPOPL-1984-Halpern #algol #axiom
A Good Hoare Axiom System for an Algol-like Language (JYH), pp. 262–271.
STOCSTOC-1983-Olderog #logic #source code
A Characterization of Hoare’s Logic for Programs with Pascal-like Procedures (ERO), pp. 320–329.
ICALPICALP-1982-Gerth #ada #axiom
A Sound and Complete Hoare Axiomatization of the Ada-Rendevous (RG), pp. 252–264.
POPLPOPL-1982-ClarkeGH #axiom #effectiveness #logic #on the
On Effective Axiomatizations of Hoare Logics (EMC, SMG, JYH), pp. 309–321.
ICALPICALP-1981-BergstraT #algebra #logic #programming
Algebraically Specified Programming Systems and Hoare’s Logic (JAB, JVT), pp. 348–362.
ICALPICALP-1981-MoriconiS #automation #generative #logic #verification
Automatic Construction of Verification Condition Generators From Hoare Logics (MM, RLS), pp. 363–377.
ICALPICALP-1980-LangmaackO #programming language
Present-Day Hoare-Like Systems for Programming Languages with Procedures: Power, Limits and most Likely Expressions (HL, ERO), pp. 363–373.
POPLPOPL-1978-CartwrightO #logic #strict
Unrestricted Procedure Calls in Hoare’s Logic (RC, DCO), pp. 131–140.
POPLPOPL-1977-CherniavskyK #consistency #programming language #semantics
A Complete and Consistent Hoare Semantics for a Simple Programming Language (JCC, SNK), pp. 1–9.
POPLPOPL-1977-Clarke #axiom #programming language
Programming Language Constructs for Which it is Impossible to Obtain “Good” Hoare-Like Axiom Systems (EMC), pp. 10–20.
STOCSTOC-1976-Wand
A New Incompleteness Result for Hoare’s System (MW), pp. 87–91.

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.