Advertisement
Published in:
2006 | OriginalPaper | Chapter
Program Verification Through Computer Algebra
Author : Zhou Chaochen
Published in: Formal Methods and Software Engineering
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
This is to advocate the approach to reducing program verification to the algebraic symbolic computation. Recent advances indicate that various verification problems can be reduced to semi-algebraic systems (SAS for short), and resolved through computer algebra tools. In this talk, we report our encouraging attempts at applying DISCOVERER to program termination analysis and state reachability computation. DISCOVERER is a Maple program implementing an algorithm of real solution classification and isolation for SAS, which is based on the discovery of complete discrimination systems of parametric polynomials. The talk also concludes that this approach deserves further attention from the program verification community.
For theoretical and technical details of the work, we refer the reader to [1,2,3,4,5].