Owiczki és Gries fogalmazta meg 1976-ban az interferenciamentesség követelményét [[???Owi Gri 76]]. Két szekvenciális folyamat interferenciamentes, ha az egyik helyességbizonyításában alkalmazott kritikus feltételek teljesülését a másik folyamat atomi műveletei nem érvénytelenítik. Lamport a monoton predikátum fogalmának bevezetésekor hasonló követelményt támasztott az együttműködő folyamatok kölcsönhatására [[???Lam 77]]. Ezek a feltételek egy-egy ill. atomi lépésből álló folyamatpár esetén az összetevők szekvenciális helyességének igazolásához szükséges bizonyítási lépéseken túlmenően a párhuzamos program parciális helyességének belátásához további bizonyítási lépést tettek szükségessé. A módszer alkalmazásakor további nehézséget okozhat az is, hogy a párhuzamos program komponenseinek állapota nem egyértelműen meghatározott az összetett program változóinak értéke által, ezért a bizonyítások során ún. segédváltozókat vagy más néven kontrollváltozókat is be kell vezetni. A segédváltozók a program futása során értéket kapnak, de értéküket csak a helyességbizonyítás során használjuk fel. Az alkalmasan megválasztott segédváltozók értéke alapján meghatározhatóvá válik, hogy melyik összetevők felelősek a korábbi állapotátmenetekért, az egyes folyamatok mely atomi művelet végrehajtásánál tartanak. Ugyanezen célt szolgálják a Lamport által bevezetett kontrollváltozók [[???Lam 90]], melyek az egyes atomi műveletekhez rendelt logikai változók. Egy művelet kontrollváltozói pontosan akkor vesznek fel logikai értéket, amikor az adott művelet végrehajtása megkezdődik, éppen folyamatban van, illetve véget ért.

van Lamsweerde és Sintzoff [[???Lam Sin 79]] a párhuzamos program szerkezetét a folyamatok halmaza helyett atomi akciók halmazaként, iteratív programstruktúra alakjában rögzíti. Megmutatják, hogy ún. explicit szekvencializálási technikával szekvenciális összetevők is felbonthatóak atomi műveletek halmazára. Modelljükben a megoldás levezetésén és nem a kész programok helyességbizonyításán van a hangsúly. Az iteratív program ciklusinvariánsa mint a párhuzamos program globális invariánsa jelenik meg és nagyban megkönnyíti biztonságossági feltételek megfogalmazását és bizonyítását. Modelljükben egyes haladási tulajdonságok kifejezésére és bizonyítására is eszközt adnak, pl. meghatározzák az adott végfeltétel elérésének leggyengébb előfeltételét, amelyet a Dijkstra által definiált leggyengébb előfeltételből [[???Dij 76]] felépített funkcionálok fixpontjainak kiszámításával határoznak meg. Módszert adnak arra is, hogy hogyan határozzuk meg egy adott invariáns biztosítását garantáló szinkronizációs feltételeket, hogyan transzformáljuk a programot olyan alakba, hogy az invariánst, és így a szinkronizációs feltételeket is a lehető leggyengébbre választhassuk meg. Megadják holtpontmentes és kiéheztetésmentes program szintézisének módszerét. A UNITYUnbounded Nondeterministic Iterative Transformations-ben [[???Cha Mis 89]] és az általunk megfogalmazott modellben definiált absztrakt program struktúrája megegyezik van Lamsweerde és Sintzoff párhuzamos programjainak stuktúrájával.

Párhuzamos programok haladási feltételeinek leírására alkalmas predikátumtranszformereket rajtuk kívül sokan megfogalmaztak. A leggyengébb előfeltételből felépített monoton funkcionálok legkisebb és legnagyobb fixpontjainak együttes alkalmazásával definiálja Park iteratív programszerkezetek haladási tulajdonságait pártatlan ütemezés feltételezése mellett. Hasonló predikátumtranszformert alkot Morris rekurzív programok haladási tulajdonságainak leírására. Számos, egyes speciális haladási tulajdonságokat különböző pártatlansági feltételek mellett kifejező predikátumtranszformert ad meg fixpontos alakban Flon és Suzuki [[???Flo Suz 81]], Francez [[???Fra 86]], Lukkien [[???Luk Sne 92]].

van Lamsweerde és Sintzoff eredményeit alkalmazza Andrews konkurens programok szintézisére [[???And 91]] azzal a különbséggel, hogy a programszerkezetet nem iteratív formában definiálja, hanem visszatér az Owiczki-Gries modell programfogalmához. Módszere a megoldás lépésenkénti finomításán alapszik. Először a megoldás szerkezetét definiálja a feladat meghatározásával egyidejűleg, azaz megadja a megoldásban szereplő folyamatokat, azok közös állapotterét és a kölcsönhatásukat korlátozó invariánst. Második lépésként definiálja az egyes folyamatok szekvenciális vázát a bizonyítás vázlatával együtt. A harmadik lépésben van Lamsweerde és Sintzoff módszerével meghatározza a szinkronizációs őrfeltételeket a leggyengébb előfeltétel kalkulus alapján. Végül implementálja az absztrakt programot egy konkrét nyelven és architektúrán. Andrews részletesen elemzi azokat a heurisztikus módszereket, amelyekkel biztosítható folyamatok interferenciamentessége. Könnyű garantálni, hogy két folyamat nem interferál egymással, ha azok diszjunkt változókon dolgoznak, azaz amelyik változót az egyik folyamat ír, azt a másik folyamat egyáltalán nem használja. Ha a változók átfedik egymást, akkor a másik folyamat utasításainak hatását is figyelembe véve gyengíthetjük a bizonyítási vázlat kritikus feltételeit. Jól alkalmazható a globális invariánsok módszere, mikor arra törekszünk, hogy az egyes atomi utasítások elő- és utófeltételeit a globális invariáns és egy olyan állítás konjunkciójaként írjuk fel, amely állítás csak a folyamat lokális változóitól vagy legfeljebb csak olyan változóktól függ, amelyet csak az adott folyamat ír. Szinkronizációt is alkalmazhatunk az interferencia elkerülésére, oly módon, hogy őrfeltétellel korlátozzuk az adott kritikus állítást érvénytelenítő, interferenciát okozó utasítás végrehajtásának lehetőségét olyan állapotokra, amikor interferencia nem jön létre. Andrews definiálja a finom atomicitás és a durva atomicitás fogalmát. Az atomi akciók szintjének megválasztása kihat arra, hogy a helyességbizonyítás szempontjából mi számít kritikus állításnak és egyben meghatározza az absztrakt program implementációjának lehetséges hatékonyságát. Programozási tételek szintézise során törekedni fogunk arra, hogy a tételek végső alakját az Andrews által megfogalmazott legfinomabb atomicitás feltételezése mellett adjuk meg és minél gyengébb szinkronizációs feltételeket határozzunk meg.