Code Level Model-Checking in the Software Development Workflow
- Submitting institution
-
Queen Mary University of London
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 543
- Type
- E - Conference contribution
- DOI
-
10.1145/3377813.3381347
- Title of conference / published proceedings
- Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Software Engineering in Practice
- First page
- 11
- Volume
- -
- Issue
- -
- ISSN
- -
- Open access status
- -
- Month of publication
- June
- Year of publication
- 2020
- 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
-
8
- Research group(s)
-
-
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Detailed data documenting continuous use of the C Bounded Model Checker (CBMC, Tautschnig is co-lead of project) to verify components of Amazon's public software libraries and FreeRTOS, an open-source real-time operating system. More than 5,000 verification runs are completed each day. The paper further details the challenges and successes in working with software developers to integrate automated verification into their workflow. Contact at AWS: Reto Kramer, retok@amazon.com.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -