Formal Method is a set of techniques and methodology that helps us in doing formal verification. Formal Verification is a way of defining a concrete / abstract overview of a problem or model and then answering some questions regarding the properties of that model. We try to prove certain assertions and check for validity. Eg. Given a program does it ever happen that some variables take negative values. Does a model access a particular array element while execution. Some of the claims and problems that verifications tries to solve are undecideable but these things are done in finite amount of time and resources for most of the practical programming/development problems that we try solving via abstractions and approximations. You can however provide specific inputs that make the problem hard to solve/non halting.

• Install and use inkspace to make beautiful drawings for your paper

• ACM Winter School : Computer Architecture, Compilers, PL, Logic, Testing & Verification.

Some cool paper links.

• KLEE Paper
• Deferred concretization in symbolic execution via fuzzing
• UCLID Paper
• Bucketing Failing Tests via Symbolic Analysis
• Hot Path SSA
• K-paths Profiling
• Exploring program phases for statistical bug localization
• Symbolic Execution and Dynamic Taint Analysis
• Non-Interference
• A Formal Approach to Secure Speculation
• A Formal Verification Framework for Security Issues of Blockchain Smart Contracts
• Formal Verification of Smart Contracts: Short Paper
• ZEUS: Analyzing Safety of Smart Contracts
• Using Dafny, an Automatic Program Verifier
• DART Paper
• From Program to Logic: An Introduction
• SAGE : Whitebox Fuzzing for Security Testing
• SoC Verification Problem

• ConCert: A Smart Contract Certification Framework in Coq
• Scilla-Paper
• CUTE Symbolic Execution
• Control Flow Integrity
• Avoiding Exponential Explosion

• Dafny
• Hyperproperties
• Computer Security
• Dafny Examples
• The Art, Science, and Engineering of Fuzzing
• Boolean Satisfiability Solversand Their Applications inModel Checking
• Software Foundations - Logical Foundations
• Model Checking
• FORMAL METHODS IIT-D Lecture Slides
• Program Analysis, Verification & Testing Book
• The Science Of Programming
• Model Checking
• Building Secure Systems from Buggy Code with Information Flow Control
• Modular Verification of Secure Information Flow - Peter Müller
• CISSP Domain Security
• Delta Debugging
• What is fuzzing?
• AFL++

1. Induction is a way to prove things that are defined recursively.

• Base case, we show that either for 1 or 0 / starting cases some property is true.
• For some k th case we show that if we assume P(k) is true, P(k+1) is true
• From this we may conclude that P(n) holds for all n in our domain.

Introduction Videos :

Fantastic videos by Dr. Subhajit Roy (IIT Kanpur)

• ACM School PAVT

• https://www.youtube.com/watch?v=m_91KWQiC0o&list=PLA72M-qSGPm3Bnkc6iKGxrL1OARztbm6V

• https://www.youtube.com/watch?v=Fy8cNMuk_rY&list=PLA72M-qSGPm3HZbcRLVOSpxELUHtdaNpt

• https://www.youtube.com/watch?v=v2i59XRceXE&list=PLA72M-qSGPm2ohvwvJVbd3abnaSkiBy8j

2. Bounded Model Checking : We model the problem like a Finite State Machine. An execution of a FSM is a string formed by simulating the state-to-state transitions. We ask if a certain property holds for the FSM globally or eventually when we move from say State S1 to S2. The model is bounded in the sense that we consider a finite number of states but an have infinite number of executions or traces possible.

• https://www.youtube.com/watch?v=QOcxbzopSk4&list=PLA72M-qSGPm27TjJaMOsNcMnLUoYAO9ZT

• https://www.youtube.com/watch?v=piISG8bV2GI&list=PLJ5C_6qdAvBGojQMUzL4x5Y0N5gBJmT4l

• https://www.youtube.com/watch?v=8wI5ee3Lwsw&list=PLJ5C_6qdAvBGojQMUzL4x5Y0N5gBJmT4l&index=13

LTL, this logic theory is needed to model temporal properties or state transitions where the property depends on time / or on the next state of execution. As in the case of an FSM, we need to check if property holds from state to state.

• https://www.youtube.com/watch?v=W5Q0DL9plns&list=PLJ5C_6qdAvBGojQMUzL4x5Y0N5gBJmT4l&index=33

For properties that need a set of set of traces to define and prove correctness, we need hyper-properties.

• https://www.youtube.com/watch?v=JZ5OWdX3hmY

• https://www.youtube.com/watch?v=kjxdelbo9C4&list=PLA72M-qSGPm2bZlhxYB-ePerW0U8nPn4H
• http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/IncorrectnessLogic.pdf

• https://www.youtube.com/watch?v=-_tx3lk7yn4

• https://arxiv.org/pdf/1701.04481.pdf.

• https://link.springer.com/book/10.1007/978-3-540-74113-8

• https://www.cs.cornell.edu/fbs/publications/Hyperproperties.pdf.

• https://www.youtube.com/watch?v=6q15ytIOE3U

What is Computer Security ?

• https://www.microsoft.com/en-us/research/publication/practical-principles-for-computer-security/
• https://dl.acm.org/doi/pdf/10.1145/1592761.1592773

• https://www.youtube.com/watch?v=v2i59XRceXE&list=PLA72M-qSGPm2ohvwvJVbd3abnaSkiBy8j

• https://www.youtube.com/watch?v=gggItiZ3Sjk&list=PLA72M-qSGPm1pISu85QR6bZL4wK4rZZxp

• https://www.youtube.com/watch?v=t-Mj4ji3tCw&list=PLA72M-qSGPm2WxSxXthNiYx2u4KBZlXCC

• https://www.youtube.com/watch?v=kjxdelbo9C4&list=PLA72M-qSGPm2bZlhxYB-ePerW0U8nPn4H

• https://www.youtube.com/watch?v=m_91KWQiC0o&list=PLA72M-qSGPm3Bnkc6iKGxrL1OARztbm6V

• https://www.youtube.com/watch?v=Fy8cNMuk_rY&list=PLA72M-qSGPm3HZbcRLVOSpxELUHtdaNpt

• https://www.youtube.com/watch?v=piISG8bV2GI&list=PLJ5C_6qdAvBGojQMUzL4x5Y0N5gBJmT4l

• https://www.youtube.com/watch?v=KrWSK-UzCRc&list=PLnbFC0ntxiqdpoWwMKCVh6BRwBePHaqQx

• https://www.youtube.com/watch?v=CUno7iGUmAo

• Clause learning : CDCL
• Handbook of SAT
• Conflict Driven Clause Learning - CDCL

• https://www.youtube.com/watch?v=vVMu6g2H50Q

• https://www.youtube.com/channel/UCP2eLEql4tROYmIYm5mA27A/videos

• https://www.youtube.com/watch?v=spcfzbisBv4

• https://github.com/uclid-org/uclid/tree/master/tutorial
• https://cse.iitk.ac.in/users/spramod/papers/memocode18.pdf
• https://cse.iitk.ac.in/users/spramod/papers/ccs17.pdf

• https://theory.stanford.edu/~nikolaj/programmingz3.html
• https://z3prover.github.io/api/html/namespacez3.html
• https://github.com/Z3Prover/z3
• https://ericpony.github.io/z3py-tutorial/guide-examples.htm

• https://users.ece.cmu.edu/~aavgerin/papers/Oakland10.pdf

• Slides : https://lara.epfl.ch/w/_media/sav15:calculus-of-computation-slides.pdf

• http://csl.sri.com/papers/csl-92-2/csl-92-2.pdf

• https://eprint.iacr.org/2019/310
• https://www.cs.cornell.edu/fbs/publications/Hyperproperties.pdf
• https://arxiv.org/pdf/1905.13517.pdf

• Probabilistic Symbolic Execution
• PSE Paper

• Hakaru

• LLVM : Compilers Lab
• LLVM Ball-Laurus Profiler

• CBMC
• ESBMC

• Universal Quantification
• Uniqueness Quantification
• More on Hoare Logic
• Abstract Interpretation

• Use of gcov & gtest
• Example use of gcov, gtest, cmake & make