FAST: Tăng tốc từ lý thuyết đến thực tiễn

Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(1), 3–34 (1995) Annichini, A., Asarin, E., Bouajjani, A.: Symbolic techniques for parametric reasoning about counter and clock systems. In: Proceedings of the 12th International Conference on Computer Aided Verification (CAV’2000), Chicago, July 2000. Lecture Notes in Computer Science, vol. 1855, pp. 419–434. Springer, Heidelberg (2000) Annichini, A., Bouajjani, A., Sighireanu, M.: TReX: a tool for reachability analysis of complex systems. In: Proceegings of the 13th International Conference on Computer Aided Verification (CAV’2001), Paris, July 2001. Lecture Notes in Computer Science, vol. 2102, pp. 368–372. Springer, Heidelberg (2001) Bardin, S., Finkel, A., Leroux, J.: FASTer acceleration of counter automata. In: Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’2004). Barcelona, March 2004. Lecture Notes in Computer Science, vol. 2988, pp. 576–590. Springer, Heidelberg (2004) Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: fast acceleration of symbolic transition systems. In: Proceedings of the 15th International Conference on Computer Aided Verification (CAV’2003), Boulder, July 2003. Lecture Notes in Computer Science, vol. 2725, pp. 118–121. Springer, Heidelberg (2003) Bardin, S., Finkel, A., Leroux, J., Petrucci, L., Worobel, L.: FAST user manual. 33 pp. http://www.lsv.ens-cachan.fr/fast/ (2003) Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: Proceedings of the 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA’2005), Taipei, October 2005. Lecture Notes in Computer Science, vol. 3707, pp. 474–488. Springer, Heidelberg (2005) Bardin, S., Leroux, J., Point, G.: FAST Extended Release. In: Proceedings of the 18th International Conference on Computer Aided Verification (CAV’2006), Seattle, August 2006. Lecture Notes in Computer Science, vol. 4144, pp. 63–66. Springer, Heidelberg (2006) Bardin, S., Petrucci, L.: From pnml to counter systems for accelerating Petri nets with fast. In: Proceedings of the Workshop on Interchange Formats for Petri Nets (at ICATPN 2004), pp. 26–40 (2004) Bartzis, C., Bultan, T.: Efficient symbolic representations for arithmetic constraints in verification. Int. J. Found. Comput. Sci. 14(4), 605–624 (2003) Bartzis, C., Bultan, T.: Widening arithmetic automata. In: Proceedings of the 16th International Conference on Computer Aided Verification (CAV 2004), Boston, July 2004. Lecture Notes in Computer Science, vol. 3114, pp. 321–333. Springer, Heidelberg (2004) Bérard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, Ph.: Systems and Software Verification. Model-Checking Techniques and Tools. Springer, Heidelberg (2001) Bérard, B., Fribourg, L.: Reachability analysis of (timed) Petri nets using real arithmetic. In: Proceedings of the 10th International Conference on Concurrency Theory (CONCUR’99), Eindhoven, August 1999. Lecture Notes in Computer Science, vol. 1664, pp. 178–193 Springer, Heidelberg (1999) Berman, L.: Precise bounds for Presburger arithmetic and the reals with addition: preliminary report. In: Proceedings of the 18th IEEE Symposium Foundations of Computer Science (FOCS’77), Providence, October–November 1977, pp. 95–99. IEEE, Washington (1977) Billington, J., Christensen, S., van Hee, K., Kindler, E., Kummer, O., Petrucci, L., Post, R., Stehno, C., Weber, M.: The Petri Net Markup Language: Concepts, technology and tools. In: Proceedings of the 24th International Conference on Application and Theory of Petri Nets (ICATPN’2003), Eindhoven, June 2003. Lecture Notes in Computer Science, vol. 2679, pp. 483–505. Springer, Heidelberg (2003) Billington, J., Gallasch, G.E., Petrucci, L.: FAST verification of the class of stop-and-wait protocols modelled by coloured Petri nets. Nord. J. Comput. 12(3), 251–274 (2005) Billington, J., Gallasch, G.E., Petrucci, L.: Transforming couloured Petri nets to counter systems for parametric verification: A stop-and-wait protocol case study. In: Proceedings of the 2nd workshop on MOdel-based Methodologies for Pervasive and Embedded Software (MOMPES’05, satellite of ACSD’05), Rennes, vol. 39, pp. 37–55. TUCS general publication (2005) Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, Université de Liège (1998) Boigelot, B.: On iterating linear transformations over recognizable sets of integers. Theor. Comput. Sci. 309(2), 413–468 (2003) Boigelot, B., Wolper, P.: Symbolic verification with periodic sets. In: Proceedings of the 6th International Conference on Computer Aided Verification (CAV’94), Stanford, June 1994. Lecture Notes in Computer Science, vol. 818, pp. 55–67. Springer, Heidelberg (1994) Bouajjani, A., Merceron, A.: Parametric verification of a group membership algorithm. In: Proceedings of the 7th International Symposium Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT’2002), Oldenburg, September 2002. Lecture Notes in Computer Science, vol. 2469, pp. 311–330. Springer, Heidelberg (2002) Boudet, A., Comon, H.: Diophantine equations, Presburger arithmetic and finite automata. In: Proceedings of the 21st International Conference on Trees in Algebra and Programming (CAAP’96), Linköping, April 1996. Lecture Notes in Computer Science, vol. 1059, pp. 30–43. Springer, Heidelberg (1996) Bruyère, V., Hansel, G., Michaux, C., Villemaire, R.: Logic and p-recognizable sets of integers. Bull. Belg. Math. Soc. 1(2), 191–238 (1994) Bultan, T., Yavuz-Kahveci, T.: Action language verifier. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE 2001), Coronado Island, 26–29 November 2001, pp. 382–386. IEEE Computer Society, Washington (2001) Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Camberidge (1999) Comon, H., Jurski, Y.: Multiple counters automata, safety analysis, and Presburger arithmetic. In: Proceedings of the 10th International Conference on Computer Aided Verification (CAV’98), Vancouver, June–July 1998. Lecture Notes in Computer Science, vol. 1427, pp. 268–279. Springer, Heidelberg (1998) Couvreur, J.-M.: A bdd-like implementation of an automata package. In: Proceedings of the 9th International Conference on Implementation and Application of Automata (CIAA’2004), Kingston, July 2004. Lecture Notes in Computer Science, vol. 3317, pp. 310–311. Springer, Heidelberg (2004) Darlot, Ch., Finkel, A., Van Begin, L.: About Fast and TReX accelerations. In: Proceedings of the 4th International Workshop on Automated Verification of Critical Systems (AVoCS’04), August–September 2004. Electronic Notes in Theoretical Computer Science, London, vol. 128. Elsevier Science Publishers, London Delzanno, G., Raskin, J.-F., Van Begin, L.: Covering sharing trees: a compact data structure for parameterized verification. J. Softw. Tools Technol. Transf. 5(2–3), 268–297 (2004) Dufourd, C., Finkel, A., Schnoebelen, P.: Reset nets between decidability and undecidability. In: Proceedings of the 25th International Conference Automata, Languages, and Programming (ICALP’98), Aalborg, July 1998. Lecture Notes in Computer Science, vol. 1443, pp. 103–115. Springer, Heidelberg (1998) Emerson, E.A., Namjoshi, K.S.: On model checking for non-deterministic infinite-state systems. In: Proceedings of the 13th IEEE Symposium Logic in Computer Science (LICS’98), Indianapolis, June 1998, pp. 70–80. IEEE Computer Socicty Press, Washington (1998) Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: Proceedings of 14th IEEE Symposium on Logic in Computer Science (LICS’99), Trento, July 1999, pp. 352–359. IEEE Computer Society Press, Washington (1999) Fast homepage. http://www.lsv.ens-cachan.fr/fast/ Finkel, A.: A generalization of the procedure of karp and miller to well structured transition systems. In: Proceedings of the 14th International Conference on Automata, Languages, and Programming (ICALP’87), Karlsruhe, July 1987. Lecture Notes in Computer Science, vol. 267, pp. 499–508. Springer, Heidelberg (1987) Finkel, A., Leroux, J.: How to compose Presburger-accelerations: Applications to broadcast protocols. In: Proceedings of the 22nd Conference on Foundation of Software Technology and Theoretical Computer Science (FST&TCS’2002), Kanpur, December 2002. Lecture Notes in Computer Science, vol. 2556, pp. 145–156. Springer, Heidelberg (2002) Finkel, A., Purushothaman Iyer, S., Sutre, G.: Well-abstracted transition systems: application to FIFO automata. Info. Comput. 181(1), 1–31 (2003) Finkel, A., Sutre, G.: Decidability of reachability problems for classes of two counters automata. In: Proceedings of the 17th Annual Symposium Theoretical Aspects of Computer Science (STACS’2000), Lille, February 2000. Lecture Notes in Computer Science, vol. 1770, pp. 346–357. Springer, Heidelberg (2000) Fribourg, L.: Petri nets, flat languages and linear arithmetic. Invited lecture. In: Alpuente, M. (ed) Proceedings of the 9th International Workshop on Functional and Logic Programming (WFLP’2000), Benicassim, September 2000, pp. 344–365, Proceedings published as Ref. 2000.2039, Universidad Politécnica de Valencia, Spain (2000) Fribourg, L., Olsén, H.: A decompositional approach for computing least fixed-points of Datalog programs with Z-counters. Constraints 2(3/4), 305–335 (1997) Fribourg, L., Olsén, H.: Proving safety properties of infinite state systems by compilation into Presburger arithmetic. In: Proceedings of the 8th International Conference on Concurrency Theory (CONCUR’97), Warsaw, July 1997, Lecture Notes in Computer Science, vol. 1243, pp. 213–227. Springer, Heidelberg (1997) Ganesh, V., Berezin, S., Dill, D.L.: Deciding presburger arithmetic by model checking and comparisons with other methods. In: Proceedings of the 4th International Conference on Formal Methods in Computer Aided Design (FMCAD’02), Portland, November 2002. Lecture Notes in Computer Science, vol. 2517, pp. 171–186. Springer, Heidelberg (2002) Geeraerts, G., Raskin, J.-F., Van Begin, L.: Expand, enlarge and check... made efficient. In: Rajjamani, S.K., Etessami, K. (eds.), Proceedings of 17th International Conference on Computer Aided Verification – (CAV 2005). Lecture Notes in Computer Science, vol. 3576, pp. 394–404. Springer, Heidelberg (2005) Ginsburg, S., Spanier, E.H.: Semigroups, Presburger formulas and languages. Pac. J. Math. 16(2), 285–296 (1966) Ibarra, O.H.: Reversal-bounded multicounter machines and their decision problems. J. ACM 25, 116–133 (1978) Ibarra, O.H., Su, J., Dang, Z., Bultan, T., Kemmerer, R.A.: Counter machines and verification problems. Theor. Comput. Sci. 289(1), 165–189 (2002) Jensen, K.: Coloured Petri Nets: Basic concepts, analysis methods and practical use. volume 1: basic concepts. In: Monographs in Theoretical Computer Science. Springer, Heidelberg (1992) Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147–195 (1969) Kelly, W., Pugh, W., Rosser, E., Shpeisman, T.: Transitive closure of infinite graphs and its applications. In: Proceedings of the 8th International Workshop Languages and Compilers for Parallel Computing (LCPC’95), Columbus, August 1995. Lecture Notes in Computer Science, vol. 1033, pp. 126–140. Springer, Heidelberg (1995) Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. Theor. Comput. Sci. 256(1–2), 93–112 (2001) Klaedtke, F.: On the automata size for presburger arithmetic. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS’04), Turku, July 2004, pp. 110–119. IEEE Computer Socicty Press, Washinston (2004) Klarlund, N., Møller, A., Schwartzbach, M.I.: MONA implementation secrets. Int. J. of Found. Comput. Sci. 13(4), 571–586 (2002) Kopetz, H., Grünsteidl, G.: A time trigerred protocol for fault- tolerant real-time systems. In: IEEE computer, Washington pp. 14–23 (1999) Lash homepage. http://www.montefiore.ulg.ac.be/~boigelot/research/lash/ Leroux, J., Sutre, G.: On flatness for 2-dimensional vector addition systems with states. In: Proceedings of the 15th International Conference on Concurrency Theory (CONCUR’04), London, Ausust–September 2004. Lecture Notes in Computer Science, vol. 3170, pp. 402–416. Springer, Heidelberg (2004) Leroux, J., Sutre, G.: Flat counter automata almost everywhere! In: Proceedings of the 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA’2005), Taipei, October 2005. Lecture Notes in Computer Science, vol. 3707, pp. 489–503. Springer, Heidelberg (2005) Liu, L., Billington, J.: Tackling the infinite state space of a multimedia control protocol service specification. In: Proceedings of the 23rd International Conference on Application and Theory of Petri Nets (ICATPN’2002), Adelaide, June 2002. Lecture Notes in Computer Science, vol. 2360, pp. 273–293. Springer, Heidelberg (2002) Mandel, A., Simon, I.: On finite semigroups of matrices. Theor. Comput. Sci. 5(2), 101–111 (1977) Mayr, E.W.: Persitence of Vector Replacement Systems is decidable. Acta Inform. 15, 309–318 (1981) Mona homepage. http://www.brics.dk/mona/index.html Omega homepage. http://www.cs.umd.edu/projects/omega/ Presburger, M.: Uber die volstandigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchem die addition als einzige operation hervortritt. In: C. R. 1er congrès des Mathématiciens des pays slaves, Varsovie, pp. 92–101 (1929) Rybina, T., Voronkov, A.: Brain: backward reachability analysis with integers. In: Proceedings of the 9th International Conference on Algebraic Methodology and Software Technology (AMAST’2002), Saint-Gilles-les-Bains, Reunion Island, September 2002. Lecture Notes in Computer Science, vol. 2422, pp. 489–494. Springer, Heidelberg (2002) Wolper, P., Boigelot, B.: An automata-theoretic approach to Presburger arithmetic constraints. In: Proceedings of the 2nd International Symposicm Static Analysis (SAS’95), Glasgow, September 1995. Lecture Notes in Computer Science, vol. 983, pp. 21–32. Springer, Heidelberg (1995) Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Proceedings of the 10th International Conference on Computer Aided Verification (CAV’98), Vancouver, June–July 1998. Lecture Notes in Computer Science, vol. 1427, pp. 88–97. Springer, Heidelberg (1998) Wolper, P., Boigelot, B.: On the construction of automata from linear arithmetic constraints. In: Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’2000), Berlin, March–April 2000. Lecture Notes in Computer Science, vol. 1785, pp. 1–19. Springer, Heidelberg (2000) Yavuz-Kahveci, T., Bartzis, C., Bultan, T.: Action language verifier, extended. In: Proceedings of the 17th International Conference on Computer Aided Verification (CAV 2005), Edinburgh, 6–10 July 2005. Lecture Notes in Computer Science, vol. 3576, pp. 413–417. Springer, Heidelberg (2005)