Abstrakt. I detta dokument studeras problemet med att formellt kontrollera tidsmässiga egenskaper hos samtidiga datatyper. Konkurrenta datatyper är implementationer av klassiska dataabstractioner, speciellt utformade för att utnyttja parallellismen som finns i multiprocessorarkitekturer. Korrektheten hos samtidiga datatyper är avgörande för den övergripande korrektheten hos klientprogramvaran. Den största svårigheten att resonera om samtidiga datatyper beror på samtidig användning av ostrukturerad konvergens och dynamiskt minne. Det första bidraget från detta papper är användningen av avdragsgilla tidsverifieringsmetoder, särskilt kontrolldiagram, berikade med resonemang om dynamiskt minne. Bevis med hjälp av verifieringsdiagram bryts ned i en begränsad samling av kontrollförhållanden. Vårt andra bidrag är ett beslutsförfarande som blandar minnesregioner, pekare och lisp-liknande listor med lås, vilket möjliggör automatisk verifiering av de genererade verifieringsförhållandena. Vi illustrerar våra tekniker som visar säkerhet och livlighet egenskaper lås-koppling samtidiga listor.
Huvudfokus i vårt tidigare arbete REF var beslutsförfarande för samtidiga listor.
Decision Procedures for the Temporal Verification of Concurrent Lists
{'venue': 'ICFEM', 'journal': None, 'mag_field_of_study': ['Computer Science']}