Si, Xujie, Zhang, Xin, Grigore, Radu, Naik, Mayur (2017) Maximum Satisfiability in Software Analysis: Applications and Techniques. In: Lecture Notes in Computer Science. Computer Aided Verification: 29th International Conference, CAV 2017 Heidelberg, Germany, July 24–28, 2017 Proceedings, Part I. 10426. pp. 68-94. Springer ISBN 978-3-319-63386-2. (doi:10.1007/978-3-319-63387-9_4) (KAR id:63671)
PDF
Author's Accepted Manuscript
Language: English |
|
Download this file (PDF/576kB) |
|
Request a format suitable for use with assistive technology e.g. a screenreader | |
Official URL: https://doi.org/10.1007/978-3-319-63387-9_4 |
Abstract
A central challenge in software analysis concerns balancing different competing tradeoffs. To address this challenge, we propose an approach based on the Maximum Satisfiability (MaxSAT) problem, an optimization extension of the Boolean Satisfiability (SAT) problem. We demonstrate the approach on three diverse applications that advance the state-of-the-art in balancing tradeoffs in software analysis. Enabling these applications on real-world programs necessitates solving large MaxSAT instances comprising over 10301030 clauses in a sound and optimal manner. We propose a general framework that scales to such instances by iteratively expanding a subset of clauses while providing soundness and optimality guarantees. We also present new techniques to instantiate and optimize the framework.
Item Type: | Conference or workshop item (Proceeding) |
---|---|
DOI/Identification number: | 10.1007/978-3-319-63387-9_4 |
Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
Depositing User: | Radu Grigore |
Date Deposited: | 29 Sep 2017 08:31 UTC |
Last Modified: | 05 Nov 2024 10:59 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/63671 (The current URI for this page, for reference purposes) |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):