Trigger Selection Strategies to Stabilize Program Verifiers
SMT-based program verifiers often suffer from the so-called butterfly effect, in which minor modifications to the program source cause significant instabilities in verification times, which in turn may lead to spurious verification failures and a degraded user experience. This paper identifies match...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | en_US |
| Published: |
Springer International Publishing
2021
|
| Online Access: | https://hdl.handle.net/1721.1/103950.2 https://orcid.org/0000-0002-1900-3901 |
| _version_ | 1811095687182417920 |
|---|---|
| author | Leino, K. Rustan M. Pit-Claudel, Clément |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Leino, K. Rustan M. Pit-Claudel, Clément |
| author_sort | Leino, K. Rustan M. |
| collection | MIT |
| description | SMT-based program verifiers often suffer from the so-called butterfly effect, in which minor modifications to the program source cause significant instabilities in verification times, which in turn may lead to spurious verification failures and a degraded user experience. This paper identifies matching loops (ill-behaved quantifiers causing an SMT solver to repeatedly instantiate a small set of quantified formulas) as a significant contributor to these instabilities, and describes some techniques to detect and prevent them. At their core, the contributed techniques move the trigger selection logic away from the SMT solver and into the high-level verifier: this move allows authors of verifiers to annotate, rewrite, and analyze user-written quantifiers to improve the solver’s performance, using information that is easily available at the source level but would be hard to extract from the heavily encoded terms that the solver works with. The paper demonstrates three core techniques (quantifier splitting, trigger sharing, and matching loop detection) by extending the Dafny verifier with its own trigger selection routine, and demonstrates significant predictability and performance gains on both Dafny’s test suite and large verification efforts using Dafny. |
| first_indexed | 2024-09-23T16:24:30Z |
| format | Article |
| id | mit-1721.1/103950.2 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T16:24:30Z |
| publishDate | 2021 |
| publisher | Springer International Publishing |
| record_format | dspace |
| spelling | mit-1721.1/103950.22022-03-30T18:04:13Z Trigger Selection Strategies to Stabilize Program Verifiers Leino, K. Rustan M. Pit-Claudel, Clément Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Pit-Claudel, Clement F. SMT-based program verifiers often suffer from the so-called butterfly effect, in which minor modifications to the program source cause significant instabilities in verification times, which in turn may lead to spurious verification failures and a degraded user experience. This paper identifies matching loops (ill-behaved quantifiers causing an SMT solver to repeatedly instantiate a small set of quantified formulas) as a significant contributor to these instabilities, and describes some techniques to detect and prevent them. At their core, the contributed techniques move the trigger selection logic away from the SMT solver and into the high-level verifier: this move allows authors of verifiers to annotate, rewrite, and analyze user-written quantifiers to improve the solver’s performance, using information that is easily available at the source level but would be hard to extract from the heavily encoded terms that the solver works with. The paper demonstrates three core techniques (quantifier splitting, trigger sharing, and matching loop detection) by extending the Dafny verifier with its own trigger selection routine, and demonstrates significant predictability and performance gains on both Dafny’s test suite and large verification efforts using Dafny. 2021-09-23T19:05:25Z 2016-08-17T20:11:11Z 2021-09-23T19:05:25Z 2016-07 Article http://purl.org/eprint/type/ConferencePaper 978-3-319-41527-7 978-3-319-41528-4 0302-9743 1611-3349 https://hdl.handle.net/1721.1/103950.2 Leino, K. R. M., and Clément Pit-Claudel. “Trigger Selection Strategies to Stabilize Program Verifiers.” Lecture Notes in Computer Science Vol. 9779, (2016): 361–381. https://orcid.org/0000-0002-1900-3901 en_US http://dx.doi.org/10.1007/978-3-319-41528-4_20 Computer Aided Verification Article is made available in accordance with the publisher's policy and may be subject to US copyright law. Please refer to the publisher's site for terms of use. application/octet-stream Springer International Publishing Pit-Claudel |
| spellingShingle | Leino, K. Rustan M. Pit-Claudel, Clément Trigger Selection Strategies to Stabilize Program Verifiers |
| title | Trigger Selection Strategies to Stabilize Program Verifiers |
| title_full | Trigger Selection Strategies to Stabilize Program Verifiers |
| title_fullStr | Trigger Selection Strategies to Stabilize Program Verifiers |
| title_full_unstemmed | Trigger Selection Strategies to Stabilize Program Verifiers |
| title_short | Trigger Selection Strategies to Stabilize Program Verifiers |
| title_sort | trigger selection strategies to stabilize program verifiers |
| url | https://hdl.handle.net/1721.1/103950.2 https://orcid.org/0000-0002-1900-3901 |
| work_keys_str_mv | AT leinokrustanm triggerselectionstrategiestostabilizeprogramverifiers AT pitclaudelclement triggerselectionstrategiestostabilizeprogramverifiers |