Automatic abstraction in symbolic trajectory evaluation
Symbolic trajectory evaluation (STE) is a model checking technology based on symbolic simulation over a lattice of abstract state sets. The STE algorithm operates over families of these abstractions encoded by Boolean formulas, enabling verification with many different abstraction cases in a single...
| Príomhchruthaitheoirí: | , , , |
|---|---|
| Formáid: | Conference item |
| Foilsithe / Cruthaithe: |
IEEE
2007
|
| _version_ | 1826297235601620992 |
|---|---|
| author | Adams, S Bjoerk, M Melham, T Seger, C |
| author_facet | Adams, S Bjoerk, M Melham, T Seger, C |
| author_sort | Adams, S |
| collection | OXFORD |
| description | Symbolic trajectory evaluation (STE) is a model checking technology based on symbolic simulation over a lattice of abstract state sets. The STE algorithm operates over families of these abstractions encoded by Boolean formulas, enabling verification with many different abstraction cases in a single modelchecking run. This provides a flexible way to achieve partitioned data abstraction. It is usually called "symbolic indexing' and is widely used in memory verification, but has seen relatively limited adoption elsewhere, primarily because users typically have to create the right indexed family of abstractions manually. This work provides the first known algorithm that automatically computes these partitioned abstractions given a reference-model specification. Our experimental results show that this approach not only simplifies memory verification, but also enables handling completely different designs fully automatically. |
| first_indexed | 2024-03-07T04:28:29Z |
| format | Conference item |
| id | oxford-uuid:cd7ccf44-4911-4f37-8645-1426202096ce |
| institution | University of Oxford |
| last_indexed | 2024-03-07T04:28:29Z |
| publishDate | 2007 |
| publisher | IEEE |
| record_format | dspace |
| spelling | oxford-uuid:cd7ccf44-4911-4f37-8645-1426202096ce2022-03-27T07:29:01ZAutomatic abstraction in symbolic trajectory evaluationConference itemhttp://purl.org/coar/resource_type/c_5794uuid:cd7ccf44-4911-4f37-8645-1426202096ceSymplectic Elements at OxfordIEEE2007Adams, SBjoerk, MMelham, TSeger, CSymbolic trajectory evaluation (STE) is a model checking technology based on symbolic simulation over a lattice of abstract state sets. The STE algorithm operates over families of these abstractions encoded by Boolean formulas, enabling verification with many different abstraction cases in a single modelchecking run. This provides a flexible way to achieve partitioned data abstraction. It is usually called "symbolic indexing' and is widely used in memory verification, but has seen relatively limited adoption elsewhere, primarily because users typically have to create the right indexed family of abstractions manually. This work provides the first known algorithm that automatically computes these partitioned abstractions given a reference-model specification. Our experimental results show that this approach not only simplifies memory verification, but also enables handling completely different designs fully automatically. |
| spellingShingle | Adams, S Bjoerk, M Melham, T Seger, C Automatic abstraction in symbolic trajectory evaluation |
| title | Automatic abstraction in symbolic trajectory evaluation |
| title_full | Automatic abstraction in symbolic trajectory evaluation |
| title_fullStr | Automatic abstraction in symbolic trajectory evaluation |
| title_full_unstemmed | Automatic abstraction in symbolic trajectory evaluation |
| title_short | Automatic abstraction in symbolic trajectory evaluation |
| title_sort | automatic abstraction in symbolic trajectory evaluation |
| work_keys_str_mv | AT adamss automaticabstractioninsymbolictrajectoryevaluation AT bjoerkm automaticabstractioninsymbolictrajectoryevaluation AT melhamt automaticabstractioninsymbolictrajectoryevaluation AT segerc automaticabstractioninsymbolictrajectoryevaluation |