From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification
Many verifications of realistic software systems are monolithic, in the sense that they define single global invariants over complete system state. More modular proof techniques promise to support reuse of component proofs and even reduce the effort required to verify one concrete system, just as mo...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | en_US |
| Published: |
Association for Computing Machinery (ACM)
2015
|
| Online Access: | http://hdl.handle.net/1721.1/99930 https://orcid.org/0000-0001-7085-9417 |
| _version_ | 1826215316957429760 |
|---|---|
| author | Chlipala, Adam |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Chlipala, Adam |
| author_sort | Chlipala, Adam |
| collection | MIT |
| description | Many verifications of realistic software systems are monolithic, in the sense that they define single global invariants over complete system state. More modular proof techniques promise to support reuse of component proofs and even reduce the effort required to verify one concrete system, just as modularity simplifies standard software development. This paper reports on one case study applying modular proof techniques in the Coq proof assistant. To our knowledge, it is the first modular verification certifying a system that combines infrastructure with an application of interest to end users. We assume a nonblocking API for managing TCP networking streams, and on top of that we work our way up to certifying multithreaded, database-backed Web applications. Key verified components include a cooperative threading library and an implementation of a domain-specific language for XML processing. We have deployed our case-study system on mobile robots, where it interfaces with off-the-shelf components for sensing, actuation, and control. |
| first_indexed | 2024-09-23T16:23:31Z |
| format | Article |
| id | mit-1721.1/99930 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T16:23:31Z |
| publishDate | 2015 |
| publisher | Association for Computing Machinery (ACM) |
| record_format | dspace |
| spelling | mit-1721.1/999302022-10-02T07:52:35Z From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification Chlipala, Adam Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Chlipala, Adam Many verifications of realistic software systems are monolithic, in the sense that they define single global invariants over complete system state. More modular proof techniques promise to support reuse of component proofs and even reduce the effort required to verify one concrete system, just as modularity simplifies standard software development. This paper reports on one case study applying modular proof techniques in the Coq proof assistant. To our knowledge, it is the first modular verification certifying a system that combines infrastructure with an application of interest to end users. We assume a nonblocking API for managing TCP networking streams, and on top of that we work our way up to certifying multithreaded, database-backed Web applications. Key verified components include a cooperative threading library and an implementation of a domain-specific language for XML processing. We have deployed our case-study system on mobile robots, where it interfaces with off-the-shelf components for sensing, actuation, and control. National Science Foundation (U.S.) (Grant CCF-1253229) United States. Defense Advanced Research Projects Agency (Agreement FA8750-12-2-0293) 2015-11-13T17:00:52Z 2015-11-13T17:00:52Z 2015-01 Article http://purl.org/eprint/type/ConferencePaper 9781450333009 http://hdl.handle.net/1721.1/99930 Adam Chlipala. 2015. From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '15). ACM, New York, NY, USA, 609-622. https://orcid.org/0000-0001-7085-9417 en_US http://dx.doi.org/10.1145/2676726.2677003 Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '15) Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf Association for Computing Machinery (ACM) MIT web domain |
| spellingShingle | Chlipala, Adam From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification |
| title | From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification |
| title_full | From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification |
| title_fullStr | From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification |
| title_full_unstemmed | From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification |
| title_short | From Network Interface to Multithreaded Web Applications: A Case Study in Modular Program Verification |
| title_sort | from network interface to multithreaded web applications a case study in modular program verification |
| url | http://hdl.handle.net/1721.1/99930 https://orcid.org/0000-0001-7085-9417 |
| work_keys_str_mv | AT chlipalaadam fromnetworkinterfacetomultithreadedwebapplicationsacasestudyinmodularprogramverification |