Stem hoar$ (all stems)

48 papers:

FoSSaCS-2015-Mamouras #hoare #logic #nondeterminism #synthesis

Synthesis of Strategies and the Hoare Logic of Angelic Nondeterminism (KM), pp. 25–40.

SOSP-2015-ChenZCCKZ #file system #hoare #logic #using

Using Crash Hoare logic for certifying the FSCQ file system (HC, DZ, TC, AC, MFK, NZ), pp. 18–37.

SEFM-2014-SznukS #education #hoare #logic #tool support

Tool Support for Teaching Hoare Logic (TS, AS), pp. 332–346.

LICS-CSL-2014-Mamouras #hoare #monad #on the #recursion

On the Hoare theory of monadic recursion schemes (KM), p. 10.

ICFP-2013-Chlipala #generative #hoare #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 #hoare #reasoning

Hoare-style reasoning with (algebraic) continuations (GAD, AN), pp. 363–376.

ICFP-2013-TuronDB #concurrent #higher-order #hoare #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 #hoare #logic

A Relatively Complete Generic Hoare Logic for Order-Enriched Effects (SG, LS), pp. 273–282.

FM-2012-RosuS #hoare #logic #reachability

From Hoare Logic to Matching Logic Reachability (GR, AS), pp. 387–402.

POPL-2012-BlackO #hoare #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 #hoare #logic

Reverse Hoare Logic (EdV, VK), pp. 155–171.

ESOP-2010-NakataU #hoare #induction #logic #semantics

A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While (KN, TU), pp. 488–506.

ICGT-2010-PoskittP #calculus #graph #hoare #source code

A Hoare Calculus for Graph Programs (CMP, DP), pp. 139–154.

CSL-2009-SchwinghammerBRY #higher-order #hoare

Nested Hoare Triples and Frame Rules for Higher-Order Store (JS, LB, BR, HY), pp. 440–454.

PODS-2008-GardnerSWZ #hoare #reasoning

Local Hoare reasoning about DOM (PG, GS, MJW, UZ), pp. 261–270.

ESOP-2008-PetersenBNM #hoare #type system

A Realizability Model for Impredicative Hoare Type Theory (RLP, LB, AN, GM), pp. 337–352.

WRLA-2006-SasseM07 #algebra #hoare #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 #hoare #type system

Abstract Predicates and Mutable ADTs in Hoare Type Theory (AN, AA, GM, LB), pp. 189–204.

TACAS-2007-MyreenG #hoare #logic

Hoare Logic for Realistically Modelled Machine Code (MOM, MJCG), pp. 568–582.

ICALP-v2-2006-CorinH #encryption #game studies #hoare #logic #probability #proving

A Probabilistic Hoare-style Logic for Game-Based Cryptographic Proofs (RC, JdH), pp. 252–263.

ICFP-2006-NanevskiMB #hoare #morphism #polymorphism #type system

Polymorphism and separation in hoare type theory (AN, GM, LB), pp. 62–73.

CSL-2006-MartinMO #hoare #logic

Hoare Logic in the Abstract (UM, EAM, PO), pp. 501–515.

LICS-2006-ParkinsonBC #hoare #logic

Variables as Resource in Hoare Logics (MJP, RB, CC), pp. 137–146.

ICALP-2005-ReusS #higher-order #hoare #logic

About Hoare Logics for Higher-Order Store (BR, TS), pp. 1337–1348.

FASE-2003-SchroderM #hoare #independence #logic

Monad-Independent Hoare Logic in HASCASL (LS, TM), pp. 261–277.

FME-2002-OheimbN #hoare #logic #revisited

Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited (DvO, TN), pp. 89–105.

CSL-2002-Nipkow #bound #hoare #logic #nondeterminism #recursion

Hoare Logics for Recursive Procedures and Unbounded Nondeterminism (TN), pp. 103–119.

FASE-2001-ReusWH #calculus #design #hoare #java #modelling #ocl #verification

A Hoare Calculus for Verifying Java Realizations of OCL-Constrained Design Models (BR, MW, RH), pp. 300–317.

FASE-2000-HuismanJ #hoare #java #logic #termination #verification

Java Program Verification via a Hoare Logic with Abrupt Termination (MH, BJ), pp. 284–303.

PPDP-2000-CalcagnoIO #alias #analysis #hoare #logic #pointer #semantics

Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic351292 (CC, SSI, PWO), pp. 190–201.

LICS-1999-Kozen #algebra #hoare #logic #on the #testing

On Hoare Logic and Kleene Algebra with Tests (DK), pp. 167–172.

SEKE-1994-Pliuskeviciene #hoare #logic #recursion

Specialization of derivations in Hoare-like logic with recursive procedures (AP), pp. 124–130.

LICS-1991-Hungar #bound #complexity #hoare #proving

Complexity Bounds of Hoare-style Proof Systems (HH), pp. 120–126.

LICS-1988-GrabowskiH #effectiveness #hoare #logic #on the

On the Existence of Effective Hoare Logics (MG, HH), pp. 428–435.

LICS-1987-Goerdt #hoare #imperative #logic

Hoare Logic for λ-Terms as Basis of Hoare Logic for Imperative Languages (AG), pp. 293–299.

LICS-1986-Meyer #hoare #logic #semantics

Floyd-Hoare Logic Defines Semantics: Preliminary Version (ARM), pp. 44–48.

ICALP-1985-Hortala-GonzalezR #hoare #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 #hoare

A Good Hoare Axiom System for an Algol-like Language (JYH), pp. 262–271.

STOC-1983-Olderog #hoare #logic #source code

A Characterization of Hoare’s Logic for Programs with Pascal-like Procedures (ERO), pp. 320–329.

ICALP-1982-Gerth #ada #axiom #hoare

A Sound and Complete Hoare Axiomatization of the Ada-Rendevous (RG), pp. 252–264.

POPL-1982-ClarkeGH #axiom #effectiveness #hoare #logic #on the

On Effective Axiomatizations of Hoare Logics (EMC, SMG, JYH), pp. 309–321.

ICALP-1981-BergstraT #algebra #hoare #logic #programming

Algebraically Specified Programming Systems and Hoare’s Logic (JAB, JVT), pp. 348–362.

ICALP-1981-MoriconiS #automation #generative #hoare #logic #verification

Automatic Construction of Verification Condition Generators From Hoare Logics (MM, RLS), pp. 363–377.

ICALP-1980-LangmaackO #hoare #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 #hoare #logic #strict

Unrestricted Procedure Calls in Hoare’s Logic (RC, DCO), pp. 131–140.

POPL-1977-CherniavskyK #consistency #hoare #programming language #semantics

A Complete and Consistent Hoare Semantics for a Simple Programming Language (JCC, SNK), pp. 1–9.

POPL-1977-Clarke #axiom #hoare #programming language

Programming Language Constructs for Which it is Impossible to Obtain “Good” Hoare-Like Axiom Systems (EMC), pp. 10–20.

STOC-1976-Wand #hoare

A New Incompleteness Result for Hoare’s System (MW), pp. 87–91.