Abstrakt. Formellt verifiera egenskaper hos program som manipulerar matriser i loopar är datoriskt utmanande. I denna uppsats fokuserar vi på en användbar klass av sådana program, och presentera en ny egendomsdriven verifieringsmetod som först drar slutsatsen array access mönster i loopar med hjälp av enkla heuristik, och sedan använder denna information för att kompositionellt bevisa universellt kvantifierade påståenden om arrayer. Specifikt identifierar vi plattor av array tillträde mönster i en slinga, och använder tiling information för att minska problemet med att kontrollera ett kvantifierat påstående i slutet av en slinga till ett induktivt argument som endast kontrollerar en del av påståendet för en enda iteration av slingan kroppen. Vi visar att denna metod kan utvidgas till program med sekventiellt komponerade slingor och inbäddade slingor också. Vi har implementerat vår metod i ett verktyg som heter Tiler. De första experimenten visar att Tiler överträffar flera toppmoderna verktyg på en serie intressanta riktmärken.
Tiling REF, en egendomsdriven verifieringsteknik, övervinner dessa begränsningar för en klass av program genom att sluta array access mönster i loopar. Men att identifiera plattor av array accesses är i sig ett svårt problem, och tillvägagångssättet är för närvarande baserat på heuristik som utvecklats genom att observera intressanta mönster.
Verifying Array Manipulating Programs by Tiling
{'venue': 'ArXiv', 'journal': 'ArXiv', 'mag_field_of_study': ['Computer Science']}