@incollection(Alur-Henzinger-others-98, author = "R. Alur and T. Henzinger and F. Mang and S. Qadeer and S. Rajamani and S. Tasiran", year = "1998", title = "MOCHA: Modularity in model checking", editor = "Alan Hu and Moshe Vardi", booktitle = "Computer Aided Verification", series = "Lecture Notes in Computer Science", volume = "1427", publisher = "Springer Berlin / Heidelberg", pages = "521--525", doi = "10.1007/BFb0028774", ) @article(Buccafurri-Eiter-others-01, author = "F. Buccafurri and T. Eiter and G. Gottlob and N. Leone", year = "2001", title = "On {ACTL} Formulas Having Linear Counterexamples", journal = "Journal of Computer and System Sciences", volume = "62", number = "3", pages = "463 -- 515", doi = "10.1006/jcss.2000.1734", ) @article(Chaum-88, author = "D. Chaum", year = "1988", title = "The dining cryptographers problem: Unconditional sender and recipient untraceability", journal = "Journal of Cryptology", volume = "1", pages = "65--75", doi = "10.1007/BF00206326", ) @incollection(Cimatti-Clarke-others-02, author = "A. Cimatti and E. M. Clarke and E. Giunchiglia and F. Giunchiglia and M. Pistore and M. Roveri and R. Sebastiani and A. Tacchella", year = "2002", title = "NuSMV 2: An OpenSource Tool for Symbolic Model Checking", editor = "Ed Brinksma and Kim Larsen", booktitle = "Computer Aided Verification", series = "Lecture Notes in Computer Science", volume = "2404", publisher = "Springer Berlin / Heidelberg", pages = "241--268", doi = "10.1007/3-540-45657-0\_29", ) @incollection(Clarke-Emerson-82, author = "E. M. Clarke and E. A. Emerson", year = "1982", title = "Design and synthesis of synchronization skeletons using branching time temporal logic", editor = "Dexter Kozen", booktitle = "Logics of Programs", series = "Lecture Notes in Computer Science", volume = "131", publisher = "Springer Berlin / Heidelberg", pages = "52--71", doi = "10.1007/BFb0025774", ) @book(Clarke-Grumberg-others-99, author = "E. M. Clarke and O. Grumberg and D. Peled", year = "1999", title = "Model Checking", publisher = "{MIT Press}", ) @inproceedings(Clarke-Jha-others-02, author = "E. M. Clarke and S. Jha and Y. Lu and H. Veith", year = "2002", title = "Tree-Like Counterexamples in Model Checking", booktitle = "Proc. of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002)", pages = "19--29", doi = "10.1109/LICS.2002.1029814", ) @article(Copty-Irron-others-03, author = "F. Copty and A. Irron and O. Weissberg and N. Kropp and G. Kamhi", year = "2003", title = "Efficient debugging in a formal verification environment", journal = "International Journal on Software Tools for Technology Transfer (STTT)", volume = "4", pages = "335--348", doi = "10.1007/s10009-002-0097-y", ) @inproceedings(Dong-Ramakrishnan-others-03, author = "Y. Dong and C. R. Ramakrishnan and S. A. Smolka", year = "2003", title = "Model Checking and Evidence Exploration", booktitle = "Proc. of the 10th IEEE International Conference on Engineering of Computer-Based Systems (ECBS 2003)", pages = "214--223", doi = "10.1109/ECBS.2003.1194802", ) @inproceedings(Gammie-Meyden-04, author = "P. Gammie and R. van der Meyden", year = "2004", title = "{MCK}: Model Checking the Logic of Knowledge", booktitle = "Proceedings of 16th International Conference on Computer Aided Verification (CAV'04)", series = "LNCS", volume = "3114", publisher = "Springer-Verlag", pages = "479--483", doi = "10.1007/978-3-540-27813-9\_41", ) @incollection(Groce-Visser-03, author = "A. Groce and W. Visser", year = "2003", title = "What Went Wrong: Explaining Counterexamples", editor = "Thomas Ball and Sriram Rajamani", booktitle = "Model Checking Software", series = "Lecture Notes in Computer Science", volume = "2648", publisher = "Springer Berlin / Heidelberg", pages = "121--136", doi = "10.1007/3-540-44829-2\_8", ) @incollection(Gurfinkel-Chechik-03, author = "A. Gurfinkel and M. Chechik", year = "2003", title = "Proof-Like Counter-Examples", editor = "Hubert Garavel and John Hatcliff", booktitle = "Tools and Algorithms for the Construction and Analysis of Systems", series = "Lecture Notes in Computer Science", volume = "2619", publisher = "Springer Berlin / Heidelberg", pages = "160--175", doi = "10.1007/3-540-36577-X\_12", ) @article(Jin-Ravi-others-04, author = "H. S. Jin and K. Ravi and F. Somenzi", year = "2004", title = "Fate and free will in error traces", journal = "International Journal on Software Tools for Technology Transfer (STTT)", volume = "6", pages = "102--116", doi = "10.1007/s10009-004-0146-9", ) @inproceedings(Lomuscio-Pecheur-others-07, author = "A. Lomuscio and C. Pecheur and F. Raimondi", year = "2007", title = "Automatic Verification of Knowledge and Time with NuSMV", booktitle = "Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI 2007)", pages = "1384--1389", url = "http://hdl.handle.net/2078.1/79759", ) @incollection(Lomuscio-Raimondi-06, author = "A. Lomuscio and F. Raimondi", year = "2006", title = "MCMAS: A Model Checker for Multi-agent Systems", editor = "Holger Hermanns and Jens Palsberg", booktitle = "Tools and Algorithms for the Construction and Analysis of Systems", series = "Lecture Notes in Computer Science", volume = "3920", publisher = "Springer Berlin / Heidelberg", pages = "450--454", doi = "10.1007/11691372\_31", ) @incollection(Meolic-Fantechi-others-04, author = "R. Meolic and A. Fantechi and S. Gnesi", year = "2004", title = "Witness and Counterexample Automata for {ACTL}", editor = "David de Frutos-Escrig and Manuel N{\'u}{\~n}ez", booktitle = "Formal Techniques for Networked and Distributed Systems -- FORTE 2004", series = "Lecture Notes in Computer Science", volume = "3235", publisher = "Springer Berlin / Heidelberg", pages = "259--275", doi = "10.1007/978-3-540-30232-2\_17", ) @incollection(Pecheur-Raimondi-07, author = "C. Pecheur and F. Raimondi", year = "2007", title = "Symbolic Model Checking of Logics with Actions", editor = "Stefan Edelkamp and Alessio Lomuscio", booktitle = "Model Checking and Artificial Intelligence", series = "Lecture Notes in Computer Science", volume = "4428", publisher = "Springer Berlin / Heidelberg", pages = "113--128", doi = "10.1007/978-3-540-74128-2\_8", ) @article(Penczek-Lomuscio-03, author = "W. Penczek and A. Lomuscio", year = "2003", title = "Verifying Epistemic Properties of multi-agent systems via bounded model checking", journal = "Fundamenta Informaticae", volume = "55", number = "2", pages = "167--185", doi = "10.1145/860606.860609", ) @article(penczek-wozna-others-02a, author = "W. Penczek and B. Wozna and A. Zbrzezny", year = "2002", title = "Bounded Model Checking for the Universal Fragment of CTL", journal = "Fundam. Inform.", volume = "51", number = "1-2", pages = "135--156", url = "http://iospress.metapress.com/content/p4dgu2g0tqgtyh4b/", ) @incollection(Rasse-92, author = "A. Rasse", year = "1992", title = "Error diagnosis in finite communicating systems", editor = "Kim Larsen and Arne Skou", booktitle = "Computer Aided Verification", series = "Lecture Notes in Computer Science", volume = "575", publisher = "Springer Berlin / Heidelberg", pages = "114--124", doi = "10.1007/3-540-55179-4\_12", ) @incollection(Shoham-Grumberg-03, author = "S. Shoham and O. Grumberg", year = "2003", title = "A Game-Based Framework for {CTL} Counterexamples and 3-Valued Abstraction-Refinement", editor = "Rebecca Wright", booktitle = "Financial Cryptography", series = "Lecture Notes in Computer Science", volume = "2742", publisher = "Springer Berlin / Heidelberg", pages = "275--287", doi = "10.1007/978-3-540-45069-6\_28", ) @incollection(Stevens-Stirling-98, author = "P. Stevens and C. Stirling", year = "1998", title = "Practical model-checking using games", editor = "Bernhard Steffen", booktitle = "Tools and Algorithms for the Construction and Analysis of Systems", series = "Lecture Notes in Computer Science", volume = "1384", publisher = "Springer Berlin / Heidelberg", pages = "85--101", doi = "10.1007/BFb0054166", )