Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more

Abrial J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)

Barradas H.R., Bert D.: Specification and proof of liveness properties under fairness assumptions in B event systems. In: Butler, M.J., Petre, L., Sere, K. (eds) IFM, LNCS, vol. 2335, pp. 360–379. Springer, Berlin (2002)

Bellegarde, F., Darlot, C., Julliand, J., Kouchnarenko, O.: Reformulation: A way to combine dynamic properties and b refinement. In: Oliveira, J.N., Zave, P. (eds.) FME. Lecture Notes in Computer Science, vol. 2021, pp. 2–19. Springer, Berlin (2001)

Bert D., Potet M.-L., Stouls N.: Genesyst: a tool to reason about behavioral aspects of B event specifications. application to security properties. In: Treharne, H., King, S., Henson, M.C., Schneider, S.A. (eds) ZB 2005, LNCS, vol. 3455, pp. 299–318. Springer, Berlin (2005)

Bouquet F., Legeard B., Peureux F.: CLPS-B—a constraint solver for B. In: Katoen, J.-P., Stevens, P. (eds) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 2280, pp. 188–204. Springer, Berlin (2002)

Butler, M., Leuschel, M.: Combining CSP and B for specification and property verification. In: Proceedings of Formal Methods 2005, LNCS, vol. 3582, pp. 221–236, Newcastle upon Tyne. Springer, Berlin (2005)

Chaki S., Clarke E., Ouaknine J., Sharygina N., Sinha N.: Concurrent software verification with states, events, and deadlocks. Formal Aspects Comput V17(4), 461–483 (2005)

Chouali S., Julliand J., Masson P.-A., Bellegarde F.: Pltl-partitioned model checking for reactive systems under fairness assumptions. ACM Trans. Embedded Comput. Syst. 4(2), 267–301 (2005)

Clarke E.M., Grumberg O., Peled D.: Model Checking. MIT Press, Cambridge (1999)

Cui, B., Dong , Y., Du, X., Kumar, N., Ramakrishnan, C.R., Ramakrishnan, I.V., Roychoudhury, A., Smolka, S.A., Warren, D.S.: Logic programming and model checking. In: Palamidessi, C., Glaser, H., Meinke, K. (eds.) Proceedings of ALP/PLILP’98. LNCS, vol. 1490, pp 1–20. Springer, Berlin (1998)

Delzanno G., Podelski A.: Constraint-based deductive model checking. STTT 3(3), 250–270 (2001)

Derrick J., North S., Simons T.: Issues in implementing a model checker for Z. In: Liu, Z., He, J. (eds) ICFEM. LNCS, vol. 4260, pp. 678–696. Springer, Berlin (2006)

Derrick, J., Smith, G.: Linear temporal logic and Z refinement. In: Rattray, C., Maharaj, S., Shankland, C. (eds) AMAST 04. LNCS, vol. 3116, pp. 117 131. Springer (2004)

Dollé D., Essamé D., Falampin J.: B dans le tranport ferroviaire. L’expérience de Siemens Transportation Systems. Technique et Science Informatiques 22(1), 11–32 (2003)

Essamé, D., Dollé, D.: B in large-scale projects: The Canarsie line CBTC experience. In: Proceedings of the 7th International B Conference (B2007). LNCS, vol. 4355, pp. 252–254, Besancon, France. Springer-Verlag, Berlin (2007)

Farwer, B., Leuschel, M.: Model checking object Petri nets in Prolog. In: Proceedings PPDP ’04, pp. 20–31. ACM Press, New York (2004)

Ferreira, C., Butler, M.: A process compensation language. In: Santen, T., Stoddart, B. (eds.) Proceedings Integrated Formal Methods (IFM 2000). LNCS, vol. 1945, pp. 424–435. Springer, Berlin (2000)

Formal Systems (Europe) Ltd. Failures-Divergence Refinement—FDR2 User Manual (version 2.8.2)

Groslambert, J.: A jag extension for verifying LTL properties on B event systems. In: Proceedings B’07, pp. 262–265 (2007)

Groslambert, J.: Verification of LTL on B event systems. In: Proceedings B’07, pp. 109–124 (2007)

Hall, A.: Using formal methods to develop an atc information system. IEEE Software, pp. 66–76, March 1996. Reprinted in Industrial-Strength Formal Methods in Practice, M.G. Hinchey & J.P. Bowen, Springer (1999)

Hallerstede, T.S.: Stefan Und Hoang. Qualitative Probabilistic Modelling in Event-B. In: Ifm’2007, LNCS, vol. 4591, pp. 49–63 (2007)

Hatcliff J., Dwyer M.B.: Using the bandera tool set to model-check properties of concurrent java software. In: Larsen, K.G., Nielsen, M. (eds) CONCUR. LNCS, vol. 2154, pp. 39–58. Springer, Berlin (2001)

Holzmann G.J.: The model checker Spin. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)

Ifill, W., Schneider, S.A., Treharne, H.: Augmenting B with control annotations. In: Proceedings B’07, pp. 34–48 (2007)

Ip, C.N., Dill, D.L.: Better verification through symmetry. In: Computer Hardware Description Languages and their Applications, pp. 97–111 (1993)

Laroussinie F., Schnoebelen P.: A hierarchy of temporal logics with past. Theor. Comput. Sci. 148(2), 303–324 (1995)

Leuschel, M.: The high road to formal validation:. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ. Lecture Notes in Computer Science, vol. 5238, pp. 4–23. Springer, Berlin

Leuschel M., Butler M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds) FME 2003: Formal Methods. LNCS, vol. 2805, pp. 855–874. Springer, Berlin (2003)

Leuschel, M., Butler, M., Spermann, C., Turner, E.: Symmetry reduction for B by permutation flooding. In: Proceedings B2007. LNCS, vol. 4355, pp. 79–93, Besancon, France. Springer, Berlin (2007)

Leuschel, M., Massart T.: Infinite state model checking by abstract interpretation and program specialisation. In: Bossi, A., (ed.) Proceedings LOPSTR’99. LNCS, vol. 1817, pp. 63–82, Venice, Italy (2000)

Leuschel, M., Massart, T.: Efficient approximate verification of B via symmetry markers. In: Proceedings International Symmetry Conference, pp. 71–85, Edinburgh, UK (2007)

Leuschel, M., Massart T., Currie, A.: How to make FDR spin: LTL model checking of CSP by refinement. In: Oliviera, J.N., Zave, P., (eds.) FME’2001. LNCS, vol. 2021, pp. 99–118, Berlin, Germany, March 2001. Springer, Berlin (2001)

Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proceedings POPL ’85, pp. 97–107. ACM Press, New York (1985)

Nilsson, U., Lübcke, J.: Constraint logic programming for local and symbolic model checking. In: Lloyd, J. (ed.) Proceedings of the International Conference on Computational Logic (CL’2000). LNAI, vol. 1861, pp. 384–398, London, UK. Springer, Berlin (2000)

Parreaux, B.: Vérification de systèmes d’événements B par model-checking PLTL. Thèse de Doctorat, LIFC, Université de Franche-Comté, 08 Décembre (2000)

Plagge, D., Leuschel, M.: Validating Z Specifications using the ProB Animator and Model Checker. In: Davies, J., Gibbons, J. (eds.) Proceedings IFM 2007. LNCS, vol. 4591, pp. 480–500. Springer, Berlin (2007)

Pokorny, R.L., Ramakrishnan, C.R.: Model checking linear temporal logic using tabled logic programming. In: Proceedings Tabling in Parsing and Deduction TAPD 2000, Vigo, Spain, September (2000)

Pouzancre G.: How to diagnose a modern car with a formal B model?. In: Bert, D., Bowen, J.P., King, S., Waldén, M.A. (eds) ZB’2003. LNCS, vol. 2651, pp. 98–100. Springer, Berlin (2003)

Ramakrishna, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Swift, T., Warren, D.S.: Efficient model checking using tabled resolution. In: Grumberg, O. (ed.) Proceedings CAV’97. LNCS, vol. 1254, pp. 143–154. Springer, Berlin (1997)

Roscoe A.W.: The Theory and Practice of Concurrency. Prentice-Hall, New Jersey (1999)

Roscoe A.W.: On the expressive power of CSP refinement. Formal Aspects Comput. 17(2), 93–112 (2005)

Sagonas, K., Swift, T., Warren, D.S.: XSB as an efficient deductive database engine. In: Proceedings of the ACM SIGMOD International Conference on the Management of Data, pp. 442–453, Minneapolis, Minnesota. ACM, New York (1994)

Schneider S.: Concurrent and Real-time Systems: The CSP Approach. Wiley, New York (1999)

Sistla A.P., Gyuris V., Emerson E.A.: Smc: a symmetry-based model checker for verification of safety and liveness properties. ACM Trans. Softw. Eng. Methodol. 9(2), 133–166 (2000)

Tarjan R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972)

Treharne H., Schneider S.: How to drive a B machine. In: Bowen, J.P., Dunne, S., Galloway, A., King, S. (eds) ZB’2000. LNCS, vol. 1878, pp. 188–208. Springer, Berlin (2000)

Turner, E., Leuschel, M., Spermann, C., Butler, M.: Symmetry reduced model checking for B. In: Proceedings Symposium TASE 2007, pp. 25–34, Shanghai, China. IEEE (2007)

Vardi M.Y.: Branching vs. linear time: final showdown. In: Margaria, T., Yi, W. (eds) TACAS’01, LNCS, vol. 2031, pp. 1–22. Springer, Berlin (2001)

Wachter B.D., Genon A., Massart T., Meuter C.: The formal design of distributed controllers with dsl and Spin. Formal Aspects Comput. 17(2), 177–200 (2005)