Software Model Checking with Spin

Abadi, 1991, The existence of refinement mappings, Theoretical Computer Science, 82, 253, 10.1016/0304-3975(91)90224-P Aho, 1974 Bartlett, 1969, A note on reliable full-duplex transmission over half-duplex lines, Comm. of the ACM, 12, 260, 10.1145/362946.362970 Bloom, 2004, Spacetime trade-offs in hash coding with allowable errors, Comm. of the ACM, 13, 422, 10.1145/362686.362692 Bochmann G.V., “Finite state description of communications protocols”, Publication No. 236, Département d'informatique, Université de Montreal, July 1976 Bozga D.M., “Verification symbolique pour les protocoles de communication”, PhD Thesis (in French), University of Grenoble, France, December 1999, Chapter 4 Bryant, 1986, Graph-based algorithms for Boolean function manipulation, IEEE Trans. on Computers, C-35, 677, 10.1109/TC.1986.1676819 Büchi, 1960, On a decision method in restricted second order arithmetic, 1 Chou, 1996, Verifying a model-checking algorithm, vol. 1055, 241 Choueka, 1974, Theories of automata on ω-tapes: a simplified approach, Journal of Computer and System Science, 8, 117, 10.1016/S0022-0000(74)80051-6 Clarke, 1982, Synthesis of synchronization skeletons for branching time temporal logic, vol. 131 Clarke, 1994, Model checking and abstraction, ACM-TOPLAS, 16, 1512, 10.1145/186025.186051 Clarke, 1999 Courcoubetis, 1990, Memory efficient algorithms for the verification of temporal properties Dillinger, 2004, Fast and accurate bitstate verification for SPIN, vol. 2989 Emerson, 1997, Combining partial order reduction and symmetry reduction, vol. 1217, 19 Etessami K., “Stutter-invariant languages, ω-automata, and temporal logic”, in: Proc. Conf. on Computer Aided Verification, CAV, 1999, pp. 236–248 Etessami, 2000, Optimizing Büchi automata, vol. 1877, 153 Gerth, 1995, Simple on-the-fly automatic verification of linear temporal logic, 3 Godefroid P., Holzmann G.J., “On the verification of temporal properties”, in: Proc. Internat. Conf. on Protocol Specification, Testing, and Verification, Liege, Belgium, May 1993, pp. 109–124 Hajek J., “Automatically verified data transfer protocols”, in: Proc. 4th ICCC, Kyoto, 1978, pp. 749–756 Holzmann G.J., “PAN: a protocol specification analyzer”, Technical Report TM81-11271-5, AT&T Bell Laboratories, March 1981 Holzmann, 1982, A theory for protocol validation, IEEE Trans. on Computers, C-31, 730, 10.1109/TC.1982.1676079 Holzmann, 1988, An improved protocol reachability analysis technique, Software, Practice and Experience, 18, 137, 10.1002/spe.4380180203 Holzmann G.J., Patti J., “Validating SDL specifications: an experiment”, in: Proc. Internat Conf. on Protocol Specification, Testing, and Verification, Twente, Netherlands, June 1989, pp. 317–326 Holzmann, 1990, Spin—A protocol analyzer, 423 Holzmann, 1991 Holzmann G.J., Peled D., “An improvement in formal verification”, in: Proc. Conf. on Formal Description Techniques, FORTE, Bern, Switzerland, October 1994, pp. 177–194 Holzmann, 1996, On nested depth-first search, vol. 32 Holzmann, 1997, The model checker Spin, IEEE Trans. on Software Engineering, 23, 279, 10.1109/32.588521 Holzmann, 1998, An analysis of bitstate hashing, Formal Methods in System Design, 13, 287, 10.1023/A:1008696026254 Holzmann, 1998, Designing executable abstractions Holzmann, 1999, A practical method for the verification of event driven systems, 597 Holzmann, 1999, Software model checking—extracting verification models from source code, 481 Holzmann, 1999, A minimized automaton representation of reachable states, Software Tools for Technology Transfer, 2, 270, 10.1007/s100090050034 Holzmann, 2004 Holzmann, 2004, Model-driven software verification, vol. 2989, 77 Kurshan, 1995, Homomorphic reduction of coordination analysis, vol. 73, 105 Manna Z., Pnueli A., “Tools and rules for the practicing verifier”, Stanford University, Report STAN-CS-90-1321, July 1990, 34 p Manna, 1991 McMillan, 1993 Moore, 1965, Cramming more components onto integrated circuits, Electronics, 19 Peled, 1994, On projective and separable properties, vol. 787, 291 Pnueli A., “The temporal logic of programs”, in: Proc. 18th IEEE Symposium on Foundations of Computer Science, 1977, Providence, RI, pp. 46–57 Queille J.P., Sifakis J., “Specification and verification of concurrent systems in Cesar”, in: Proc. of Fifth Internat. Symp. on Programming, 1981, pp. 337–350 Schneider, 1998, Validating requirements for fault tolerant systems using model checking, 4 Tanenbaum, 1981 Tarjan, 1972, Depth first search and linear graph algorithms, SIAM J. Computing, 1, 146, 10.1137/0201010 LATA Switching Systems Generic Requirements (LSSGR), FR-NWT-000064, 1992 edition. Feature requirements, including: SPCS Capabilities and Features, SR-504, Issue 1, March 1996. Telcordia/Bellcore Thomas, 1990, Automata on infinite objects, vol. B, 133 Turing, 1936, On computable numbers, with an application to the Entscheidungsproblem, Proc. London Math. Soc. Ser. 2, 42, 230, 10.1112/plms/s2-42.1.230 Vardi M.Y., Wolper P., “An automata-theoretic approach to automatic program verification”, in: Proc. Symp. on Logic in Comput. Sci., Cambridge, June 1986, pp. 322–331 West, 1978, General technique for communications protocol validation, IBM J. Res. Develop., 22, 393, 10.1147/rd.224.0393 West, 1978, Automated validation of a communications protocol: the CCITT X. 21 recommendation, IBM J. Res. Develop., 22, 60, 10.1147/rd.221.0060 Wolper P., Vardi M.Y., Sistla A.P., “Reasoning about infinite computation paths”, in: Proc. 24th IEEE Symp. on Foundations of Comput. Sci., Tucson, 1983, pp. 185–194 Wolper, 1993, Reliable hashing without collision detection, vol. 697, 59