Abstrakt. Verifiera samtidiga program är utmanande eftersom antalet tråd interleavevings som behöver utforskas kan vara enorm även för måttliga program. Vi presenterar en kartesiska semantik som minskar mängden icke-determinism i samtidiga program genom att fördröja onödiga sammanhang switchar. Med hjälp av denna semantik konstruerar vi en ny dynamisk partiell orderreduktionsalgoritm. Den kartesiska semantiken kan användas för att skapa andra partiell-order reduktionsalgoritmer och kan också användas som grund för abstrakt tolkning. Vi har implementerat vår algoritm och utvärderat den på en liten uppsättning riktmärken. Våra preliminära experimentella resultat visar en betydande potentiell besparing i antalet utforskade tillstånd och övergångar.
Gueta m.fl. REF föreslog Cartesian partiell orderreduktion, vilket minskar sökytan genom att försena onödiga sammanhangsbrytare med hjälp av Cartesian vektorer.
Cartesian partial-order reduction
{'venue': 'SPIN 2007. LNCS', 'journal': None, 'mag_field_of_study': ['Computer Science']}