Abstrakt. Uttömmande söktekniker som modellkontroll och symboliskt utförande är otillräckliga för att upptäcka fel i samtidiga program. I detta arbete presenterar vi en abstraktionsstyrd symbolisk exekveringsteknik som snabbt upptäcker fel i samtidiga program som uppstår från trådscheman och indatavärden. Ett abstrakt system genereras som innehåller en uppsättning av viktiga program platser som är relevanta för att testa genomförbarheten av ett möjligt fel i programmet. Vi vägleder en symbolisk körning längs platser i det abstrakta systemet i ett försök att generera en motsvarande genomförbar körning spår till felplatsen. En kombination av heuristik används för att automatiskt ranka tråd och data icke-determinism för att styra utförandet. Vi visar empiriskt att abstraktion-styrd symboliskt utförande genererar genomförbara genomförandevägar i det faktiska systemet för att hitta konvergensfel på några sekunder där uttömmande symboliskt utförande misslyckas med att hitta samma fel på en timme.
En experimentell studie för att utvärdera en abstraktion-styrd symbolisk exekveringsteknik som upptäcker fel i samtidiga program, beskrivs i REF.
Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution
{'venue': 'SPIN', 'journal': None, 'mag_field_of_study': ['Computer Science']}