Synthesizing Modular Invariants for Synchronous Code
In this paper, we explore different techniques to synthesize modular invariants for synchronous code encoded as Horn clauses. Modular invariants are a set of formulas that characterizes the validity of predicates. They are very useful for different aspects of analysis, synthesis, testing and program...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2014-12-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1412.1152v1 |
| _version_ | 1819057468369534976 |
|---|---|
| author | Pierre-Loic Garoche Arie Gurfinkel Temesghen Kahsai |
| author_facet | Pierre-Loic Garoche Arie Gurfinkel Temesghen Kahsai |
| author_sort | Pierre-Loic Garoche |
| collection | DOAJ |
| description | In this paper, we explore different techniques to synthesize modular invariants for synchronous code encoded as Horn clauses. Modular invariants are a set of formulas that characterizes the validity of predicates. They are very useful for different aspects of analysis, synthesis, testing and program transformation. We describe two techniques to generate modular invariants for code written in the synchronous dataflow language Lustre. The first technique directly encodes the synchronous code in a modular fashion. While in the second technique, we synthesize modular invariants starting from a monolithic invariant. Both techniques, take advantage of analysis techniques based on property-directed reachability. We also describe a technique to minimize the synthesized invariants. |
| first_indexed | 2024-12-21T13:39:47Z |
| format | Article |
| id | doaj.art-ed61628b2fe24c9c829f5bf91ea72196 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-21T13:39:47Z |
| publishDate | 2014-12-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-ed61628b2fe24c9c829f5bf91ea721962022-12-21T19:02:04ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802014-12-01169Proc. HCVS 2014193010.4204/EPTCS.169.4:1Synthesizing Modular Invariants for Synchronous CodePierre-Loic Garoche0Arie Gurfinkel1Temesghen Kahsai2 Onera, The French Aerospace Lab SEI / CMU NASA Ames / CMU In this paper, we explore different techniques to synthesize modular invariants for synchronous code encoded as Horn clauses. Modular invariants are a set of formulas that characterizes the validity of predicates. They are very useful for different aspects of analysis, synthesis, testing and program transformation. We describe two techniques to generate modular invariants for code written in the synchronous dataflow language Lustre. The first technique directly encodes the synchronous code in a modular fashion. While in the second technique, we synthesize modular invariants starting from a monolithic invariant. Both techniques, take advantage of analysis techniques based on property-directed reachability. We also describe a technique to minimize the synthesized invariants.http://arxiv.org/pdf/1412.1152v1 |
| spellingShingle | Pierre-Loic Garoche Arie Gurfinkel Temesghen Kahsai Synthesizing Modular Invariants for Synchronous Code Electronic Proceedings in Theoretical Computer Science |
| title | Synthesizing Modular Invariants for Synchronous Code |
| title_full | Synthesizing Modular Invariants for Synchronous Code |
| title_fullStr | Synthesizing Modular Invariants for Synchronous Code |
| title_full_unstemmed | Synthesizing Modular Invariants for Synchronous Code |
| title_short | Synthesizing Modular Invariants for Synchronous Code |
| title_sort | synthesizing modular invariants for synchronous code |
| url | http://arxiv.org/pdf/1412.1152v1 |
| work_keys_str_mv | AT pierreloicgaroche synthesizingmodularinvariantsforsynchronouscode AT ariegurfinkel synthesizingmodularinvariantsforsynchronouscode AT temesghenkahsai synthesizingmodularinvariantsforsynchronouscode |