Engineering with Logic: Rigorous Test-Oracle Specification and Validation for TCP/IP and the Sockets API
- Submitting institution
-
The University of Leicester
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 1430
- Type
- D - Journal article
- DOI
-
10.1145/3243650
- Title of journal
- Journal of the ACM
- Article number
- 1
- First page
- 1
- Volume
- 66
- Issue
- 1
- ISSN
- 0004-5411
- Open access status
- Exception within 3 months of publication
- Month of publication
- December
- Year of publication
- 2018
- URL
-
-
- Supplementary information
-
https://doi.org/10.1145/3243650
- 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
-
0
- Research group(s)
-
-
- Citation count
- 2
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This JACM article details the formal specification of TCP/IP in higher-order logic, and its validation against real-world implementations. These original techniques have been used by other major specification/verification efforts: weak memory models (REMS project), filesystems (SibylFS), processor models (CHERI), C and C++ standards (REMS again). There are more than 50 papers in top venues such as POPL using techniques described in the paper. Our experience of "specification at scale" led us to develop tools, such as "Ott" (ICFP "most influential paper" prize winner) and its successor "Lem", which have themselves had significant impact on the field of formal specification.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -