Abstrakt. Antalet interleavings av en samtidig program gör automatisk analys av sådan programvara mycket svårt. Moderna multiprocessorers utförandemodeller gör detta problem ännu svårare. Modellering program exekveringar med partiella order snarare än interleavings behandlar båda frågorna: vi får en effektiv kodning i heltal skillnad logik för begränsad modellkontroll som möjliggör första gången formell verifiering av utplacerade samtidiga systemkod. Vi implementerade kodningen i CBMC-verktyget och presenterar experiment över ett brett spektrum av minnesmodeller, inklusive SC, Intel x86 och IBM Power. Våra experiment inkluderar kärndelar av PostgreSQL, Linuxkärnan och Apache HTTP-servern.
Alglave m.fl. REF introducerar en symbolisk kodning för att verifiera samtidig programvara över en rad minnesmodeller, inklusive SC, TSO och PSO.
Partial Orders for Efficient Bounded Model Checking of Concurrent Software ⋆
{'venue': 'CAV', 'journal': None, 'mag_field_of_study': ['Computer Science']}