Abstrakt. Vi presenterar en statisk analys av Abstract Interpretation för att kontrollera run-time fel i parallella C-program. Efter vårt arbete med Astrée fokuserar vi på inbäddade kritiska program utan rekursion eller dynamisk minnesallokering, men utökar analysen till en statisk uppsättning trådar. Vår metod itererar en något modifierad icke-parallellanalys över varje tråd i tur och ordning, tills trådinterferenserna stabiliseras. Vi bevisar sundheten i metoden med avseende på en sekventiell konsekvent semantik och en rimlig svagt konsekvent minnessemantik. Vi visar sedan hur man tar hänsyn till ömsesidig uteslutning och gängprioriteringar genom uppdelning över schemaläggningstillståndet. Vi presenterar preliminära experimentella resultat som analyserar ett verkligt program med vår prototyp, Thésée, och demonstrerar skalbarheten i vårt tillvägagångssätt.
Miné REF beskriver en utvidgning av abstrakt tolkning till program med ett fast antal trådar och delat minne.
Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs
{'venue': 'ESOP', 'journal': None, 'mag_field_of_study': ['Computer Science']}