Abstrakt. Många vanliga statiska kodkontroller gör ett antal kompromisser för att förbättra automatisering, prestanda och noggrannhet. Dessa kompromisser inkluderar inte kontrollera vissa program egenskaper samt göra implicita, osunda antaganden. Följaktligen ger resultaten av sådana statiska kontroller inte definitiva garantier om program korrekthet, vilket gör det oklart vilka egenskaper som återstår att testa. Vi föreslår en teknik för gemensam verifiering och provning som gör kompromisser med statiska kontroller så tydliga att de kan kompenseras genom kompletterande kontroller eller tester. Våra experiment tyder på att vår teknik hittar fler fel och bevisar fler egenskaper än statisk kontroll ensam, testning ensam, och kombinationer som inte uttryckligen dokumenterar de kompromisser som gjorts av statiska kontroller. Vår teknik är också användbar för att få små testsviter för delvis verifierade program.
REF föreslogs för att slutföra resultaten av statiska kontroller med dynamisk symbolisk körning med Pex.
Collaborative Verification and Testing with Explicit Assumptions
{'venue': 'FM', 'journal': None, 'mag_field_of_study': ['Computer Science']}