Efficient CTL Verification via Horn Constraints Solving
The use of temporal logics has long been recognised as a fundamental approach to the formal specification and verification of reactive systems. In this paper, we take on the problem of automatically verifying a temporal property, given by a CTL formula, for a given (possibly infinite-state) program....
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2016-07-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1607.04456v1 |
| _version_ | 1811255964812181504 |
|---|---|
| author | Tewodros A. Beyene Corneliu Popeea Andrey Rybalchenko |
| author_facet | Tewodros A. Beyene Corneliu Popeea Andrey Rybalchenko |
| author_sort | Tewodros A. Beyene |
| collection | DOAJ |
| description | The use of temporal logics has long been recognised as a fundamental approach to the formal specification and verification of reactive systems. In this paper, we take on the problem of automatically verifying a temporal property, given by a CTL formula, for a given (possibly infinite-state) program. We propose a method based on encoding the problem as a set of Horn constraints. The method takes a program, modeled as a transition system, and a property given by a CTL formula as input. It first generates a set of forall-exists quantified Horn constraints and well-foundedness constraints by exploiting the syntactic structure of the CTL formula. Then, the generated set of constraints are solved by applying an off-the-shelf Horn constraints solving engine. The program is said to satisfy the property if and only if the generated set of constraints has a solution. We demonstrate the practical promises of the method by applying it on a set of challenging examples. Although our method is based on a generic Horn constraint solving engine, it is able to outperform state-of-art methods specialised for CTL verification. |
| first_indexed | 2024-04-12T17:33:27Z |
| format | Article |
| id | doaj.art-f41d8663843647a8a0f102fd3d93a6a4 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-04-12T17:33:27Z |
| publishDate | 2016-07-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-f41d8663843647a8a0f102fd3d93a6a42022-12-22T03:23:05ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802016-07-01219Proc. HCVS201611410.4204/EPTCS.219.1:5Efficient CTL Verification via Horn Constraints SolvingTewodros A. Beyene0Corneliu Popeea1Andrey Rybalchenko2 fortiss GmbH, Munich, Germany CQSE GmbH, Munich, Germany Microsoft Research, Cambridge, UK The use of temporal logics has long been recognised as a fundamental approach to the formal specification and verification of reactive systems. In this paper, we take on the problem of automatically verifying a temporal property, given by a CTL formula, for a given (possibly infinite-state) program. We propose a method based on encoding the problem as a set of Horn constraints. The method takes a program, modeled as a transition system, and a property given by a CTL formula as input. It first generates a set of forall-exists quantified Horn constraints and well-foundedness constraints by exploiting the syntactic structure of the CTL formula. Then, the generated set of constraints are solved by applying an off-the-shelf Horn constraints solving engine. The program is said to satisfy the property if and only if the generated set of constraints has a solution. We demonstrate the practical promises of the method by applying it on a set of challenging examples. Although our method is based on a generic Horn constraint solving engine, it is able to outperform state-of-art methods specialised for CTL verification.http://arxiv.org/pdf/1607.04456v1 |
| spellingShingle | Tewodros A. Beyene Corneliu Popeea Andrey Rybalchenko Efficient CTL Verification via Horn Constraints Solving Electronic Proceedings in Theoretical Computer Science |
| title | Efficient CTL Verification via Horn Constraints Solving |
| title_full | Efficient CTL Verification via Horn Constraints Solving |
| title_fullStr | Efficient CTL Verification via Horn Constraints Solving |
| title_full_unstemmed | Efficient CTL Verification via Horn Constraints Solving |
| title_short | Efficient CTL Verification via Horn Constraints Solving |
| title_sort | efficient ctl verification via horn constraints solving |
| url | http://arxiv.org/pdf/1607.04456v1 |
| work_keys_str_mv | AT tewodrosabeyene efficientctlverificationviahornconstraintssolving AT corneliupopeea efficientctlverificationviahornconstraintssolving AT andreyrybalchenko efficientctlverificationviahornconstraintssolving |