Symbolic Representation and Constraint Reasoning in Invariant Checking (bibtex)
by
Abstract:
Tools for formal verification of complex systems often encounter problems of infinite size, making solutions with explicit representations impossible. Even for finite systems, formal verification is often infeasible when expecting an answer in reasonable time due to exponential complexity of the underlying algorithms. This report demonstrates the occurrence of such complexity challenges in our verification tool, which is based on graph transformation systems and inductive invariants. As two orthogonal approaches to such challenges, the report explains symbolic representation for negative application conditions and constraint reasoning. Both techniques have already been seen to significantly reduce the algorithm�s runtime for specific examples.
Reference:
Symbolic Representation and Constraint Reasoning in Invariant Checking (Johannes Dyck), Technical report 83, Proceedings of the 7th Ph.D. Retreat of the HPI Research School on Service-oriented Systems Engineering, Hasso Plattner Institute, University of Potsdam (Fall 2013 Workshop), 2014.
Bibtex Entry:
@TechReport{DyckFK13,
AUTHOR = {Dyck, Johannes},
TITLE = {{Symbolic Representation and Constraint Reasoning in Invariant Checking}},
YEAR = {2014},
NUMBER = {83},
PAGES = {25-35},
INSTITUTION = {Proceedings of the 7th Ph.D. Retreat of the HPI Research School on Service-oriented Systems Engineering, Hasso Plattner Institute, University of Potsdam (Fall 2013 Workshop)},
URL = {http://opus.kobv.de/ubp/volltexte/2014/6349/pdf/tbhpi83.pdf},
ABSTRACT = {Tools for formal verification of complex systems often encounter problems of infinite
size, making solutions with explicit representations impossible. Even for finite systems,
formal verification is often infeasible when expecting an answer in reasonable time due
to exponential complexity of the underlying algorithms. This report demonstrates the occurrence of such complexity challenges in our verification tool, which is based on graph transformation systems and inductive invariants. As two orthogonal approaches to such challenges, the report explains symbolic representation for negative application conditions and constraint reasoning. Both techniques have already been seen to significantly reduce the algorithm\^{a}��s runtime for specific examples.}
}
Powered by bibtexbrowser