Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems
- Submitting institution
-
The University of Leicester
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 1408
- Type
- D - Journal article
- DOI
-
10.1145/3060257
- Title of journal
- Journal of the ACM
- Article number
- 15
- First page
- 1
- Volume
- 64
- Issue
- 2
- ISSN
- 0004-5411
- Open access status
- Compliant
- Month of publication
- May
- Year of publication
- 2017
- URL
-
-
- Supplementary information
-
https://doi.org/10.1145/3060257
- 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
- 3
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Selected as a best paper in conference on Computer Aided Verification 2015 and invited to a special issue in JACM of papers from that conference. The technique we introduced (prophecy variables for partial determinization) was used by others (e.g., Padon et al. FMCAD’18). The benchmarks we have included have been used by others to validate alternative approaches (e.g., PhD thesis of Bauch (Masaryk University), Daniel et al. CAV 2016).
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -