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 :
Formal Specification
Formal Proofs
Model Checking
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 :

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.

The reader is expected to have some basic knowledge of Type Theory. A more academic insight can be found here learntt.
Contents
 Books & Lectures
 Blogs
 MOOCs
 Tools
 Projects
 Upcoming Challenges
 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 MLextraction, Project packaging (Project and Makefile creation). There are plenty of
howto
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 :
SMT Solvers :
SMC Solvers :
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 :
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 subprojects are actively worked upon :

ikos is a reliable bugfree 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 HigherOrder Concurrent Separation Logic Framework implemented and verified in the proof assistant Coq.

VeHICal : Project focused on developing the foundations of verified codesign of interfaces and control for human cyberphysical 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
 ProjectEverest 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 codebased cryptographic proofs
 Videos
 Readings

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
 Readings

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 Blockchainbased 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
 Readings

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 BugFree Machine Learning models using Certigrad  Daniel Selsam
 Readings

Create secure CyberPhysical Systems
VeHICal : Project focused on developing the foundations of verified codesign of interfaces and control for human cyberphysical systems.
fm4cps  Formal methods for Cyber Physical Systems, joint efforts by INRIA and ECNU shanghai.
 Readings
 CyberPhysical Systems Design: Formal Foundations, Methods and Integrated Tool Chains
 New Frontiers in Formal Methods: Learning, CyberPhysical Systems, Education, and Beyond
 Statistical Model Checking for CyberPhysical Systems
 Formal Verification of Transportation Cyber Physical Systems
 Verification of CyberPhysical Systems
 Verification and Validation in Cyber Physical Systems: Research Challenges and a Way Forward
 Anomaly Detection in CyberPhysical Systems: A Formal Methods Approach
 Compositional Verification of SelfAdaptive CyberPhysical Systems
 Videos
 Readings
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 PartialCorrectness Logic for Probabilistic Programs
 Unifying Logic and Probability
 Videos
 Readings

Development of Quantum Programming Language
 Readings
 Videos

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
License
Any suggestions are welcome. Please do consider submitting a pull request if you feel like !!