Tag #hoare
54 papers:
PLDI-2019-ZhouYY #logic #quantum- An applied quantum Hoare logic (LZ, NY, MY), pp. 1149–1162.
POPL-2019-Unruh #logic #quantum #relational- Quantum relational Hoare logic (DU), p. 31.
CAV-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.
OOPSLA-2016-SergeyNBD #concurrent #correctness #specification- Hoare-style specifications as correctness conditions for non-linearizable concurrent objects (IS, AN, AB0, GAD), pp. 92–110.
- PLDI-2016-SousaD #logic #verification
- Cartesian hoare logic for verifying k-safety properties (MS, ID), pp. 57–69.
SOSP-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.
FoSSaCS-2015-Mamouras #logic #nondeterminism #synthesis- Synthesis of Strategies and the Hoare Logic of Angelic Nondeterminism (KM), pp. 25–40.
SEFM-2014-SznukS #education #logic #tool support- Tool Support for Teaching Hoare Logic (TS, AS), pp. 332–346.
LICS-CSL-2014-Mamouras #monad #on the #recursion- On the Hoare theory of monadic recursion schemes (KM), p. 10.
ICFP-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.
- ICFP-2013-DelbiancoN #algebra #continuation #reasoning
- Hoare-style reasoning with (algebraic) continuations (GAD, AN), pp. 363–376.
- ICFP-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.
- LICS-2013-GoncharovS #logic
- A Relatively Complete Generic Hoare Logic for Order-Enriched Effects (SG, LS), pp. 273–282.
FM-2012-RosuS #logic #reachability- From Hoare Logic to Matching Logic Reachability (GR, AS), pp. 387–402.
- POPL-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.
- SEFM-2011-VriesK #logic
- Reverse Hoare Logic (EdV, VK), pp. 155–171.
ICGT-2010-PoskittP #calculus #graph #source code- A Hoare Calculus for Graph Programs (CMP, DP), pp. 139–154.
ESOP-2010-NakataU #induction #logic #semantics- A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While (KN, TU), pp. 488–506.
CSL-2009-SchwinghammerBRY #higher-order- Nested Hoare Triples and Frame Rules for Higher-Order Store (JS, LB, BR, HY), pp. 440–454.
PODS-2008-GardnerSWZ #reasoning- Local Hoare reasoning about DOM (PG, GS, MJW, UZ), pp. 261–270.
- ESOP-2008-PetersenBNM #type system
- A Realizability Model for Impredicative Hoare Type Theory (RLP, LB, AN, GM), pp. 337–352.
WRLA-2006-SasseM07 #algebra #java #logic #semantics #verification- Java+ITP: A Verification Tool Based on Hoare Logic and Algebraic Semantics (RS, JM), pp. 29–46.
- ESOP-2007-NanevskiAMB #data type #type system
- Abstract Predicates and Mutable ADTs in Hoare Type Theory (AN, AA, GM, LB), pp. 189–204.
TACAS-2007-MyreenG #logic- Hoare Logic for Realistically Modelled Machine Code (MOM, MJCG), pp. 568–582.
ICALP-v2-2006-CorinH #encryption #game studies #logic #probability #proving- A Probabilistic Hoare-style Logic for Game-Based Cryptographic Proofs (RC, JdH), pp. 252–263.
- ICFP-2006-NanevskiMB #morphism #polymorphism #type system
- Polymorphism and separation in hoare type theory (AN, GM, LB), pp. 62–73.
- CSL-2006-MartinMO #logic
- Hoare Logic in the Abstract (UM, EAM, PO), pp. 501–515.
- LICS-2006-ParkinsonBC #logic
- Variables as Resource in Hoare Logics (MJP, RB, CC), pp. 137–146.
- ICALP-2005-ReusS #higher-order #logic
- About Hoare Logics for Higher-Order Store (BR, TS), pp. 1337–1348.
FASE-2003-SchroderM #independence #logic- Monad-Independent Hoare Logic in HASCASL (LS, TM), pp. 261–277.
- FME-2002-OheimbN #logic #revisited
- Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited (DvO, TN), pp. 89–105.
- CSL-2002-Nipkow #bound #logic #nondeterminism #recursion
- Hoare Logics for Recursive Procedures and Unbounded Nondeterminism (TN), pp. 103–119.
- FASE-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.
PPDP-2000-CalcagnoIO #alias #analysis #logic #pointer #semantics- Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic351292 (CC, SSI, PWO), pp. 190–201.
- FASE-2000-HuismanJ #java #logic #termination #verification
- Java Program Verification via a Hoare Logic with Abrupt Termination (MH, BJ), pp. 284–303.
- LICS-1999-Kozen #algebra #logic #on the #testing
- On Hoare Logic and Kleene Algebra with Tests (DK), pp. 167–172.
SEKE-1994-Pliuskeviciene #logic #recursion- Specialization of derivations in Hoare-like logic with recursive procedures (AP), pp. 124–130.
- LICS-1991-Hungar #bound #complexity #proving
- Complexity Bounds of Hoare-style Proof Systems (HH), pp. 120–126.
- LICS-1988-GrabowskiH #effectiveness #logic #on the
- On the Existence of Effective Hoare Logics (MG, HH), pp. 428–435.
- LICS-1987-Goerdt #imperative #logic
- Hoare Logic for λ-Terms as Basis of Hoare Logic for Imperative Languages (AG), pp. 293–299.
- LICS-1986-Meyer #logic #semantics
- Floyd-Hoare Logic Defines Semantics: Preliminary Version (ARM), pp. 44–48.
- ICALP-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.
- POPL-1984-Halpern #algol #axiom
- A Good Hoare Axiom System for an Algol-like Language (JYH), pp. 262–271.
STOC-1983-Olderog #logic #source code- A Characterization of Hoare’s Logic for Programs with Pascal-like Procedures (ERO), pp. 320–329.
- ICALP-1982-Gerth #ada #axiom
- A Sound and Complete Hoare Axiomatization of the Ada-Rendevous (RG), pp. 252–264.
- POPL-1982-ClarkeGH #axiom #effectiveness #logic #on the
- On Effective Axiomatizations of Hoare Logics (EMC, SMG, JYH), pp. 309–321.
- ICALP-1981-BergstraT #algebra #logic #programming
- Algebraically Specified Programming Systems and Hoare’s Logic (JAB, JVT), pp. 348–362.
- ICALP-1981-MoriconiS #automation #generative #logic #verification
- Automatic Construction of Verification Condition Generators From Hoare Logics (MM, RLS), pp. 363–377.
- ICALP-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.
- POPL-1978-CartwrightO #logic #strict
- Unrestricted Procedure Calls in Hoare’s Logic (RC, DCO), pp. 131–140.
- POPL-1977-CherniavskyK #consistency #programming language #semantics
- A Complete and Consistent Hoare Semantics for a Simple Programming Language (JCC, SNK), pp. 1–9.
- POPL-1977-Clarke #axiom #programming language
- Programming Language Constructs for Which it is Impossible to Obtain “Good” Hoare-Like Axiom Systems (EMC), pp. 10–20.
- STOC-1976-Wand
- A New Incompleteness Result for Hoare’s System (MW), pp. 87–91.
