Störningsfrihet

Inom datavetenskap är störningsfrihet en teknik för att bevisa partiell korrekthet av samtidiga program med delade variabler . Hoare-logik hade introducerats tidigare för att bevisa korrektheten av sekventiella program. I sin doktorsavhandling (och artiklar som härrör från den) under rådgivare David Gries , utökade Susan Owicki detta arbete till att gälla samtidiga program.

Samtidig programmering hade använts sedan mitten av 1960-talet för att koda operativsystem som uppsättningar av samtidiga processer (se särskilt Dijkstra.), men det fanns ingen formell mekanism för att bevisa korrekthet. Att resonera om interfolierade exekveringssekvenser för de individuella processerna var svårt, var felbenäget och skalade inte upp. Interferensfrihet gäller för bevis istället för exekveringssekvenser; en visar att exekvering av en process inte kan störa korrekthetsbeviset för en annan process.

En rad intrikata samtidiga program har visat sig vara korrekta med hjälp av störningsfrihet, och störningsfrihet ligger till grund för mycket av det efterföljande arbetet med att utveckla samtidiga program med delade variabler och bevisa att de är korrekta. Owicki-Gries-uppsatsen En axiomatisk provningsteknik för parallella program Jag fick 1977 ACM Award för bästa papper inom programmeringsspråk och -system.

Notera. Lamport presenterar en liknande idé. Han skriver, "Efter att ha skrivit den första versionen av detta dokument fick vi veta om Owickis senaste arbete." Hans uppsats har inte fått lika mycket uppmärksamhet som Owicki-Gries, kanske för att den använde flödesscheman istället för texten i programmeringskonstruktioner som if- satsen och while- loopen. Lamport generaliserade Floyds metod medan Owicki-Gries generaliserade Hoares metod. I princip allt senare arbete inom detta område använder text och inte flödesscheman. En annan skillnad nämns nedan i avsnittet Hjälpvariabler .

Dijkstras princip om icke-interferens

Edsger W. Dijkstra introducerade principen om icke-interferens i EWD 117, "Programming Considered as a Human Activity", skriven om 1965. Denna princip säger att: Helhetens riktighet kan fastställas genom att endast ta hänsyn till de yttre specifikationerna ( förkortade specifikationer genomgående) av delarna, och inte deras inre konstruktion. Dijkstra beskrev de allmänna stegen för att använda denna princip:

1. Ge en komplett spec för varje enskild del.
2. Kontrollera att det totala problemet är löst när programdelar som uppfyller deras specifikationer är tillgängliga.
3. Konstruera de enskilda delarna för att tillfredsställa deras specifikationer, men oberoende av varandra och det sammanhang där de kommer att användas.

Han gav flera exempel på denna princip utanför programmering. Men dess användning i programmering är ett huvudproblem. Till exempel bör en programmerare som använder en metod (subrutin, funktion, etc.) bara förlita sig på dess specifikation för att avgöra vad den gör och hur den ska anropas, och aldrig på dess implementering.

Programspecifikationer är skrivna i Hoare-logik , introducerad av Sir Tony Hoare , som exemplifieras i specifikationerna för processerna S1 och S2 :

       
                 
      {pre-S1 } {pre-S2 } S1 S2 {post-S1 } {pre-S2 }

Betydelse: Om exekvering av Si i ett tillstånd där precondition pre-Si är sant avslutas, så är postcondition post-Si vid avslutning sant.

Överväg nu samtidig programmering med delade variabler. Specifikationerna för två (eller flera) processer S1 och S2 ges i termer av deras för- och eftervillkor, och vi antar att implementeringar av S1 och S2 ges som uppfyller deras specifikationer. Men när man utför sina implementeringar parallellt, eftersom de delar variabler, kan ett rastillstånd uppstå; en process ändrar en delad variabel till ett värde som inte förutses i beviset för den andra processen, så den andra processen fungerar inte som avsett.

Därmed bryts Dijkstras princip om icke-inblandning.

I sin doktorsavhandling från 1975 i datavetenskap , Cornell University , skriven under rådgivaren David Gries , utvecklade Susan Owicki begreppet störningsfrihet . Om processerna S1 och S2 uppfyller störningsfrihet, kommer deras parallella utförande att fungera som planerat. Dijkstra kallade detta arbete det första betydande steget mot att tillämpa Hoare-logik på samtidiga processer. För att förenkla diskussioner begränsar vi uppmärksamheten till endast två samtidiga processer, även om Owicki-Gries tillåter fler.

Störningsfrihet när det gäller beviskonturer

Owicki-Gries introducerade beviskonturen för en Hoare trippel {P}S{Q }. Den innehåller alla detaljer som behövs för att bevisa riktigheten av {P}S{Q } med hjälp av Hoare-logikens axiom och slutledningsregler . (Detta arbete använder uppdragssatsen x: = e , if-then och if-then-else , och while- loopen.) Hoare anspelade på beviskonturer i sitt tidiga arbete; för störningsfrihet måste den formaliseras.

En beviskontur för {P}S{Q } börjar med förutsättning P och slutar med eftervillkor Q . Två påståenden inom klammerparenteser { och } som visas bredvid varandra indikerar att den första måste antyda den andra.

Exempel: En beviskontur för {P} S {Q } där S är: x : = a; om e så S1 annars S2

  
  
  
  
  
                 
                 
        
                 
                 
  
   {P } {P1[x/a] } x : = a; {P1 } om e då {P1 ∧ e } S1 {Q1 } annars {P1 ∧ ¬ e } S2 {Q1 } {Q1 } {Q }

P ⇒ P1[x/a] måste gälla, där P1[x/a] står för P1 med varje förekomst av x ersatt av en . (I det här exemplet S1 och S2 grundläggande uttalanden, som en tilldelningssats, skippa eller en avvaktansats .)

Varje påstående T i beviskonturen föregås av ett previllkor pre-T och följs av ett postvillkor post-T , och {pre-T}T{post-T } måste kunna bevisas med hjälp av något axiom eller slutledningsregel för Hoare-logik. Således innehåller beviskonturen all information som behövs för att bevisa att {P}S{Q } är korrekt.

Tänk nu på två processer S1 och S2 som körs parallellt och deras specifikationer:

       
                 
      {pre-S1 } {pre-S2 } S1 S2 {post-S1 } {post-S2 }

Att bevisa att de fungerar på lämpligt sätt parallellt kommer att kräva att de begränsas enligt följande. Varje uttryck E i S1 eller S2 kan hänvisa till högst en variabel y som kan ändras av den andra processen medan E utvärderas, och E kan hänvisa till y högst en gång. En liknande begränsning gäller för tilldelningssatser x: = E .

Med denna konvention behöver den enda odelbara åtgärden vara minnesreferensen. Anta till exempel att process S1 refererar till variabel y medan S2 ändrar y . Värdet S1 får för y måste vara värdet före eller efter att S2 ändrar y , och inte något falskt mellanvärde.

Definition av störningsfri

Den viktiga innovationen med Owicki-Gries var att definiera vad det betyder för ett påstående T att inte störa beviset för {P}S{Q }. Om exekvering av T inte kan förfalska något påstående som ges i beviskonturen för {P}S{Q }, så gäller det beviset fortfarande även inför samtidig exekvering av S och T .

Definition . Påstående T med precondition pre-T stör inte beviset för {P}S{Q } om två villkor gäller:

(1) {Q ∧ pre-T} T {Q } (2) Låt S' vara vilket som helst uttalande inom S men inte inom ett avvaktande uttalande (se senare avsnitt). Sedan {pre-S' ∧ pre-T} T {pre-S' }.

Läs den sista Hoare-trippeln så här: Om tillståndet är sådant att både T och S' kan exekveras, så kommer exekveringen av T inte att förfalska pre-S' .

Definition . Beviskonturer för {P1}S1{Q1 } och {P2}S2{Q2 } är störningsfria om följande gäller. Låt T vara en await- eller tilldelningssats (som inte visas i en await ) av process S1 . Då T beviset för {P2}S2{Q2 }. På samma sätt för T för process S2 och {P1}S1{Q1 }.

Uttalanden börjar och väntar

Två uttalanden infördes för att hantera samtidighet. Exekvering av satsen cobegin S1 // S2 coend exekverar S1 och S2 parallellt. Den avslutas när både S1 och S2 har avslutats.

Utförande av await -satsen await B , sedan S tills villkor fördröjs B är sant. Sedan exekveras påstående S som en odelbar handling - utvärdering av B är en del av den odelbara handlingen. Om två processer väntar på samma villkor B , när det blir sant, fortsätter en av dem att vänta medan den andra fortsätter.

Vänta uttalandet kan inte implementeras effektivt och föreslås inte infogas i programmeringsspråket . Snarare tillhandahåller det ett sätt att representera flera standardprimitiver såsom semaforer – uttryck först semaforoperationerna som await s , använd sedan de tekniker som beskrivs här.

Slutledningsregler för avvakta och cobegin är:

vänta {P ∧ B} S {Q} / {P} vänta B sedan S {Q} börjar med
{P1} S1 {Q1}, {P2} S2 {Q2} störningsfritt / {P1∧P2} börjar med S1// S2 coend {Q1∧Q2}

Hjälpvariabler

En hjälpvariabel förekommer inte i programmet utan introduceras i korrekthetsbeviset för att göra resonemanget enklare — eller till och med möjligt. Hjälpvariabler används endast i tilldelningar till hjälpvariabler, så deras introduktion varken ändrar programmet för någon inmatning eller påverkar värdena på programvariabler. Vanligtvis används de antingen som programräknare eller för att registrera historik för en beräkning.

Definition . Låt AV vara en uppsättning variabler som endast förekommer i S' i tilldelningarna x: = E , där x är i AV . Då är AV en hjälpvariabel satt för S' .

Eftersom en uppsättning AV med hjälpvariabler endast används i tilldelningar till variabler i AV , ändrar inte programmets korrekthet att ta bort alla tilldelningar till dem, och vi har slutledningsregeln AV- eliminering:

   {P} S' {Q} / {P} S {Q}

AV är en hjälpvariabel för S' . Variablerna i AV förekommer inte i P eller Q . S erhålls från S' genom att ta bort alla tilldelningar till variablerna i AV .

Istället för att använda hjälpvariabler kan man införa en programräknare i bevissystemet, men det ökar komplexiteten i bevissystemet.

Notera: Apt diskuterar Owicki-Gries-logiken i samband med rekursiva påståenden, det vill säga effektivt beräkningsbara påståenden. Han bevisar att alla påståenden i beviskonturer kan vara rekursiva, men att detta inte längre är fallet om hjälpvariabler endast används som programräknare och inte för att registrera beräkningshistorik. Lamport, i sitt liknande arbete, använder påståenden om tokenpositioner istället för hjälpvariabler, där en token på kanten av ett flödesschema är besläktad med en programräknare. Det finns ingen föreställning om en historikvariabel. Detta indikerar att Owicki-Gries och Lamports tillvägagångssätt inte är likvärdiga när de är begränsade till rekursiva påståenden.

Dödläge och uppsägning

Owicki-Gries behandlar huvudsakligen partiell korrekthet: {P} S {Q } betyder: Om S exekveras i ett tillstånd där P är sant slutar, så är Q sant för tillståndet vid avslutning. Men Owicki-Gries ger också några praktiska tekniker som använder information som erhållits från ett partiellt korrekthetsbevis för att härleda andra korrekthetsegenskaper, inklusive frihet från dödläge, programavslutning och ömsesidig uteslutning.

Ett program är i dödläge om alla processer som inte har avslutats exekverar await- satser och ingen kan fortsätta eftersom deras await -villkor är falska. Owicki-Gries ger förhållanden under vilka dödläge inte kan uppstå.

Owicki-Gries presenterar en slutledningsregel för total korrekthet av while- slingan. Den använder en bunden funktion som minskar med varje iteration och är positiv så länge som loopvillkoret är sant. Apt et al visar att denna nya slutledningsregel inte tillfredsställer störningsfrihet. Det faktum att den bundna funktionen är positiv så länge loopvillkoret är sant ingick inte i ett interferenstest. De visar två sätt att rätta till detta misstag.

Ett enkelt exempel

       
       

       
        Betrakta påståendet: {x=0} cobegin await true then x: = x+1 // await true then x: = x+2 coend {x=3}

Beviset för det:

       
       
       
       
     
       
       
       
       
     

{x=0} S: medstart {x=0} {x=0 ∨ x=2} S1: vänta sant sedan x : = x+1 {Q1: x=1 ∨ x=3} // {x=0 } {x=0 ∨ x=1} S2: vänta sant sedan x : = x+2 {Q2: x=2 ∨ x=3} coend {(x=1 ∨ x=3) ∧ (x=2 ∨ x =3)} {x=3}

Att bevisa att S1 inte stör beviset för S2 kräver bevis på två Hoare-trippel:

(1) {(x=0 ∨ x=2) ∧ (x=0 ∨ x=1} S1 {x=0 ∨ x=1} (2) {(x=0 ∨ x=2) ∧ ( x = 2 ∨ x=3} S1 {x=2 ∨ x=3}

Förutsättningen för (1) reduceras till x=0 och förutsättningen för (2) reduceras till x=2 . Av detta är det lätt att se att dessa Hoare-trippel håller. Två liknande Hoare-trippel krävs för att visa att S2 inte stör beviset för S1 .

Antag att S1 ändras från await -satsen till tilldelningen x: = x+1 . Då uppfyller inte beviskonturen kraven, eftersom uppgiften innehåller två förekomster av delad variabel x . Faktum är att värdet på x efter exekvering av cobegin -satsen kan vara 2 eller 3.

Antag att S1 ändras till await -satsen await true då x: = x+2 , så det är samma som S2 . Efter exekvering av S bör x vara 4. För att bevisa detta , eftersom de två tilldelningarna är lika, behövs två hjälpvariabler, en för att indikera om S1 har exekveras; den andra, om S2 har utförts. Vi lämnar ändringen i korrekturkonturen till läsaren.

Exempel på formellt bevisade samtidiga program

A. Findpos . Skriv ett program som hittar det första positiva elementet i en array (om det finns en). En process kontrollerar alla arrayelement vid jämna positioner i arrayen och avslutas när den hittar ett positivt värde eller när inget hittas. På liknande sätt kontrollerar den andra processen arrayelement vid udda positioner i arrayen. Detta exempel handlar alltså om while- slingor. Den har inte heller några avvaktande uttalanden.

Detta exempel kommer från Barry K. Rosen. Lösningen i Owicki-Gries, komplett med program, korrekturöversikt och diskussion om störningsfrihet, tar mindre än två sidor. Störningsfrihet är ganska lätt att kontrollera, eftersom det bara finns en delad variabel. Däremot använder Rosens artikel Findpos som det enda löpande exemplet i detta 24-sidiga papper.

En översikt över båda processerna i en allmän miljö:

     
     
     
     
  
     
     
     
     

cobegin producent: ... vänta in-ut < N hoppa över ; add: b[in mod N]:= nästa värde; markin: in: = in+1; ... // konsument: ... vänta in-ut > 0 och hoppa över ; ta bort:
        detta värde:= b[out mod N]; markout: ut: = ut+1; coend ...

B. Begränsad buffertkonsument/producentproblem . En producentprocess genererar värden och placerar dem i avgränsad buffert b av storlek N ; en konsumentprocess tar bort dem. De går till rörlig ränta. Producenten måste vänta om buffert b är full; konsumenten måste vänta om buffert b är tom. I Owicki-Gries visas en lösning i en allmän miljö; den är sedan inbäddad i ett program som kopierar en array c[1..M] till en array d[1..M] .

Det här exemplet visar en princip för att reducera störningskontroller till ett minimum: Placera så mycket som möjligt i ett påstående som alltid är sant överallt i båda processerna. I det här fallet är påståendet definitionen av den avgränsade bufferten och gränser för variabler som indikerar hur många värden som har lagts till och tagits bort från bufferten. Förutom själva bufferten b registrerar två delade variabler antalet in värden som lagts till bufferten och antalet ut som tas bort från bufferten.

C. Implementering av semaforer . I sin artikel om THE multiprogramming system introducerar Dijkstra semaforen sem som en synkroniseringsprimitiv: sem är en heltalsvariabel som endast kan refereras till på två sätt, som visas nedan; var och en är en odelbar operation:

1. P(sem) : Minska sem med 1. Om nu sem < 0 , avbryt processen och lägg den på en lista över avbrutna processer associerade med sem .

2. V(sem) : Öka sem med 1. Om nu sem ≤ 0 , ta bort en av processerna från listan över avbrutna processer associerade med sem , så att dess dynamiska framsteg återigen är tillåtet.

Implementeringen av P och V med avvaktande uttalanden är:

      
          
              
                
          
          
                


      
          
              
                 
                                   
                            
                  P(sem): invänta sant och sedan börja sem: = sem-1; om sem < 0 då w[denna process]: = sann slut ; await ¬w[denna process] hoppa över V(sem): await true sedan börja sem: = sem+1; om sem ≤ 0, välj börja p så att w[ p ]; w[ p : ] = falskt slutslut
          

Här är w en rad processer som väntar eftersom de har avbrutits; initialt, w[p] = falskt för varje process p . Man skulle kunna ändra implementeringen för att alltid väcka den längsta avbrutna processen.

D. Sophämtning i farten . Vid 1975 års sommarskola i Marktoberdorf diskuterade Dijkstra en sopsamlare i farten som en övning för att förstå parallellism. Datastrukturen som används i en konventionell implementering av LISP är en riktad graf där varje nod har högst två utgående kanter, av vilka endera kan saknas: en utgående vänsterkant och en utgående högerkant. Alla noder i grafen måste kunna nås från en känd rot. Att ändra en nod kan resultera i oåtkomliga noder, som inte längre kan användas och kallas skräp . En sopsamlare i farten har två processer: själva programmet och en sopsamlare, vars uppgift är att identifiera sopnoder och lägga upp dem på en gratislista så att de kan användas igen.

Gries ansåg att störningsfrihet kunde användas för att bevisa att sopsamlaren hade rätt. Med hjälp av Dijkstra och Hoare kunde han hålla en presentation i slutet av Sommarskolan, vilket resulterade i en artikel i CACM.

E. Verifiering av läsare/skrivare lösning med semaforer . Courtois et al använder semaforer för att ge två versioner av problemet med läsare/författare, utan bevis. Skrivoperationer blockerar både läsning och skrivning, men läsoperationer kan ske parallellt. Owicki ger ett bevis.

F. Petersons algoritm , en lösning på problemet med ömsesidig uteslutning av två processer, publicerades av Peterson i en tvåsidig artikel. Schneider och Andrews ger ett korrekthetsbevis.

Beroende av störningsfrihet

Bilden nedan, av Ilya Sergey, skildrar flödet av idéer som har implementerats i logiker som handlar om samtidighet. Grunden är störningsfrihet. Filen CSL-Family-Tree (PDF) innehåller referenser. Nedan sammanfattar vi de stora framstegen.

• Rely-Garanti . 1981. Interferensfrihet är inte kompositionsmässigt. Cliff Jones återställer kompositionalitet genom att abstrahera interferens till två nya predikat i en spec: ett rely-villkor registrerar vilken interferens en tråd måste kunna tolerera och ett garantivillkor sätter en övre gräns för den interferens som tråden kan orsaka på sina syskontrådar . Xu et al observerar att Rely-Guarantee är en omformulering av störningsfrihet; Att avslöja sambandet mellan dessa två metoder, säger de, ger en djup förståelse för verifiering av delade variabelprogram.
• CSL . 2004. Separationslogik stöder lokalt resonemang, där specifikationer och bevis för en programkomponent endast nämner den del av minnet som används av komponenten. Concurrent separation logic (CSL) föreslogs ursprungligen av Peter O'Hearn . Vi citerar från: "Owicki-Gries-metoden involverar explicit kontroll av icke-interferens mellan programkomponenter, medan vårt system utesluter interferens på ett implicit sätt, av naturen om hur bevis är konstruerade."
• Härleda samtidiga program . 2005-2007. Feijen och van Gasteren visar hur man använder Owicki-Gries för att designa samtidiga program, men avsaknaden av en teori om framsteg innebär att konstruktioner enbart drivs av säkerhetskrav . Dongol, Goldson, Mooij och Hayes har utökat detta arbete till att inkludera en "framstegslogik" baserad på Chandy och Misras språk Unity , formad för att passa en sekventiell programmeringsmodell. Dongel och Goldson beskriver sin logik för framsteg. Goldson och Dongol visar hur denna logik används för att förbättra processen att designa program, med hjälp av Dekkers algoritm för två processer som ett exempel. Dongol och Mooij presenterar fler tekniker för att härleda program, med Petersons ömsesidiga uteslutningsalgoritm som ett exempel. Dongol och Mooij visar hur man minskar beräkningsoverheaden i formella bevis och härledningar och härleder Dekkers algoritm igen, vilket leder till några nya och enklare varianter av algoritmen. Mooij studerar beräkningsregler för Unitys leads-to- relation. Slutligen ger Dongol och Hayes en teoretisk grund för och bevisar sundheten i processlogiken.
• OGRA . 2015. Lahav och Vafeiadis stärker interferensfrihetskontrollen för att producera (vi citerar från abstraktet) "OGRA, en programlogik som är bra för resonemang om program i release-acquire-fragmentet av C11-minnesmodellen." De ger flera exempel på dess användning, inklusive en implementering av RCU-synkroniseringsprimitiv.
• Kvantprogrammering . 2108. Ying et al utökar störningsfriheten till kvantprogrammering. Svårigheter de möter inkluderar sammanflätad icke-determinism: icke-determinism som involverar kvantmätningar och icke-determinism som introduceras av parallellism som inträffar samtidigt. Författarna verifierar formellt Bravyi-Gosset-Königs parallella kvantalgoritm som löser ett linjärt algebraproblem och ger, säger de, för första gången ett ovillkorligt bevis på en beräkningskvantfördel.
• POG . 2020. Raad et al presenterar POG (Persistent Owicki-Gries), den första programlogiken för resonemang om icke-flyktiga minnesteknologier, närmare bestämt Intel-x86.

Texter som diskuterar störningsfrihet

• On A Method of Multiprogramming , 1999. Van Gasteren och Feijen diskuterar den formella utvecklingen av samtidiga program helt utifrån idén om störningsfrihet.
• On Current Programming, 1997. Schneider använder störningsfrihet som det huvudsakliga verktyget för att utveckla och bevisa samtidiga program. En koppling till tidslogik ges, så godtyckliga säkerhets- och livlighetsegenskaper kan bevisas. Kontrollpredikat undanröjer behovet av hjälpvariabler för resonemang om programräknare.
• Verification of Sequential and Concurrent Programs , 1991, 2009. Denna första text som täcker verifiering av strukturerade samtidiga program, av Apt et al , har gått igenom flera upplagor under flera decennier.
• Concurrency Verification: Introduction to Compositional and Non-Compositional Methods , 2112. De Roever et al tillhandahåller en systematisk och omfattande introduktion till kompositions- och icke-kompositionsbevismetoder för tillståndsbaserad verifiering av samtidiga program

Implementeringar av störningsfrihet

• 1999: Nipkow och Nieto presenterar den första formaliseringen av interferensfrihet och dess kompositionsversion, rely-garantie-metoden, i ett teorembevis: Isabelle/HOL.
• 2005: Ábraháms doktorsavhandling ger ett sätt att bevisa att flertrådade Java-program är korrekta i tre steg: (1) Kommentera programmet för att producera en korrekturskiss, (2) Använd deras verktyg Verger för att automatiskt skapa verifieringsvillkor och (3) Använd satsen prover PVS för att bevisa verifieringsvillkoren interaktivt.
• 2017: Denissen rapporterar om en implementering av Owicki-Gries i programmeringsspråket "verifieringsklar" Dafny . Denissen anmärker på användarvänligheten av Dafny och hans utvidgning av den, vilket gör den extremt lämplig när man lär elever om störningsfrihet. Dess enkelhet och intuitivitet uppväger nackdelen med att vara icke-kompositör. Han listar ett tjugotal institutioner som lär ut störningsfrihet.
• 2017: Amani et al kombinerar tillvägagångssätten från Hoare-Parallel, en formalisering av Owicki-Gries i Isabelle/HOL för ett enkelt medan-språk, och SIMPL, ett generiskt språk inbäddat i Isabelle/HOL, för att tillåta formella resonemang i C-program.
• 2022: Dalvandi et al introducerar den första deduktiva verifieringsmiljön i Isabelle/HOL för C11-liknande svaga minnesprogram, som bygger på Nipkow och Nietos kodning av Owicki–Gries i Isabelles teoremprover.
• 2022: Den här webbsidan beskriver Civl-verifieraren för samtidiga program och ger instruktioner för hur du installerar den på din dator. Den är byggd ovanpå Boogie, en verifierare för sekventiella program. Kragl et al beskriver hur störningsfrihet uppnås i Civl med hjälp av deras nya specifikation idiom, avkastningsinvarianter . Man kan också använda specifikationer i rely-garanti-stilen. Civl erbjuder en kombination av linjär typning och logik som tillåter ekonomiskt och lokalt resonemang om osammanhängande (som separationslogik). Civl är det första systemet som erbjuder förfiningsresonemang på strukturerade samtidiga program.
• 2022. Esen och Rümmer utvecklade TRICERA, ett automatiserat verifieringsverktyg med öppen källkod för C-program. Den är baserad på konceptet med begränsade Horn-satser , och den hanterar program som arbetar på högen med hjälp av en teori om högar. Det finns ett webbgränssnitt för att prova det online. För att hantera samtidighet använder TRICERA en variant av Owicki-Gries bevisregler, med explicita variabler som ska läggas till för att representera tid och klockor.