nach oben

International Journal on Software Tools for Technology Transfer

Erschienen in:

31.05.2021 | Competitions and Challenges

SL-COMP: competition of solvers for separation logic

Report on the Third Edition

verfasst von: Mihaela Sighireanu

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 6/2021

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

SL-COMP is a competition bringing together researchers and users interested in automated reasoning methods for separation logic (SL). The competition provides a snapshot of the state of the art in the area through a set of problems that put forward the strengths and challenges of the existing solvers and a comparative and replicable evaluation of participating solvers. The third edition of SL-COMP took place in April 2019, as part of the TOOLympics event at TACAS 2019. It collected more than 1K satisfiability and entailment problems, had seen the adoption of the new input format based on SMT-LIB and had doubled the number of participant solvers compared with the first edition in 2014. This report relates the history and the context of SL-COMP competition and accounts of its third edition. It also discusses the issues related with its organization and the challenges for the next editions.

Vorheriger Artikel VerifyThis 2019: a program verification competition

Nächster Artikel CoCo 2019: report on the eighth confluence competition

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

O’Hearn, P.: Separation logic. Commun. ACM 62(2), 86–95 (2019). https://doi.org/10.1145/3211968CrossRef

O’Hearn, P.: Separation logic. http://www0.cs.ucl.ac.uk/staff/p.ohearn/SeparationLogic/Separation_Logic/SL_Home.html

StarExec: http://www.starexec.org

Sighireanu, M., Cok, D.: Report on SL-COMP’14. JSAT 9, 173–186 (2014). https://doi.org/10.3233/SAT190107CrossRef

Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.): Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, LNCS, vol. 11429. Springer (2019). https://doi.org/10.1007/978-3-030-17502-3

SmallFoot: http://www0.cs.ucl.ac.uk/staff/p.ohearn/smallfoot/

Chin, W.N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program. 77(9), 1006–1036 (2012). https://doi.org/10.1016/j.scico.2010.07.004CrossRefMATH

Jacobs, B., Smans, J., Piessens, F.: A quick tour of the VeriFast program verifier. In: APLAS, LNCS, vol. 6461, pp. 304–311. Springer (2010). https://doi.org/10.1007/978-3-642-17164-2_21

SL-COMP’2018: https://www.irif.fr/~sighirea/sl-comp/18/

10.

Sighireanu, M., Pérez, J.A.N., Rybalchenko, A., Gorogiannis, N., Iosif, R., Reynolds, A., Serban, C., Katelaan, J., Matheja, C., Noll, T., Zuleger, F., Chin, W., Le, Q.L., Ta, Q., Le, T., Nguyen, T., Khoo, S., Cyprian, M., Rogalewicz, A., Vojnar, T., Enea, C., Lengál, O., Gao, C., Wu, Z.: SL-COMP: competition of solvers for separation logic. In: Beyer et al. [5], pp. 116–132. https://doi.org/10.1007/978-3-030-17502-3_8

11.

SL-COMP website. https://sl-comp.github.io/

12.

SL-COMP repository. https://github.com/sl-comp

13.

Iosif, R., Serban, C., Reynolds, A., Sighireanu, M.: Encoding separation logic in SMT-LIB v2.5 (2018). https://doi.org/10.1145/32119680

14.

Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Tech. rep., Department of Computer Science, The University of Iowa (2017). https://doi.org/10.1145/32119681

15.

Antonopoulos, T., Gorogiannis, N., Haase, C., Kanovich, M.I., Ouaknine, J.: Foundations for decision problems in separation logic with general inductive predicates. In: FOSSACS, LNCS, vol. 8412, pp. 411–425. Springer (2014). https://doi.org/10.1007/978-3-642-54830-7_27

16.

Demri, S., Deters, M.: Separation logics and modalities: a survey. J. Appl. Non Class. Log. 25(1), 50–99 (2015). https://doi.org/10.1145/32119682MathSciNetCrossRefMATH

17.

Iosif, R., Rogalewicz, A., Simácek, J.: The tree width of separation logic with recursive definitions. In: CADE, LNCS, vol. 7898, pp. 21–38. Springer (2013). https://doi.org/10.1007/978-3-642-38574-2_2

18.

Enea, C., Sighireanu, M., Wu, Z.: On automated lemma generation for separation logic with inductive definitions. In: ATVA, LNCS, vol. 9364, pp. 80–96. Springer (2015). https://doi.org/10.1007/978-3-319-24953-7_7

19.

Pérez, J.A.N., Rybalchenko, A.: Separation logic modulo theories. In: APLAS, LNCS, vol. 8301, pp. 90–106. Springer (2013). https://doi.org/10.1007/978-3-319-03542-0_7

20.

Gu, X., Chen, T., Wu, Z.: A complete decision procedure for linearly compositional separation logic with data constraints. In: IJCAR, LNCS, vol. 9706, pp. 532–549. Springer (2016). https://doi.org/10.1007/978-3-319-40229-1_36

21.

Brotherston, J., Gorogiannis, N., Petersen, R.L.: A generic cyclic theorem prover. In: APLAS, LNCS, vol. 7705, pp. 350–367. Springer (2012). https://doi.org/10.1007/978-3-642-35182-2_25

22.

Reynolds, A., Iosif, R., Serban, C., King, T.: A decision procedure for separation logic in SMT. In: ATVA, pp. 244–261 (2016). https://doi.org/10.1007/978-3-319-46520-3_16

23.

Katelaan, J., Matheja, C., Noll, T., Zuleger, F.: Harrsh: A tool for unified reasoning about symbolic-heap separation logic. In: LPAR-22, Kalpa Publications in Computing, vol. 9, pp. 23–36. EasyChair (2018). https://doi.org/10.29007/qwd8

24.

S2S: https://doi.org/10.1145/32119683

25.

Iosif, R., Rogalewicz, A., Vojnar, T.: Deciding entailments in inductive separation logic with tree automata. In: ATVA, LNCS, vol. 8837, pp. 201–218. Springer (2014). https://doi.org/10.1007/978-3-319-11936-6_15

26.

Brotherston, J., Fuhs, C., Pérez, J.A.N., Gorogiannis, N.: A decision procedure for satisfiability in separation logic with inductive predicates. In: CSL-LICS, pp. 25:1–25:10. ACM (2014). https://doi.org/10.1145/2603088.2603091

27.

Ta, Q.T., Le, T.C., Khoo, S.C., Chin, W.N.: Automated lemma synthesis in symbolic-heap separation logic. Proc. ACM Program. Lang. 2(POPL), 9:1-9:29 (2017). https://doi.org/10.1145/32119684CrossRef

28.

Enea, C., Lengál, O., Sighireanu, M., Vojnar, T.: Compositional entailment checking for a fragment of separation logic. In: APLAS, LNCS, vol. 8858, pp. 314–333. Springer (2014). https://doi.org/10.1007/978-3-319-12736-1_17

29.

Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Beyond reachability: shape abstraction in the presence of pointer arithmetic. In: SAS, LNCS, vol. 4134, pp. 182–203. Springer (2006). https://doi.org/10.1007/11823230_13

30.

Brotherston, J., Gorogiannis, N., Kanovich, M.: Biabduction (and related problems) in array separation logic. In: CADE, vol. 10395, pp. 472–490. Springer (2017). https://doi.org/10.1007/978-3-319-63046-5_29

31.

Kimura, D., Tatsuta, M.: Decidability for entailments of symbolic heaps with arrays. CoRR arXiv:1802.05935 (2018)

Titel: SL-COMP: competition of solvers for separation logic
Report on the Third Edition
verfasst von: Mihaela Sighireanu
Publikationsdatum: 31.05.2021
Verlag: Springer Berlin Heidelberg
Erschienen in: International Journal on Software Tools for Technology Transfer / Ausgabe 6/2021
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-021-00628-w

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 6/2021

CPA/Tiger-MGP: test-goal set partitioning for efficient multi-goal test-suite generation

Plain random test generation with PRTest

Study of the efficiency of model checking techniques using results of the MCC from 2015 To 2019

CoCo 2019: report on the eighth confluence competition

TOOLympics II: competitions on formal methods

KLEE symbolic execution engine in 2019