Property based heurisitcs in Model Checking

Here are some papers that should be read for property based heuristics. There isn't a ton of heuristics stuff. In fact Willam Visser seems to have done the most.

1. Directed explicit model checking with HSF-SPIN
by Stefan Edelkamp, A. Lluch-Lafuente

2. Symbolic guided search for CTL model checking
by R.Bloem, K. Ravi, and F.Somenzi

3. Validation with guided search for the state space
by C.Yang and D. Dill

4. Guided Model Checking with a Bayesian Meta-heuristic
by Kevin Seppi, Mike Jones and Peter Lamborn

Static Analysis for Model Checking

Here are some must read before doing any kind of Static Analysis in Model Checking. This is mostly structural based static analysis. Most everything I have found is in the Java PathFinder. Nobody seems to have done it with Murphi or SPIN. I guess the way Murphi and SPIN are designed, it would really hard to do similar kind of things.

1. Byte Code Distance Heuristics and Trail Direction for Model Checking Java Programs
by Stefan Edelkamp and Tilman Mehler

-- cite this paper for FSM

2. Heuristic Model Checking for Java Programs
by Alex Groce and W. Visser

-- this paper has the interleaving thread stuff

3. Combining Static Analysis and Model Checking for Software Analysis
by G.Brat and W. Visser

-- cite this paper for on-demand heuristic

4. Model Checking Java Programs using Structural Heuristic
by A Groce and W. Visser

-- cite this paper as an example of structural heuristic

NASA - Swades - Pathfinder

This is just an interesting titbit. Only Indians who are hindi movie fans and into Formal Methods will most probably notice this. In the movie "Swades", the main protoganist is a NASA employee and is visiting his own country (Swades). There is manning a bookstore for a friend. The bookstore is called "PathFinder". For all those who are familiar with software Model Checking know that there is a NASA product called the Java PathFinder. So this got me thinking on whether the mention of PathFinder was a coincidence or whether they knew it was a NASA product. The thing is they make it a point to show the name of the shop that what makes me think it is more than a conincidence.

Using Runtime Analysis To Guide Model Checking of Java Programs

This paper takes the Eraser algorithm which detects data races in a program by studying a single run of the program and from that trying to conclude whether any runs with data races are possible.

This was implemented in JPF2 and it can be run Eraser mode. This is implemented specifically to see if there are unprotected variables. This can yield in lots of warnings that are not valid.

For our research, combined with static analysis, a few runs of the programs are done. Relevant data is collected. If there is user input we should test the boundary values in a finite system. And some random values. Mark the critical points in the program and see if the values at those points change drastically or not? If they do change drastically then see what is causing it? Whether it is system stuff or whether it is user stuff or even random? This could help us detect where the major fluctuations occur in the program. This information can be used to guide the heuristic alongwith the static anaylsis. Ideally this information should lie on top of the control flow graph.

Tagore books at BYU

These great Tagore books are available at the BYU library.

Mashi, and other stories
PK 1722 .M374x 1972

Binodini
Translation of the Choker Bali
PK 1723 .C53 E5 1964

Broken Ties, and other short stories
PK 1722 .A2 B76x

Stories from Tagore
PR 6039 .A2 S65 1918a

The hungry stones, and other stories
PK 1722 .A2 H8 1916

Gitanjali
PR 6039 .A2 G6x 1914

The post office
PR 9499 .T34 P6 1914

The Gardener
PR 6039 .A2 G3

The King of the Dark Chamber
PR 6039 .A2 K5 1915

read books online

I found this really good site where you can read a lot of classics online. I started looking for short stories by O Henry and found this site. There are novels, short stories, poems from authors from 18th and 19th Century.

Read books online

This has everything from Mark Twain to Rabindranath Tagore.