Paper Info
Title
Scalable Automated Verification via Expert-System Guided Transformations
Abstract
Transformation-based verification has been proposed to synergistically leverage various transformations to successively simplify and decompose large problems to ones which may be formally discharged. While powerful, such systems require a fair amount of user sophistication and experimentation to yield greatest benefits - every verification problem is different, hence the most efficient transformation flow differs widely from problem to problem. Finding an efficient proof strategy not only enables exponential reductions in computational resources, it often makes the difference between obtaining a conclusive result or not. In this paper, we propose the use of an expert system to automate this proof strategy development process. We discuss the types of rules used by the expert system, and the type of feedback necessary between the algorithms and expert system, all oriented towards yielding a conclusive result with minimal resources. Experimental results are provided to demonstrate that such a system is able to automatically discover efficient proof strategies, even on large and complex problems with more than 100,000 state elements in their respective cones of influence. These results also demonstrate numerous types of algorithmic synergies that are critical to the automation of such complex proofs.
Year
DOI
Venue
2004
10.1007/978-3-540-30494-4_12
Lecture Notes in Computer Science
Keywords
Field
DocType
expert system,development process
Algorithmics,Computer science,Computer Aided Design,Expert system,Proof theory,Automation,Theoretical computer science,Mathematical proof,Formal methods,Scalability,Distributed computing
Conference
Volume
ISSN
Citations 
3312
0302-9743
41
PageRank 
References 
Authors
1.69
15
5
Name
Order
Citations
PageRank
Hari Mony118613.30
Jason Baumgartner231323.36
Viresh Paruthi337121.84
Robert Kanzelman41076.16
Andreas Kuehlmann51217105.62