Vi presenterar en metod för att verifiera riktigheten av parallella program som utför komplexa numeriska beräkningar, inklusive beräkningar som involverar flyttal aritmetik. Metoden kräver att en sekventiell version av programmet tillhandahålls, att fungera som specifikation för parallellen. Den viktigaste idén är att använda modellkontroll, tillsammans med symboliskt utförande, för att fastställa likvärdigheten av de två programmen.
Siegel m.fl. REF tillämpar modellkontroll och symbolisk körning för att verifiera likvärdigheten av sekventiella och parallella versioner av ett program.
Using model checking with symbolic execution to verify parallel numerical programs
{'venue': "ISSTA '06", 'journal': None, 'mag_field_of_study': ['Computer Science']}