Formal Methods and Program Analysis in Industry
(draft)
See also: Compilers: correctness, Software Verification Literature Review (https://alastairreid.github.io/RelatedWork/papers/)
- What Works (and Doesn't) Selling Formal Methods
- Lessons from Formally Verified Deployed Software Systems
- 2023
- Li Huang, Sophie Ebersold, Alexander Kogtenkov, Alexandr Naumchev, Bertrand Meyer, Yinling Liu, ALiyu Alege
- https://arxiv.org/abs/2301.02206
- A Decade Verifying LLVM, or How to Retrofit Soundness in Industrial Software
- Workshop on Dependable and Secure Software Systems 2022
- Nuno P. Lopes
- https://www.youtube.com/watch?v=36NLxbSSfwQ
- https://files.sri.inf.ethz.ch/website/events/workshop2022/Nuno-Lopes.pdf
- Formally Verifying Industry Cryptography
- IEEE IEEE Security & Privacy May-June 2022
- Mike Dodds
- https://doi.ieeecomputersociety.org/10.1109/MSEC.2022.3153035
- Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3
- SOSP 2021
- James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran, Jacob Van Geffen, Andrew Warfield
- https://www.amazon.science/publications/using-lightweight-formal-methods-to-validate-a-key-value-storage-node-in-amazon-s3
- https://dl.acm.org/doi/10.1145/3477132.3483540
- Code-Level Model Checking in the Software Development Workflow
- ICSE 2020 Software Engineering in Practice
- Nathan Chong, Byron Cook, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle
- https://www.amazon.science/blog/how-to-integrate-formal-proofs-into-software-development
- https://www.amazon.science/publications/model-checking-as-a-human-endeavor
- https://angelhof.github.io/files/papers/model-checking-2020-icse-seip.pdf
- Towards making formal methods normal: meeting developers where they are
- HATRA 2020: Human Aspects of Types and Reasoning Assistants
- Alastair Reid, Luke Church, Shaked Flur, Sarah de Haas, Maritza Johnson, Ben Laurie
- https://arxiv.org/abs/2010.16345
- Boost the Impact of Continuous Formal Verification in Industry
- TAPAS 2019: Workshop on Tools for Automatic Program Analysis
- Felipe R. Monteiro, Mikhail R. Gadelha, Lucas C. Cordeiro
- https://arxiv.org/abs/1904.06152
- https://staticanalysis.org/tapas2019/talks/TAPAS_2019_paper_7.pdf
- Model Checking a C++ Software Framework, a Case Study
- European Software Engineering Conference / Foundations of Software Engineering (ESEC/FSE) 2019
- John Lång, I.S.W.B. Prasetya
- https://arxiv.org/abs/1907.00172
- One-Click Formal Methods
- IEEE Software 36(6) 2019
- John Backes, Pauline Bolignano, Byron Cook, Andrew Gacek, Kasper Søe Luckow, Neha Rungta, Martin Schäf, Cole Schlesinger, Rima Tanash, Carsten Varming, Michael W. Whalen
- https://doi.org/10.1109/MS.2019.2930609
- http://www0.cs.ucl.ac.uk/staff/b.cook/oneclick.pdf
- Scaling Static Analyses at Facebook
- Dino Distefano, Manuel Fähndrich, Francesco Logozzo, Peter W. O'Hearn
- Communications of the ACM, Vol. 62 No. 8, 2019
- https://cacm.acm.org/magazines/2019/8/238344-scaling-static-analyses-at-facebook/fulltext
- The Evolution of Automated Reasoning Technology at AWS
- AWS re:Inforce 2019
- https://www.youtube.com/watch?v=x6wsTFnU3eY
- Continuous Formal Verification of Amazon s2n
- CAV 2018
- Andrey Chudnov, Nathan Collins, Byron Cook, Joey Dodds, Brian Huffman, Colm MacCárthaigh, Stephen Magill, Eric Mertens, Eric Mullen, Serdar Tasiran, Aaron Tomb, Eddy Westbrook
- https://doi.org/10.1007/978-3-319-96142-2_26
- Continuous Reasoning: Scaling the Impact of Formal Methods
- Logic in Computer Science (LISC) 2018; Peter O'Hearn
- https://research.fb.com/publications/continuous-reasoning-scaling-the-impact-of-formal-methods/
- End-to-End Verification of ARM Processors with ISA-Formal
- International Conference on Computer Aided Verification (CAV) 2016
- Alastair Reid, Rick Chen, Anastasios Deligiannis, David Gilday, David Hoyes,Will Keen, Ashan Pathirane, Owen Shepherd, Peter Vrabel, and Ali Zaidi
- https://alastairreid.github.io/papers/CAV_16/
- https://alastairreid.github.io/finding-bugs/
- Experience developing and deploying concurrency analysis at Facebook
- Formal Reasoning About the Security of Amazon Web Services
- CAV 2018
- Byron Cook
- https://doi.org/10.1007/978-3-319-96145-3_3
- From Start-ups to Scale-ups: Opportunities and Open Problems for Static and Dynamic Program Analysis
- IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM) 2018
- Mark Harman, Peter O'Hearn
- https://research.fb.com/publications/from-start-ups-to-scale-ups-opportunities-and-open-problems-for-static-and-dynamic-program-analysis/
- Lessons from Building Static Analysis Tools at Google
- Communications of the ACM, Vol. 61 No. 4, 2018
- Caitlin Sadowski, Edward Aftandilian, Alex Eagle, Liam Miller-Cushon, Ciera Jaspan
- https://cacm.acm.org/magazines/2018/4/226371-lessons-from-building-static-analysis-tools-at-google/abstract
- https://research.google.com/pubs/pub46576.html
- https://cacm.acm.org/magazines/2018/4/226371-lessons-from-building-static-analysis-tools-at-google/fulltext
- Model Checking Boot Code from AWS Data Centers
- CAV 2018
- Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, Mark R. Tuttle
- https://doi.org/10.1007/978-3-319-96142-2_28
- Moving Fast with Software Verification
- NASA Formal Method Symposium 2015
- Cristiano Calcagno, Dino Distefano, Jérémy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter W. O'Hearn, Irene Papakonstantinou, Jim Purbrick, Dulma Rodriguez:
- https://research.fb.com/publications/moving-fast-with-software-verification/
- https://blog.acolyer.org/2015/11/20/moving-fast-with-software-verification/
- Use of Formal Methods at Amazon Web Services
- CACM 2015 (How Amazon web services uses formal methods)
- https://dl.acm.org/citation.cfm?id=2699417
- https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf
- A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World
- Communications of the ACM, Vol. 53 No. 2, 2010
- Al Bessey, Ken Block, Ben Chelf, Andy Chou, Bryan Fulton, Seth Hallem, Charles Henri-Gros, Asya Kamsky, Scott McPeak, Dawson Engler
- https://cacm.acm.org/magazines/2010/2/69354-a-few-billion-lines-of-code-later/fulltext
- Replacing Testing with Formal Verification in Intel Core i7 Processor Execution Engine Validation
- CAV 2009
- Roope Kaivola, Rajnish Ghughal, Naren Narasimhan, Amber Telfer, Jesse Whittemore, Sudhindra Pandav, Anna Slobodová, Christopher Taylor, Vladimir Frolov, Erik Reeber, Armaghan Naik
- https://dl.acm.org/citation.cfm?id=1575095
- PDF: https://is.muni.cz/el/1433/jaro2010/IA159/um/intel.pdf
- Slides: https://cps-vo.org/node/1371
- Case study: Integrating FV and DV within the Verification of Intel(r) Core(TM)2 Microprocessor
- FMCAD 2007
- Alon Flaisher, Alon Gluska, Eli Singerman
- https://ieeexplore.ieee.org/document/4402000
- Formal Reasoning and the Hacker Way (Keynote)
- ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis (SOAP) 2020
- Peter W. O’Hearn
- https://www.youtube.com/watch?v=wlbfjAnQw6U
- https://pldi20.sigplan.org/details/SOAP-2020-papers/4/Keynote-Formal-Reasoning-and-the-Hacker-Way
- Using Formal Methods to Eliminate Exploitable Bugs
- Chalmers Functional Programming Seminar Series 2020
- Kathleen Fisher
- https://www.youtube.com/watch?v=YyT9BU0aJUE