Skip to content

Program Analysis, Software Verification & Testing. Python3, CAS, Dafny, Z3, CVC4, UCLID, ZChaff, NuSMV, AFL, Scala, CBMC & LLVM Framework (CO).

License

Notifications You must be signed in to change notification settings

codersguild/Software-Analysis-PAVT

Repository files navigation

Program Analysis, Testing & Formal Verification :

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.

Figures

ACM Winter School :

Some cool paper links.

Reading Material & Book References

Some Methods & Basic Resources :

  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 :

Program Analysis & Verification

Fantastic videos by Dr. Subhajit Roy (IIT Kanpur)

Simple Inductions :

Tree Data Structure Induction :

Natural Deductions :

  1. 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.

Turing Machine, As an extension to FSM :

Model Checking :

How we model and define properties :

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.

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

Hoare Logic :

Binary Search Verification in Dafny :

Dafny PDF :

Calculus of Computation :

Hyperproperties :

Hedra Formal Methods :

Detailed Study : For Research Orientated Learning

What is Computer Security ?

Propositional Natural Deductions :

First Order Natural Deductions :

Hoare Logic Link :

Hoare Logic + Loops :

Induction :

Tree Induction :

Model Checking - 1 :

Model Chceking - 2 :

Linear Temporal Logic :

Clause Learning (CDCL) :

Hyperproperties :

Verification Corner Dafny :

Verification Corner Loop Invariants :

UCLID5 :

UCLID5 is based on Z3. Z3 Reference :

Dynamic Taint Analysis :

The Calculus of Computation. (Bradley & Manna)

Non-Interference :

Hyperproperties :

Probabilistic Symbolic Execution :

Probabilistic Programming :

LLVM Frameworks :

Model Checkers :

Concepts/Topics :

Hands-On Stuff & Tutorials I made :