AVR: Abstractly Verifying Reachability
Aman Goel, Karem A. Sakallah
Abstract
We present AVR, a push-button model checker for verifying state transition systems directly at the source-code level. AVR uses information embedded in the word-level syntax of the design representation to automatically perform scalable model checking by combining a novel syntax-guided abstraction-refinement technique with a word-level implementation of the IC3 algorithm. AVR provides independently-verifiable certificates that offer provable assurance and are easy to relate to the word-level system. Moreover, proof certificates can be further used in innovative ways to extract key design information and are useful in a growing number of applications.
Topics & Concepts
Computer scienceReachabilityProgramming languageSyntaxModel checkingWord (group theory)ScalabilityAbstract syntax treeKey (lock)Formal verificationVerifiable secret sharingRepresentation (politics)AbstractionTheoretical computer scienceState (computer science)Artificial intelligenceParsingSet (abstract data type)DatabaseOperating systemEpistemologyLinguisticsLawPhilosophyPolitical sciencePoliticsFormal Methods in VerificationSafety Systems Engineering in AutonomySecurity and Verification in Computing