@book(principles.mc, author = "C. Baier and J.P. Katoen", year = "2008", title = "Principles of Model Checking", publisher = "The MIT Press", ) @article(barnat.brim.multicore, author = "J. Barnat and L. Brim and P. Ro\v {c}kai", year = "2010", title = "Scalable Shared Memory {LTL} Model Checking", journal = "STTT", volume = "12", number = "2", pages = "139--153", doi = "10.1007/s10009-010-0136-z", ) @inproceedings(BBCR10, author = "J. Barnat and L. Brim and M. \v {C}e\v {s}ka and P. Ro\v {c}kai", year = "2010", title = "{{DiVinE: Parallel Distributed Model Checker (Tool paper)}}", booktitle = "Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology (HiBi/PDMC 2010)", publisher = "IEEE", pages = "4--7", doi = "10.1007/978-3-540-88387-6\_20", ) @inproceedings(owcty-otf, author = "L. Barnat and L. Brim and P. Ro{\v c}kai", year = "2009", title = "A Time-Optimal On-The-Fly Parallel Algorithm for Model Checking of Weak {LTL} Properties", booktitle = "ICFEM 2009", series = "LNCS", volume = "5885", publisher = "Springer, Heidelberg", pages = "407--425", doi = "10.1007/978-3-642-10373-5\_21", ) @inproceedings(BrnoMAP, author = "L. Brim and I. Cern{\'a} and P. Moravec and J. Simsa", year = "2004", title = "Accepting Predecessors Are Better than Back Edges in Distributed {LTL} Model-Checking", editor = "A.J. Hu and A.K. Martin", booktitle = "FMCAD", series = "Lecture Notes in Computer Science", volume = "3312", publisher = "Springer", pages = "352--366", doi = "10.1007/978-3-540-30494-4\_25", ) @article(courcoubetis, author = "C. Courcoubetis and M.Y. Vardi and P. Wolper and M. Yannakakis", year = "1992", title = "{Memory-Efficient Algorithms for the Verification of Temporal Properties}", journal = "Formal Methods in System Design", volume = "1", number = "2/3", pages = "275--288", doi = "10.1007/BFb0023737", ) @inproceedings(Evangelista11, author = "S. Evangelista and L. Petrucci and S. Youcef", year = "2011", title = "Parallel Nested Depth-First Searches for {LTL} Model Checking", editor = "T. Bultan and P.-A. Hsiung", booktitle = "Automated Technology for Verification and Analysis 2011", series = "Lecture Notes in Computer Science", volume = "6996", publisher = "Springer", pages = "381--396", doi = "10.1007/978-3-642-24372-1\_27", ) @techreport(report, author = "S. Evangelista and L. Petrucci and S. Youcef", year = "Last accessed 15 Sept 2011", title = "Parallel Nested Depth-First Searches for {LTL} Model Checking", type = "Technical Report", institution = "Universit\'e Paris 13", url = "http://www-lipn.univ-paris13.fr/~evangelista/doc/mc-ndfs.pdf", ) @inproceedings(gaiser, author = "A. Gaiser and S. Schwoon", year = "2009", title = "Comparison of Algorithms for Checking Emptiness on B{\"u}chi Automata", editor = "P. Hlinen{\'y} and V. Maty{\'a}{\v {s}} and T. Vojnar", booktitle = "MEMICS'09", series = "OpenAccess Series in Informatics (OASIcs)", volume = "13", address = "Schloss Dagstuhl, Germany", doi = "10.4230/DROPS.MEMICS.2009.2349", ) @inproceedings(holzmann-swarm, author = "G.J. Holzmann and R. Joshi and A. Groce", year = "2008", title = "Swarm Verification", booktitle = "ASE", publisher = "IEEE", address = "L'Aquila, Italy", pages = "1--6", doi = "10.1109/ASE.2008.9", ) @inproceedings(holzmann-ndfs, author = "G.J. Holzmann and D. Peled and M. Yannakakis", year = "1996", title = "{On Nested Depth First Search}", booktitle = "The {SPIN} Verification System", publisher = "American Mathematical Society", pages = "23--32", ) @inproceedings(HyvarinenJN08, author = "A.E.J. Hyv{\"a}rinen and T.A. Junttila and I. Niemel{\"a}", year = "2008", title = "Strategies for Solving {SAT} in Grids by Randomized Search", editor = "S. Autexier and J. Campbell and J. Rubio and V. Sorge and M. Suzuki and F. Wiedijk", booktitle = "AISC/MKM/Calculemus", series = "LNCS 5144", publisher = "Springer", pages = "125--140", doi = "10.1007/978-3-540-85110-3\_11", ) @inproceedings(Laarman11, author = "A.W. Laarman and R. Langerak and J.C. van de Pol and M. Weber and A. Wijs", year = "2011", title = "Multi-Core Nested Depth-First Search", editor = "T. Bultan and P.-A. Hsiung", booktitle = "Automated Technology for Verification and Analysis 2011", series = "Lecture Notes in Computer Science", volume = "6996", publisher = "Springer", pages = "321--335", doi = "10.1007/978-3-642-24372-1\_23", ) @inproceedings(freelunch, author = "A.W. Laarman and J.C. van de Pol and M. Weber", year = "2011", title = "Parallel Recursive State Compression for Free", editor = "A. Groce and M. Musuvathi", booktitle = "SPIN", series = "Lecture Notes in Computer Science", volume = "6823", publisher = "Springer", address = "Snowbird, USA", pages = "38--56", doi = "10.1007/978-3-642-22306-8\_4", ) @inproceedings(boosting, author = "A.W. {Laarman} and J.C. {van de Pol} and M. {Weber}", year = "2010", title = "{Boosting Multi-Core Reachability Performance with Shared Hash Tables}", editor = "N. Sharygina and R. Bloem", booktitle = "Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design, Lugano, Swiss", publisher = "IEEE Computer Society", address = "USA", pages = "247--256", url = "http://eprints.eemcs.utwente.nl/18437/", ) @inproceedings(ltsmin, author = "A.W. {Laarman} and J.C. {van de Pol} and M. {Weber}", year = "2011", title = "Multi-Core {LTSmin}: Marrying Modularity and Scalability", editor = "M. {Bobaru} and K. {Havelund} and G. {Holzmann} and R. {Joshi}", booktitle = "Proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011, Pasadena, CA, USA", series = "LNCS", volume = "6617", publisher = "Springer Verlag", address = "Berlin", pages = "506--511", doi = "10.1007/978-3-642-20398-5\_40", ) @inproceedings(beem, author = "R. Pel\'anek", year = "2007", title = "{BEEM: Benchmarks for Explicit Model Checkers}", booktitle = "Proc. of SPIN Workshop", series = "LNCS", volume = "4595", publisher = "Springer", pages = "263--267", doi = "10.1007/978-3-540-73370-6\_17", ) @article(reif, author = "J.H. Reif", year = "1985", title = "Depth-first {S}earch is {I}nherently {S}equential", journal = "Information Processing Letters", volume = "20", number = "5", pages = "229--234", doi = "10.1016/0020-0190(85)90024-9", ) @inproceedings(schwoon, author = "S. Schwoon and J. Esparza", year = "2005", title = "{A Note on On-the-Fly Verification Algorithms}", editor = "Nicolas Halbwachs and Lenore D. Zuck", booktitle = "Tools and Algorithms for the Construction and Analysis of Systems", series = "Lecture Notes in Computer Science", volume = "3440", publisher = "Springer", pages = "174--190", doi = "10.1007/978-3-540-31980-1\_12", ) @inproceedings(AutoVerif1986, author = "M.Y. Vardi and P. Wolper", year = "1986", title = "An Automata-Theoretic Approach to Automatic Program Verification", booktitle = "Proc. 1st Symp. on Logic in Computer Science", address = "Cambridge", pages = "332--344", url = "http://www.cs.rice.edu/~vardi/papers/lics86.pdf.gz", ) @inproceedings(BrnoOWCTY, author = "I. \v {C}ern{\'a} and R. Pel{\'a}nek", year = "2003", title = "Distributed Explicit Fair Cycle Detection (Set Based Approach)", editor = "T. Ball and S.K. Rajamani", booktitle = "SPIN", series = "Lecture Notes in Computer Science", volume = "2648", publisher = "Springer", pages = "49--73", doi = "10.1007/3-540-44829-2\_4", )