Abstract
We focus on the verification of stabilizing programs using SMT solvers. SMT solvers have the potential to convert the verification problem into a satisfiability problem of a Boolean formula and utilize efficient techniques to determine whether it is satisfiable. We focus on utilizing techniques from bounded model checking to determine whether the given program is stabilizing. We illustrate our approach using three case studies. We also identify tradeoffs between verification with SMT solvers and existing approaches. © Springer-Verlag 2013.
Author supplied keywords
Cite
CITATION STYLE
Chen, J., & Kulkarni, S. (2013). SMT-based model checking for stabilizing programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7730 LNCS, pp. 393–407). https://doi.org/10.1007/978-3-642-35668-1_27
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
