Efficient verification of concurrent systems using synchronisation analysis and SAT/SMT solving
- Submitting institution
-
University of Oxford
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 2072
- Type
- D - Journal article
- DOI
-
10.1145/3335149
- Title of journal
- ACM Transactions on Software Engineering and Methodology
- Article number
- 18
- First page
- -
- Volume
- 28
- Issue
- 3
- ISSN
- 1049-331X
- Open access status
- Compliant
- Month of publication
- August
- Year of publication
- 2019
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
2
- Research group(s)
-
-
- Citation count
- 0
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper, bringing together work published at a number of conferences (IFM�16, FM�16, TACAS�17, and SBMF�17), helped to introduce a new style of verification, in which the PSPACE and seemingly intractable reachability problem for concurrent systems is replaced by NP approximations based on local analysis. The latter are far more tractable in typical cases thanks to SAT and SMT checkers. The approximations are conservative in that they over-approximate the state space. The paper was partly inspired by the need to have scalable verification of properties required by our industrial collaboration with ASML as part of Roscoe�s EPSRC standard grant EP/N022777/1.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -