nach oben

International Journal on Software Tools for Technology Transfer

Erschienen in:

09.11.2017 | Introduction

Recent advances in interactive and automated analysis

verfasst von: Radu Mateescu

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 2/2018

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Computers and distributed software applications are becoming nowadays ubiquitous, and therefore their safety and reliability have increasingly important societal impact. In this context, formal methods equipped with powerful and versatile analysis tools are more important than ever in the design process. Despite the relevant scientific results and well-established tools obtained in recent years, there is a constant need of enhancing the analysis capabilities in order to handle increasingly complex systems. We briefly discuss some recent advances in the field, introducing five papers selected from the 22th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016).

Nächster Artikel Coqoon

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Giunchiglia, F., Traverso, P.: Theorem proving in technology transfer: the user’s point of view. Int. J. Softw. Tools Technol. Transf. 3(1), 1–12 (2000)CrossRefMATH

Aspinall, D.: Proof general: a generic tool for proof development. In: Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS’00). Lecture Notes in Computer Science, vol. 1785, pp. 38–42. Springer, Berlin (2000)

Aspinall, D., Denney, E., Lüth, C.: A tactic language for hiproofs. In: Proceedings of the 9th International Conference on Intelligent Computer Mathematics (AISC’08). Lecture Notes in Computer Science, vol. 5144, pp. 339–354. Springer, Berlin (2008)

Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH

Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development—Coq’Art: The Calculus of Inductive Constructions. Springer, Berlin (2004)CrossRefMATH

Beyer, S., Jacobi, C., Kröning, D., Leinenbach, D., Paul, W.-J.: Putting it all together—formal verification of the VAMP. Int. J. Softw. Tools Technol. Transf. 8(4–5), 411–430 (2006)CrossRef

Blom, S., Orzan, S.: A distributed algorithm for strong bisimulation reduction of state spaces. Int. J. Softw. Tools Technol. Transf. 7(1), 74–86 (2005)CrossRefMATH

Blom, S., van de Pol, J.: Distributed branching bisimulation minimization by inductive signatures. In: Proceedings of the 8th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC’09). EPCTS vol. 14, pp. 32–46 (2009)

Boldo, S., Jourdan, J.-H., Leroy, X., Melquiond, G.: A formally-verified C compiler supporting floating-point arithmetic. In: Proceedings of the 21st IEEE Symposium on Computer Arithmetic (ARITH’13), pp. 107–115. IEEE (2013)

10.

Brucker, A.D., Wolff, B.: A verification approach to applied system security. Int. J. Softw. Tools Technol. Transf. 7(3), 233–247 (2005)CrossRef

11.

Chechik, M., Raskin J.-F. (eds.): Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’16). Lecture Notes in Computer Science, vol. 9636. Springer, Berlin (2016)

12.

Cleaveland, R., Sokolsky, O.: Equivalence and preorder checking for finite-state systems. In: Bergstra, J.A., Ponse, A., Smolka S.A. (eds.) Handbook of Process Algebra, pp. 391–424. Elsevier, Amsterdam (2001)

13.

Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: Proceedings of the 29th International Conference on Computer Aided Verification (CAV’17). Lecture Notes in Computer Science, vol. 10427, pp. 592–600. Springer, Berlin (2017)

14.

Delahaye, D.: A tactic language for the system Coq. In: Proceedings of the 7th International Conference on Logic for Programming and Automated Reasoning (LPAR’00), Lecture Notes in Computer Science, vol. 1955, pp. 85–95. Springer, Berlin (2000)

15.

Faithfull, A., Bengtson, J., Tassi, E., Tankink, C.: Coqoon—an IDE for interactive proof development in Coq. In: Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’16). Lecture Notes in Computer Science, vol. 9636, pp. 316–331. Springer, Berlin (2016)

16.

Faithfull, A., Bengtson, J., Tassi, E., Tankink, C.: Coqoon—an IDE for interactive proof development in Coq. Int. J. Softw. Tools Technol. Transf. (2017). https://doi.org/10.1007/s10009-017-0457-2

17.

Ferreira, J.-F., Gherghina, C., He, G., Qin, S., Chin, W.-N.: Automated verification of the freeRTOS scheduler in Hip/Sleek. Int. J. Softw. Tools Technol. Transf. 16(4), 381–397 (2014)CrossRef

18.

Garavel, H., Mateescu, M., Serwe, W.: Large-scale distributed verification using CADP: beyond clusters to grids. In: Proceedings of the 11th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC’12). ENTCS, vol. 296, pp. 145–161. Elsevier (2013)

19.

Garavel, H., Mateescu, R., Smarandache, I.: Parallel state space construction for model-checking. In: Proceedings of the 8th International SPIN Workshop on Model Checking of Software (SPIN’01). Lecture Notes in Computer Science, vol. 2057, pp. 217–234. Springer, Berlin (2001)

20.

Gonthier, G.: The four colour theorem: engineering of a formal proof. In: Proceedings of the 8th Asian Symposium on Computer Mathematics (ASCM’07). Lecture Notes in Computer Science, vol. 5081, pp. 333. Springer, Berlin (2007)

21.

Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Le Roux, S., Mahboubi, A., O’Connor, R., Biha, S.-O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Théry, L.: A machine-checked proof of the odd order theorem. In: Proceedings of the 4th International Conference on Interactive Theorem Proving (ITP’13). Lecture Notes in Computer Science, vol. 7998, pp. 163–179. Springer, Berlin (2013)

22.

Grov, G., Lin, Y.: The Tinker tool for graphical tactic development. Int. J. Softw. Tools Technol. Transf. (2017). https://doi.org/10.1007/s10009-017-0452-7

23.

Holzmann, G.J.: Parallelizing the SPIN model checker. In: Proceedings of the 19th International Workshop on Model Checking Software (SPIN’12). Lecture Notes in Computer Science, vol. 7385, pp. 155–171. Springer, Berlin (2012)

24.

Holzmann, G.J., Bosnacki, D.: The design of a multicore extension of the SPIN model checker. IEEE Trans. Softw. Eng. 33(10), 659–674 (2007)CrossRef

25.

Klein, J., Baier, C., Chrszon, P., Daum, M., Dubslaff, C., Klüppelholz, S., Märcker, S., Müller, D.: Advances in symbolic probabilistic model checking with PRISM. In: Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’16). Lecture Notes in Computer Science, vol. 9636, pp. 349–366. Springer, Berlin (2016)

26.

Klein, J., Baier, C., Chrszon, P., Daum, M., Dubslaff, C., Klüppelholz, S., Märcker, S., Müller, D.: Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata. Int. J. Softw. Tools Technol. Transf. (2017). https://doi.org/10.1007/s10009-017-0456-3

27.

Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Proceedings of the 23rd International Conference on Computer Aided Verification (CAV’11). Lecture Notes in Computer Science, vol. 6806, pp. 585–591. Springer, Berlin (2011)

28.

Kwiatkowska, M., Parker, D., Wiltsche, C.: PRISM-games 2.0: a tool for multi-objective strategy synthesis for stochastic games. In: Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’16). Lecture Notes in Computer Science, vol. 9636, pp. 560–566. Springer, Berlin (2016)

29.

Kwiatkowska, M., Parker, D., Wiltsche, C.: PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives. Int. J. Softw. Tools Technol. Transf. (2017). https://doi.org/10.1007/s10009-017-0476-z

30.

Li, W., Paulson, L.-C.: A formal proof of Cauchy’s residue theorem. In: Proceedings of the 7th International Conference on Interactive Theorem Proving (ITP’16). Lecture Notes in Computer Science, vol. 9807, pp. 235–251. Springer, Berlin (2016)

31.

Lin, Y., Le Bras, P., Grov, G.: Developing and debugging proof strategies by tinkering. In: Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’16). Lecture Notes in Computer Science, vol. 9636, pp. 573–579. Springer, Berlin (2016)

32.

Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer, Berlin (2002)MATH

33.

Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Proceedings of the 11th International Conference on Automated Deduction (CADE’92). Lecture Notes in Computer Science, vol. 607, pp. 748–752. Springer, Berlin (1992)

34.

Rajasekaran, S., Lee, I.: Parallel algorithms for relational coarsest partition problems. IEEE Trans. Parallel Distrib. Syst. 9(7), 687–699 (1998)CrossRef

35.

Renault, E., Duret-Lutz, A., Kordon, K., Poitrenaud, D.: Parallel explicit model checking for generalized Büchi automata. In: Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’15). Lecture Notes in Computer Science, vol. 9035, pp. 613–627. Springer, Berlin (2015)

36.

Stern, U., Dill, D.L.: Parallelizing the Murphi verifier. Form. Methods Syst. Des. 18(2), 117–129 (2001)CrossRefMATH

37.

van Dijk, T., van de Pol, J.: Sylvan: multi-core decision diagrams. In: Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’15). Lecture Notes in Computer Science, vol. 9035, pp. 677–691. Springer, Berlin (2015)

38.

van Dijk, T., van de Pol, J.: Multi-core symbolic bisimulation minimisation. In: Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’16). Lecture Notes in Computer Science, vol. 9636, pp. 332–348. Springer, Berlin (2016)

39.

van Dijk, T., van de Pol, J.: Multi-core symbolic bisimulation minimisation. Int. J. Softw. Tools Technol. Transf. (2017). https://doi.org/10.1007/s10009-017-0468-z

40.

Wijs, A.: Towards informed swarm verification. In: Proceedings of the 3rd International Symposium on NASA Formal Methods (NFM’11). Lecture Notes in Computer Science, vol. 6617, pp. 422–437. Springer, Berlin (2011)

Titel: Recent advances in interactive and automated analysis
verfasst von: Radu Mateescu
Publikationsdatum: 09.11.2017
Verlag: Springer Berlin Heidelberg
Erschienen in: International Journal on Software Tools for Technology Transfer / Ausgabe 2/2018
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-017-0477-y

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Weitere Artikel der Ausgabe 2/2018

Coqoon

The Tinker tool for graphical tactic development

Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata

Multi-core symbolic bisimulation minimisation

Automated translation of VDM to JML-annotated Java

PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives