SVNITPhDbibtex.bib

% % %My publication
@book{B-Principle,
  author = {Baier, Christel, Katoen and Joost-Pieter},
  title = {Principles of Model Checking (Representation and Mind Series)},
  year = {2008},
  isbn = {026202649X, 9780262026499},
  publisher = {The MIT Press},
} 

@inproceedings{MC:Clarke,
  author    = {Edmund M. Clarke},
  title     = {Model Cheking},
  year      = {1997},
  pages     = {54--56},
  booktitle = {Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 17th Conference}, 
  address   = {Kharagpur, India}, 
  month     = {December}, 
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1346},
}

@article{BAN,
 author = {Burrows, Michael and Abadi, Martin and Needham, Roger},
 title = {A logic of authentication},
 journal = {ACM Trans. Comput. Syst.},
 volume = {8},
 number = {1},
 month = feb,
 year = {1990},
 issn = {0734-2071},
 pages = {18--36},
 numpages = {19},
 publisher = {ACM},
 address = {New York, NY, USA},
}

@book{Paulson,
  author    = {Lawrence C. Paulson},
  title     = {Isabelle - A Generic Theorem Prover (with a contribution
               by T. Nipkow)},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {828},
  year      = {1994},
}

@inproceedings{MC:Birth,
  author    = {Edmund M. Clarke},
  title     = {The Birth of Model Checking},
  booktitle = {25 Years of Model Checking},
  year      = {2008},
  pages     = {1-26},
}

@article{6:Hoare,
 author = {Hoare, C. A. R.},
 title = {An axiomatic basis for computer programming},
 journal = {Commun. ACM},
 issue_date = {Oct. 1969},
 volume = {12},
 number = {10},
 month = {oct},
 year = {1969},
 pages = {576--580},
}

@TECHREPORT{CSMV,
  AUTHOR = {K. L. McMillan},
  TITLE = {The {SMV} Language},
  INSTITUTION = {Cadence Berkeley Labs},
  YEAR = 1999,
  MONTH = {March}
}

@article{NuSMV,
  author    = {Alessandro Cimatti and
               Edmund M. Clarke and
               Fausto Giunchiglia and
               Marco Roveri},
  title     = {NUSMV: A New Symbolic Model Checker},
  journal   = {International Journal on Software Tools for Technology Transfer},
  volume    = {2},
  number    = {4},
  year      = {2000},
  pages     = {410-425},
}

@inproceedings{LTL,
  author = {Pnueli, Amir},
  title = {The temporal logic of programs},
  booktitle = {Proceedings of the 18th Annual Symposium on Foundations of Computer Science},
  series = {SFCS '77},
  year = {1977},
  pages = {46--57},
  publisher = {IEEE Computer Society},
  address = {Washington, DC, USA},
}

@misc{Thesis-PTools,
  month = {May},
  title = {Probabilistic model checking : a comparison of tools},
  author = {H.A. {Oldenkamp}},
  year = {2007},
..url = {http://essay.utwente.nl/591/},
}

@article{ETMCC,
  author    = {Holger Hermanns and Joost-Pieter Katoen and Joachim Meyer-Kayser and Markus Siegle},
  title     = {A tool for model-checking Markov chains},
  journal   = {STTT},
  volume    = {4},
  number    = {2},
  year      = {2003},
  pages     = {153--172},
}

@inproceedings{MRMC,
  author = {Katoen, Joost-Pieter and Khattri, Maneesh and Zapreev, Ivan S.},
  title = {A Markov Reward Model Checker},
  booktitle = {Proceedings of the Second International Conference on the Quantitative Evaluation of Systems},
  series = {QEST '05},
  year = {2005},
  pages = {243--244},
  publisher = {IEEE Computer Society},
  address = {Washington, DC, USA},
} 

@inproceedings{YMER,
  author = {Younes, H{\aa}kan L. S.},
  title = {{YMER}: a statistical model checker},
  booktitle = {Proceedings of the 17th international conference on Computer Aided Verification},
  series = {CAV'05},
  year = {2005},
  location = {Edinburgh, Scotland, UK},
  pages = {429--433},
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg},
}

@inproceedings{VESTA,
  author = {Sen, Koushik and Viswanathan, Mahesh and Agha, Gul A.},
  title = {{VESTA}: A Statistical Model-checker and Analyzer for Probabilistic Systems},
  booktitle = {Second International Conference on the Quantitative Evaluaiton of Systems (QEST 2005)},
  month = {September},
  address = {Torino, Italy},
  pages = {251--252},
  year = {2005},
  publisher = {IEEE Computer Society},
}

% % % % % % % % % % % % % % % % % % % % %PRISM


@inproceedings{PRISM:Advances,
 author = {Katoen, Joost-Pieter},
 title = {Advances in probabilistic model checking},
 booktitle = {Proceedings of the 11th international conference on Verification, Model Checking, and Abstract Interpretation},
 series = {VMCAI'10},
 year = {2010},
 pages = {25--25},
 numpages = {1},
 publisher = {Springer-Verlag},
} 


@inproceedings{PRISM-Tool,
  author    = {Andrew Hinton and Marta Z. Kwiatkowska and Gethin Norman and David Parker},
  title     = {{PRISM}: A Tool for Automatic Verification of Probabilistic Systems},
  booktitle={Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06)},
  year      = {2006},
  pages     = {441--444},
  address   = {Vienna, Austria}, 
  month     = {March},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3920},
}

@inproceedings{PRISM-model,
  author = {Kwiatkowska, Marta Z. and Norman, Gethin and Parker, David},
  title = {{PRISM}: Probabilistic Symbolic Model Checker},
  booktitle = {Proceedings of the 12th International Conference on Computer Performance Evaluation, Modelling Techniques and Tools},
  series = {TOOLS '02},
  year = {2002},
  pages = {200--204},
  publisher = {Springer-Verlag},
  address = {London, UK, UK},
} 

@inproceedings{PRISM:ProbSymmetry,
 author = {Kwiatkowska, Marta and Norman, Gethin and Parker, David},
 title = {Symmetry reduction for probabilistic model checking},
 booktitle = {Proceedings of the 18th international conference on Computer Aided Verification},
 series = {CAV'06},
 year = {2006},
 pages = {234--248},
 numpages = {15},
 publisher = {Springer-Verlag},
} 


@Misc{18:State_SYmmetry,
author = {Christian Appold},
title = {Using State Symmetries to Speed up Symmetry Reduction in Model Checking},
}


@Misc{11:Approach_Prob,
author = {Christopher Power and Alice Miller},
title = {An Approach to Probabilistic Symmetry Reduction},
}

@article{Symbolic:1020,
title = "Symbolic model checking: $10^{20}$ States and beyond ",
journal = "Information and Computation ",
volume = "98",
number = "2",
pages = "142 - 170",
year = "1992",
author = "J.R. Burch and E.M. Clarke and K.L. McMillan and D.L. Dill and L.J. Hwang"
}

@article{BDD,
 author = {Bryant, Randal E.},
 title = {Graph-Based Algorithms for Boolean Function Manipulation},
 journal = {IEEE Trans. Comput.},
 issue_date = {August 1986},
 volume = {35},
 number = {8},
 month = aug,
 year = {1986},
 pages = {677--691},
 publisher = {IEEE Computer Society},
 address = {Washington, DC, USA},
}

@PhdThesis{PRISM:Dave_Thesis,
.title = {Implementation of symbolic model checking for probabilistic systems},
 school = {University of Birmingham},
 author = {David Anthony Parker},
 year = {2003},
 url = {http://etheses.bham.ac.uk/229/},
}

@article{MTBDD,
 author = {Fujita, M. and McGeer, P. C. and Yang, J. C.-Y.},
 title = {Multi-Terminal Binary Decision Diagrams: An Efficient DataStructure for Matrix Representation},
 journal = {Form. Methods Syst. Des.},
 issue_date = {April -May  1997},
 volume = {10},
 number = {2-3},
 month = apr,
 year = {1997},
 pages = {149--169},
 numpages = {21},
} 

@article{PRISM:Hybrid,
 author = {Kwiatkowska, Marta and Norman, Gethin and Parker, David},
 title = {Probabilistic symbolic model checking with PRISM: a hybrid approach},
 journal = {Int. J. Softw. Tools Technol. Transf.},
 issue_date = {August 2004},
 volume = {6},
 number = {2},
 month = aug,
 year = {2004},
 issn = {1433-2779},
 pages = {128--142},
 numpages = {15},
 publisher = {Springer-Verlag},
} 

@inproceedings{MTBDD:Ref1,
author = {H. {Hermanns} and J. {Meyer-Kayser} and M. {Siegle}},
num_pages = {20},
booktitle = {3rd Int. Workshop on the Numerical Solution of Markov Chains, Zaragossa, Spain},
title = {Multi Terminal Binary Decision Diagrams to Represent and Analyse Continuous Time Markov Chains},
pages = {188--207},
year = {1999},
}

@incollection{MTBDD:Ref2,
year={1997},
booktitle={Automata, Languages and Programming},
volume={1256},
series={Lecture Notes in Computer Science},
title={Symbolic model checking for probabilistic processes},
publisher={Springer Berlin Heidelberg},
author={Baier, Christel and Clarke, EdmundM. and Hartonas-Garmhausen, Vasiliki and Kwiatkowska, Marta and Ryan, Mark},
pages={430-440},
}

@incollection{MTBDD:Ref3,
year={1999},
booktitle={Formal Methods for Real-Time and Probabilistic Systems},
volume={1601},
series={Lecture Notes in Computer Science},
title={ProbVerus: Probabilistic Symbolic Model Checking},
publisher={Springer Berlin Heidelberg},
author={Hartonas-Garmhausen, Vicky and Campos, Sergio and Clarke, Ed},
pages={96-110},
}



% % % % % %Related Work References % % % % % %
@article{21:Employ_Symmetry,
title = "Employing symmetry reductions in model checking ",
journal = "Computer Languages, Systems \& Structures ",
volume = "30",
number = "3–4",
pages = "99 - 137",
year = "2004",
author = "A.Prasad Sistla",
}

@inproceedings{22:Symmetry_explicit,
booktitle = {First International Symmetry Conference},
title = {Symmetry reduction techniques for explicit-state model checking},
author = {A. Donaldson and A. Miller},
year = {2007},
pages = {41--45},
}

@article{23:Temporal,
 author = {Miller, Alice and Donaldson, Alastair and Calder, Muffy},
 title = {Symmetry in temporal logic model checking},
 journal = {ACM Comput. Surv.},
 issue_date = {2006},
 volume = {38},
 number = {3},
 month = sep,
 year = {2006},
 publisher = {ACM},
} 

@Article{24:Replication,
AUTHOR = {Wahl, Thomas and Donaldson, Alastair},
TITLE = {Replication and Abstraction: Symmetry in Automated Formal Verification},
JOURNAL = {Symmetry},
VOLUME = {2},
YEAR = {2010},
NUMBER = {2},
PAGES = {799--847},
}

@PhdThesis{25:Automatic,
author = {Donaldson, A.F.},
title = {Automatic Techniques for Detecting and Exploiting Symmetry in Model Checking},
school = {University of Glasgow},
year = {2007},
month = {June},
}


@book{26:Symmetry_Science,
  title={Symmetry in Science: An Introduction to the General Theory},
  author={Rosen, J.},
  series={Springer study edition},
  year={1995},
  publisher={SPRINGER VERLAG GMBH}
}

@article{27:Symmetry_model,
author={Emerson, E.Allen and Sistla, A.Prasad},
year={1996},
journal={Formal Methods in System Design},
volume={9},
number={1-2},
title={Symmetry and model checking},
publisher={Kluwer Academic Publishers},
pages={105-131},
}

@article{28:Exploting_temporal,
 author = {Clarke, E. M. and Enders, R. and Filkorn, T. and Jha, S.},
 title = {Exploiting symmetry in temporal logic model checking},
 journal = {Form. Methods Syst. Des.},
 issue_date = {Aug. 1996},
 volume = {9},
 number = {1-2},
 month = aug,
 year = {1996},
 pages = {77--104},
 numpages = {28},
}

@article{29:Better_Verification,
 author = {Ip, C. Norris and Dill, David L.},
 title = {Better verification through symmetry},
 journal = {Form. Methods Syst. Des.},
 issue_date = {Aug. 1996},
 volume = {9},
 number = {1-2},
 month = aug,
 year = {1996},
 pages = {41--75},
 numpages = {35},
}

@article{211:Under_Approx,
 author = {Barner, Sharon and Grumberg, Orna},
 title = {Combining symmetry reduction and under-approximation for symbolic model checking},
 journal = {Form. Methods Syst. Des.},
 issue_date = {September 2005},
 volume = {27},
 number = {1-2},
 month = {sep},
 year = {2005},
 pages = {29--66},
 numpages = {38},
}

@inproceedings{212:Dynamic_Symmetry,
 author = {Emerson, E. Allen and Wahl, Thomas},
 title = {Dynamic symmetry reduction},
 booktitle = {Proceedings of the 11th international conference on Tools and Algorithms for the Construction and Analysis of Systems},
 series = {TACAS'05},
 year = {2005},
 pages = {382--396},
 numpages = {15},
 publisher = {Springer-Verlag},
} 

@inproceedings{213:Counter_abstraction,
 author = {Pnueli, Amir and Xu, Jessie and Zuck, Lenore D.},
 title = {Liveness with (0, 1, infty)-Counter Abstraction},
 booktitle = {Proceedings of the 14th International Conference on Computer Aided Verification},
 series = {CAV '02},
 year = {2002},
 isbn = {3-540-43997-8},
 pages = {107--122},
 numpages = {16},
 url = {http://dl.acm.org/citation.cfm?id=647771.734286},
 acmid = {734286},
 publisher = {Springer-Verlag},
 address = {London, UK, UK},
} 

@inproceedings{214:Asymmetry,
 author = {Emerson, E. Allen and Trefler, Richard J.},
 title = {From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking},
 booktitle = {Proceedings of the 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods},
 series = {CHARME '99},
 year = {1999},
 pages = {142--156},
 numpages = {15},
}
@inproceedings{215:UPPAL,
  author    = {Martijn Hendriks and
               Gerd Behrmann and
               Kim Guldstrand Larsen and
               Peter Niebert and
               Frits W. Vaandrager},
  title     = {Adding Symmetry Reduction to Uppaal},
  booktitle = {FORMATS},
  year      = {2003},
  pages     = {46-59},
}

@inproceedings{216:RED,
 author = {Wang, Farn and Schmidt, Karsten},
 title = {Symmetric Symbolic Safety-Analysis of Concurrent Software with Pointer Data Structures},
 booktitle = {Proceedings of the 22nd IFIP WG 6.1 International Conference Houston on Formal Techniques for Networked and Distributed Systems},
 series = {FORTE '02},
 year = {2002},
 pages = {50--64},
 numpages = {15},
 publisher = {Springer-Verlag},
}

@article{217:SMC,
 author = {Sistla, A. Prasad and Gyuris, Viktor and Emerson, E. Allen},
 title = {SMC: a symmetry-based model checker for verification of safety and liveness properties},
 journal = {ACM Trans. Softw. Eng. Methodol.},
 issue_date = {April 2000},
 volume = {9},
 number = {2},
 month = apr,
 year = {2000},
 pages = {133--166},
 numpages = {34},
 publisher = {ACM},
}

@article{PCTL,
  author    = {Hans Hansson and Bengt Jonsson},
  title     = {A Logic for Reasoning about Time and Reliability},
  journal   = {Formal Aspects of Computing},
  volume    = {6},
  number    = {5},
  year      = {1994},
  pages     = {512--535},
}

@inproceedings{CTL,
  author = {Clarke, Edmund M. and Emerson, E. Allen},
  title = {Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic},
  booktitle = {Logic of Programs, Workshop},
  year = {1982},
  pages = {52--71},
  publisher = {Springer-Verlag},
  address = {London, UK, UK},
} 

@inproceedings{CSL,
  title = {Verifying Continuous Time Markov Chains},
  author = {Adnan Aziz and Kumud Sanwal and Vigyan Singhal and Robert K. Brayton},
  year = {1996},
  tags = {Markov},
  pages = {269--276},
  booktitle = {Computer Aided Verification, 8th International Conference, CAV  96, New Brunswick, NJ, USA, July 31 - August 3, 1996, Proceedings},
  editor = {Rajeev Alur and Thomas A. Henzinger},
  volume = {1102},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
}

% % % % % % % % % % % % %
@inproceedings{ADD,
 author = {Bahar, R. Iris and Frohm, Erica A. and Gaona, Charles M. and Hachtel, Gary D. and Macii, Enrico and Pardo, Abelardo and Somenzi, Fabio},
 title = {Algebraic decision diagrams and their applications},
 booktitle = {Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design},
 series = {ICCAD '93},
 year = {1993},
 pages = {188--191},
 numpages = {4},
 publisher = {IEEE Computer Society Press},
}

@inproceedings{ZBDD,
 author = {Minato, Shin-ichi},
 title = {Zero-suppressed BDDs for set manipulation in combinatorial problems},
 booktitle = {Proceedings of the 30th international Design Automation Conference},
 series = {DAC '93},
 year = {1993},
 pages = {272--277},
 numpages = {6},
 publisher = {ACM},
}

@article{PRISM_Quanti,
 author = {Kwiatkowska, Marta and Norman, Gethin and Parker, David},
 title = {Quantitative Analysis With the Probabilistic Model Checker PRISM},
 journal = {Electron. Notes Theor. Comput. Sci.},
 issue_date = {May, 2006},
 volume = {153},
 number = {2},
 month = may,
 year = {2006},
 pages = {5--31},
 numpages = {27},
 publisher = {Elsevier Science Publishers B. V.},
}

@Misc{CUDD,
author = {Fabio Somenzi},
title = {CUDD: CU Decision Diagram Package Release 2.5.0},
url = {http://vlsi.colorado.edu/~fabio/CUDD/},
}

@InBook{Dice,
author={D. Knuth and A. Yao},
title={Algorithms and Complexity: New Directions and Recent Results},
chapter={The complexity of nonuniform random number generation},
publisher={Academic Press},
year={1976},
}

@Article{Her90,
author={T. Herman},
title={Probabilistic Self-stabilization},
journal={Information Processing Letters},
year={1990},
volume={35},
number={2},
pages={63--67},
}

@InProceedings{Phill,
author={D. Lehmann and M. Rabin},
title={On the Advantage of Free Choice: {A} Symmetric and Fully Distributed Solution to the Dining Philosophers Problem (Extended Abstract)},
booktitle={Proc. 8th Annual ACM Symposium on Principles of Programming Languages (POPL'81)},
year={1981},
pages={133--138},
}

@article{Mutual,
 author = {Lamport, Leslie},
 title = {The mutual exclusion problem: part I - theory of interprocess communication},
 journal = {J. ACM},
 issue_date = {April 1986},
 volume = {33},
 number = {2},
 month = apr,
 year = {1986},
 pages = {313--326},
 numpages = {14},
 publisher = {ACM},
}

@article{CTMC,
  author = {Baier, Christel and Haverkort, Boudewijn and Hermanns, Holger and Katoen, Joost-Pieter},
  title = {Model-Checking Algorithms for Continuous-Time Markov Chains},
  journal = {IEEE Trans. Softw. Eng.},
  volume = {29},
  number = {6},
  month = {june},
  year = {2003},
  pages = {524--541},
  publisher = {IEEE Press},
  address = {Piscataway, NJ, USA},
} 

@inproceedings{MDP,
 author={A. Bianco and L. de Alfaro},
 title={Model Checking of Probabilistic and Nondeterministic Systems},
 booktitle={Proc. 15th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'95)},
 year={1995},
 editor={P. Thiagarajan},
 pages={499--513},
 publisher={Springer},
 series={LNCS},
 volume={1026},
 }
 
 @book{DTMC,
   author = {Kulkarni, Vidyadhar G.},
   title = {Modeling and analysis of stochastic systems},
   year = {1995},
   publisher = {Chapman \& Hall, Ltd.},
   address = {London, UK, UK},
 }

@Misc{PRISM_Website,
title = {PRISM Website},
url = {http://www.prismmodelchecker.org/},
}


 %%%% New for RPS3 
 
 @article{LazySR,
  author = {Wahl, Thomas and DSilva, Vijay},
  title = {A Lazy Approach to Symmetry Reduction},
  journal = {Form. Asp. Comput.},
  issue_date = {November 2010},
  volume = {22},
  number = {6},
  month = nov,
  year = {2010},
  pages = {713--733},
  numpages = {21},
  publisher = {Springer-Verlag},
  } 
 
  @incollection{AdaptiveSR,
 year={2007},
 booktitle={Computer Aided Verification},
 volume={4590},
 series={Lecture Notes in Computer Science},
 title={Adaptive Symmetry Reduction},
publisher={Springer Berlin Heidelberg},
 author={Wahl, Thomas},
 pages={393-405}
 }
 
 @inproceedings{VirtualSR,
  author = {Emerson, E. Allen and Havlicek, John W. and Trefler, Richard J.},
  title = {Virtual Symmetry Reduction},
  booktitle = {Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science},
  series = {LICS '00},
  year = {2000},
  publisher = {IEEE Computer Society},
} 

@article{Kripke,
	volume = {16},
	number = {1963},
	author = {Saul A. Kripke},
	title = {Semantical Considerations on Modal Logic},
	journal = {Acta Philosophica Fennica},
	year = {1963},
	pages = {83--94}
}