Programming Language Theory & Formal Methods - Resources

Image Courtsey : Forsyte group

Formal methods are mathematical techniques that are used for design, verification and specifications of software and hardware problems. These are essentially a subset of Programming Language Theory research that are being used to study complex computer science problems.

Analysis by Formal Methods basically involves these steps :

1. Formal Specification
2. Formal Proofs
3. Model Checking
4. Abstraction

The formal proof development and model checking are primarily done using interactive theorem provers often called as proof Assistants. Abstraction is creating structurally sound relations between parts of models.

Here is my attempt to curate a list of useful reading materials, videos and tools accompanied by some upcoming challenges in the field.

NOTE :

1. I have tried to make the content more focused on current research and industrial application. People looking for purely academic collection must refer Formal Methods in Education - Jeremy Avigad.

2. The reader is expected to have some basic knowledge of Type Theory. A more academic insight can be found here learn-tt.

Contents

• Books & Lectures
• Blogs
• MOOCs
• Tools
• Projects
• Upcoming Challenges
  • Security Related
    • Software Security
    • Differential Privacy
    • Applications in Block Chain Security
    • Challenges in Making AI secure
    • Create Secure CyberPhysical Systems
  • Abstract Interpretation focused
  • Programming Language research related
    • Probabilistic Programming
    • Development of Quantum Programming Language
    • Language Refinement using formal methods
• Related Industries & Startups

Books & Lectures

• Software Foundations : I highly advice this as a starting material for diving deep into this field. The book is very helpful in building basic concepts and serves as a very sound introduction to the field. Beautifully illustrated concepts with examples to practice are provided all throughout making interactive theorem proving learning fun.

• FRAP - Adam Chlipala : A book that helps you understand and reason formal correctness of programs. Imperative language (C) inspired examples of data structures and algorithms helps immensely to begin thinking about their formal verification.

• Certified Programming with Dependent Types - Adam Chlipala : One of the best theoretical books to learn theorem proving using coq.

• Formal Verification - Jacques Fleuriot : This a course that involves theorem proving using some more developed tools like SAT and SMT solvers.

• Abstract Interpretation - Patrick Cousot The best available material on the theory of Abstract Interpretation. It gives a complete and pure mathematical analysis of program mutations. The Program behaviour as a continuously modifying relation between different abstract mathematical structures is explained and proved!!.

• Logic and Proof - CMU & Lean introduction : This is course designed at CMU and it also serves as a introductory material for theorem proving in Lean

If you feel you need more theoretical insights, please refer Note above.

Blogs

• Getting Started with formal methods
• K Framework & efforts of Formal verification in Blockchain
• Pact Formal Verification for Blockchain smart contracts : Awesome short blog explaining the Pact FV's methodology with a small introduction to formal verification by first principles.
• Towards Robust and Verified AI: Specification Testing, Robust Training, and Formal Verification - DeepMind
• The challenge of verification and testing of machine learning - Ian GoodFellow & Nicolas Papernot

MOOCs

• Formal Software Verification - edX
• Quantitative Model Checking - Coursera
• Cyber Physical Systems : Course by UC Berkeley, focused in using verification methods for modelling Cyper Physical systems (CPS).
• Programming Languages - Coursera

Tools

Proof Assistants

• coq: The most popular and widely used theorem prover. It supports a lot of features including ML-extraction, Project packaging (Project and Makefile creation). There are plenty of how-to material available that use coq for formalization. Anyone might find this very interesting 100 Theorems in Coq.

• lean: A fairly new Theorem Prover by Microsoft Research. Has a nice interactive tutorial, is easy to get started with.

• PRISM model checker : It is model checker developed by University of Oxford.

• Nuprl : Theorem Prover by Cornell under Proof Refinement Logic Project.

• Agda: A quite Mature Proof Assistant. Has features similar to Coq. easy to learn after some experience in coq.

• Isabelle: It is an old theorem Prover. Has nice implementation of core logic but lacks other UX related features.

• VCC : A mechanical verifier for concurrent C programs by Microsoft.

• TLA+ : High Level language for modelling languages and systems ( especially concurrent & distributed).

SAT/SMT/SMC solvers

SAT Solvers :

• MiniSat.

SMT Solvers :

• Z3

• CVC4

• MathSAT5

• SMTInterpol

• Princess

SMC Solvers :

• Publication

Hybrid Solvers

Proof Assitants have very strong implmentations of program logics. Sometimes it may not be tactically possible to carry out complex proofs only by using them. Therefore Current research combines this principle of strong logic based reasoning with powerful SMT and SMC solvers to ease the proof development. Some examples are here below :

• Fstar(F*)

  • It is possible to extract F* code to C using KreMLin.

• SMTCoq

Projects

Most of the projects are more or less development of the respective theorem provers or SAT/SMT/SMC/ solvers and hence can be looked up there. These are some of other projects actively developed.

• DeepSpec is an umbrella project that focuses on building verified software systems. Follwoing major sub-projects are actively worked upon :

  • Compcert
  • Verified LLVM (VeLLVM)
  • Verified Software ToolChain (VST)

• ikos is a reliable bug-free C compiler based on the theory of abstract interpretation.

• Project Everest: It is research project that aims at creating secure and verified HTTPS ecosystem.

• CertiCrypt: It is a project focuse on modelling public key cryptography using coq proof assistant.

• Iris: Iris is a Higher-Order Concurrent Separation Logic Framework implemented and verified in the proof assistant Coq.

• VeriDeep - Safety Verification of Deep Neural Networks

• VeHICal : Project focused on developing the foundations of verified co-design of interfaces and control for human cyber-physical systems.

• FastSMT - Tool to augment your SMT solver by learning to optimize its performance for your dataset of formulas. It is developed by SRI lab, ETH Zurich built on top of Z3 SMT solver.

• fm4cps - Formal methods for Cyber Physical Systems, joint efforts by INRIA and ECNU shanghai.

Upcoming Challenges

Security Related

• Software Security

  • Readings
    • Formal Methods for Security, NSF workshop
    • Symbolic Relationship between Formal Methods and Security
    • Project-Everest Research Papers
    • Formal Methods in Software Security
    • Formal Methods for Safe and Secure Computers Systems
    • The Computational Soundness of Formal Encryption
    • Security Structures using Formal Methods
    • Verification of Cryptographic Primitive
    • Formal Certification of Game based Cryptographic proofs
    • Formal certification of code-based cryptographic proofs
  • Videos
    • Deep Specification for Dropbox
    • DSL for Verified Secure Multiparty Computations in F*
    • Using Formal Methods for development of Highly Secure Systems
    • Security through FOrmal Methods and Secure Architecture (CERIAS - Purdue University)
    • Language based techniques for Cryptography and Privacy

• Differential Privacy

  • Readings
    • Formal Verification of Differential Privacy for Interactive Systems
    • Formal Methods for Privacy
    • LightDP - Towards automating Differential Privacy Proofs
    • EasyCrypt - Verified Computational Differential Privacy with Applications to Smart Meter
    • Proving Differential Privacy in Hoare Logic
    • Differentially Private Bayesian Programming
    • Advanced Probabilistic Coupling for Differential Privacy
  • Videos
    • Formal Methods and proofs of privacy properties - 1
    • Formal Methods and proofs of privacy properties - 2
    • Formal Methods and proofs of privacy properties - 3
    • Proving Differential privacy using Relational Types

• Applications in Block Chain Security

  Formal Methods for Block Chains : This is first ever workshop focused on using formal methods in Block Chain technology. It will be on 11th October 2019.

  CertiK : It is a startup focused on using formal methods to make blockchains verifialbly secure.

  • Readings
    • How Formal Analysis and Verification Add Security to Blockchain-based Systems - Tutorial @ MIT
    • Smart contracts and oppurtunities for formal methods
    • K Framework & efforts of Formal verification in Blockchain an Awesome collection of explainatory material on K framework and its application in verifying Blockchain systems.
    • Pact Formal Verification for Blockchain smart contracts : Awesome short blog explaining the Pact FV's methodology with a small introduction to formal verification by first principles.
    • Temoporal Blockchains - a formal analysis
    • Validation of Decentralised Smart Contracts through Game Theory and Formal Methods
  • Videos
    • Formal Design, Implementation and Verification of BlockChain Languages
    • CertiK - Smart contract formal verification platform (review)
    • Simplicity - A new Language for blockchains

• Challenges in making AI secure

  FLoC 2018- Summit of Machine Learning meets formal methods

  Verified Machine Learning - Radboud University Nijmegen : University course on using verification methods in Machine Learning.

  Formal Methods meets Machine Learning - RWTH Aachen University : 2018's seminar on advancements in Verifiably Secure Machine Learning using formal methods.

  • Readings

    • Towards Verified Artificial Intelligence - S. Seshia
    • Towards Robust and Verified AI: Specification Testing, Robust Training, and Formal Verification - DeepMind
    • Developing BugFree Machine Learning Systems with Formal Mathematics
    • Mixing Formal methods, Machine Learning & Human Computer Interaction
    • Machine Learning in Formal Methods
    • Machine Learning and Formal Methods
    • Algorithms for Verifying Deep Neural Networks
    • Safety Verification of Deep Neural Networks
    • The challenge of verification and testing of machine learning - Ian GoodFellow & Nicolas Papernot
    • Verifying Properties of Binarized Deep Neural Networks
    • Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks
    • Verification of Piecewise Linear Feed Forward Networks
    • Challenges in Verification of Reinforcement Learning Algorithms
    • Applying Formal Methods in Reinforcement Learning - Galois Inc.
    • Towards Proving the Adversarial Robustness of Deep Neural Networks

  • Videos

    • Safety Verification for Deep Neural Networks -ICST 2018
    • Safety Verification for Deep Neural Networks - Marta Kwiatkowska - CAV 2017
    • Safety Verification for Deep Neural Networks -INRIA
    • Rules of Machine Learning Verification, from data driven bugs to explainable AI
    • Verification of Machine Learning Programs
    • Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks - Conference Video
    • Developing Bug-Free Machine Learning models using Certigrad - Daniel Selsam

• Create secure CyberPhysical Systems

  VeHICal : Project focused on developing the foundations of verified co-design of interfaces and control for human cyber-physical systems.

  fm4cps - Formal methods for Cyber Physical Systems, joint efforts by INRIA and ECNU shanghai.

  • Readings
    • Cyber-Physical Systems Design: Formal Foundations, Methods and Integrated Tool Chains
    • New Frontiers in Formal Methods: Learning, Cyber-Physical Systems, Education, and Beyond
    • Statistical Model Checking for Cyber-Physical Systems
    • Formal Verification of Transportation Cyber Physical Systems
    • Verification of Cyber-Physical Systems
    • Verification and Validation in Cyber Physical Systems: Research Challenges and a Way Forward
    • Anomaly Detection in Cyber-Physical Systems: A Formal Methods Approach
    • Compositional Verification of Self-Adaptive Cyber-Physical Systems
  • Videos
    • A Formal Methods Charter for Cyber-Physical Systems and Industrial Internet of Things
    • Formal Verification of Cyber Physical Systems
    • Monitoring Cyber Physical Systems

Abstract Interpretation focused

• Fast and Effective Robustness Certification : project DeepZ - for certifying neural network robustness based on abstract interpretation.
• AI2 : Safety and Robustness Certification of Neural Networks with Abstract Interpretation
• Boosting Robustness Certification of Neural Networks : Uses Abstract Interpretation in its methodology.

Programming Language Research related

• Probabilistic Programming

  • Readings
    • An introduction to Probabilistic Programming
    • Formal Verification of Higher Order Probabilistic programs
    • Probabilistic Logic Programming and Bayesian Networks
    • probabilistic Functions and Cryptographic Oracles in Higher Order Logic - Andreas Lochbihler
    • Probabilistic Relational Verification of Cryptographic implementations
    • Coupling Proofs are Probabilistic product programs
    • Advanced Probabilistic Coupling for Differential Privacy
    • Formal Methods for probabilistic Programming
    • Formal methods for probabilistic programs : Lecture slides
    • Probabilistic Programming - True Verification Challenge
    • FairSquare : Probabilistic Verification of Program Fairness
    • VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs
    • Unifying Logic and Probability
  • Videos
    • Formal Verification of Higher Order Probabilistic Programs - POPL 2019 conference video
    • Probabilistic logic programming and its applications - Luc De Raedt, Leuven

• Development of Quantum Programming Language

  • Readings
    • Qwire : Formal Verification of Quantum Programs in Coq
    • A Logic for Formal Verification of Quantum Programs
    • Coupling Techniques for Reasoning about Quantum Programs
    • Formal Verification vs Quantum Uncertainity
    • Model Checking Recursive Quantum Protocols
  • Videos
    • Mission-capable Quantum Computing for Software Verification and Validation (VV) - CMU
    • Dominique Unruh: Formal Verification of Quantum Cryptography

• Languages Refinement using formal methods

This particularily deals with improving certain properties (like Parallelism & Concurrency) of existing programming languages. A lot can be easily looked up in regard to this since after all this is the sole most important reason to study PL theory. All the conferences listed up in here ACM SIGPLAN have majority of research papers on programming language development do check them out.

Related Industries & Startups

• CertiK
• Galois Inc
• Synthetic Minds
• Nomadic Labs
• Tezos
• JaneStreet
• Systerel
• Tweag
• Veriflow

License

Any suggestions are welcome. Please do consider submitting a pull request if you feel like !!