Algebraic Techniques in Software Verification : Challenges and Opportunities
One of the main application areas and driving forces behind the development of Satisfiability Modulo Theory (SMT) solvers is software verification. The requirements of software verification are somewhat different to other applications of automated reasoning, posing a number of challenges but also pr...
| Κύριοι συγγραφείς: | , , |
|---|---|
| Μορφή: | Conference item |
| Έκδοση: |
2016
|
| _version_ | 1826286754896805888 |
|---|---|
| author | Brain, M Kroening, D McCleeary, R |
| author_facet | Brain, M Kroening, D McCleeary, R |
| author_sort | Brain, M |
| collection | OXFORD |
| description | One of the main application areas and driving forces behind the development of Satisfiability Modulo Theory (SMT) solvers is software verification. The requirements of software verification are somewhat different to other applications of automated reasoning, posing a number of challenges but also providing some interesting opportunities. This paper brings together and summarises the algebras and structures of interest, along with some of the problems that are characteristic of software verification. It is hoped that this will allow computer algebra researchers to assess the applicability of their techniques to this challenging, but rewarding domain. |
| first_indexed | 2024-03-07T01:48:25Z |
| format | Conference item |
| id | oxford-uuid:9939886a-2dc0-470a-925e-6faab900fbdb |
| institution | University of Oxford |
| last_indexed | 2024-03-07T01:48:25Z |
| publishDate | 2016 |
| record_format | dspace |
| spelling | oxford-uuid:9939886a-2dc0-470a-925e-6faab900fbdb2022-03-27T00:12:50ZAlgebraic Techniques in Software Verification : Challenges and OpportunitiesConference itemhttp://purl.org/coar/resource_type/c_5794uuid:9939886a-2dc0-470a-925e-6faab900fbdbSymplectic Elements at Oxford2016Brain, MKroening, DMcCleeary, ROne of the main application areas and driving forces behind the development of Satisfiability Modulo Theory (SMT) solvers is software verification. The requirements of software verification are somewhat different to other applications of automated reasoning, posing a number of challenges but also providing some interesting opportunities. This paper brings together and summarises the algebras and structures of interest, along with some of the problems that are characteristic of software verification. It is hoped that this will allow computer algebra researchers to assess the applicability of their techniques to this challenging, but rewarding domain. |
| spellingShingle | Brain, M Kroening, D McCleeary, R Algebraic Techniques in Software Verification : Challenges and Opportunities |
| title | Algebraic Techniques in Software Verification : Challenges and Opportunities |
| title_full | Algebraic Techniques in Software Verification : Challenges and Opportunities |
| title_fullStr | Algebraic Techniques in Software Verification : Challenges and Opportunities |
| title_full_unstemmed | Algebraic Techniques in Software Verification : Challenges and Opportunities |
| title_short | Algebraic Techniques in Software Verification : Challenges and Opportunities |
| title_sort | algebraic techniques in software verification challenges and opportunities |
| work_keys_str_mv | AT brainm algebraictechniquesinsoftwareverificationchallengesandopportunities AT kroeningd algebraictechniquesinsoftwareverificationchallengesandopportunities AT mccleearyr algebraictechniquesinsoftwareverificationchallengesandopportunities |