×

Assertion-based slicing and slice graphs. (English) Zbl 1259.68119


MSC:

68Q60 Specification and verification (program logics, model checking, etc.)

Software:

Spec#; JML; Boogie; KeY; ACSL
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Ahrendt W, Baar T, Beckert B, Bubel R, Giese M, Hähnle R, Menzel W, Mostowski W, Roth A, Schlager S, Schmitt PH (2005) The KeY tool. Softw System Model, 4(1): 32–54 · Zbl 02243139 · doi:10.1007/s10270-004-0058-x
[2] Burdy L, Cheon Y, Cok DR, Ernst MD, Kiniry JR, Leavens GT, Rustan K, Leino M, Poll E (2005) An overview of JML tools and applications. Int J Softw Tools Technol Transf 7(3): 212–232 · doi:10.1007/s10009-004-0167-4
[3] Barnett M, Evan Chang B-Y, DeLine R, Jacobs B, Rustan K, Leino M (2005) Boogie: a modular reusable verifier for object-oriented programs. In: de Boer FS, Bonsangue MM, Graf S, de Roever WP (eds) FMCO, Lecture Notes in Computer Science, vol 4111. Springer, Berlin, pp 364–387
[4] Baudin P, Cuoq P, Filliâtre J-C, Marché C, Monate B, Moy Y, Prevosto V (2010) ACSL: ANSI/ISO C Specification Language. CEA LIST and INRIA
[5] Barros J, da Cruz D, Henriques PR, Pinto JS (2010) Assertion-based slicing and slice graphs. In: Fiadeiro JL, Gnesi S (eds) Proceedings of the 8th IEEE international conference on software engineering and formal methods (SEFM’10). IEEE Computer Society, pp 93–102
[6] Barnett M, Rustan K, Leino M, Schulte W (2004) The Spec# programming system: an overview. In: CASSIS: construction and analysis of safe, secure, and interoperable smart devices, Lecture Notes in Computer Science, vol 3362. Springer, Berlin, pp 49–69
[7] Canfora G, Cimitile A, De Lucia A (1998) Conditioned program slicing. Inform Softw Technol 40(11–12): 595–608 (Special issue on program slicing) · doi:10.1016/S0950-5849(98)00086-X
[8] Comuzzi JJ, Hart JM (1996) Program slicing using weakest preconditions. In: FME ’96: Proceedings of the third international symposium of formal methods Europe on industrial benefit and advances in formal methods. Springer, London, pp 557–575
[9] Chung IS, Lee WK, Yoon GS, Kwon YR (2001) Program slicing based on specification. In: SAC ’01: Proceedings of the 2001 ACM symposium on applied computing. ACM New York, pp 605–609
[10] da Cruz D, Henriques PR, Pinto JS (2011) Verification graphs for programs with contracts (Submitted for publication)
[11] da Cruz D, Henriques PR, Pinto JS (2010) Gamaslicer: an online laboratory for program verification and analysis. In: LDTA ’10: Proceedings of the tenth workshop on language descriptions, tools and applications. ACM, New York, pp 1–8
[12] Dijkstra EW (1976) A discipline of programming. Prentice-Hall, Englewood Cliffs · Zbl 0368.68005
[13] Fox C, Danicic S, Harman M, Hierons RM (2001) Backward conditioning: a new program specialisation technique and its application to program comprehension. In: Proceedings of the 9th international workshop on program comprehension (IWPC’01). IEEE Computer Society, pp 89–97
[14] Frade MJ, Pinto JS (2011) Verification Conditions for source-level imperative programs. Comput Sci Rev 5: 252–277 · Zbl 1298.68171 · doi:10.1016/j.cosrev.2011.02.002
[15] Flanagan C, Saxe JB (2001) Avoiding exponential explosion: generating compact verification conditions. In: POPL ’01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on principles of programming languages. ACM, New York, pp 193–205 · Zbl 1323.68372
[16] Harman M, Hierons RM, Fox C, Danicic S, Howroyd J (2001) Pre/post conditioned slicing. In: Proceedings of the IEEE international conference on software maintenance (ICSM’01). IEEE Computer Society, pp 138–147
[17] Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM, 12: 576–580 · Zbl 0179.23105 · doi:10.1145/363235.363259
[18] Meyer B (1992) Applying ”Design by contract”. IEEE Comput, 25(10)
[19] Ward M (2009) Properties of slicing definitions. In: SCAM ’09: Proceedings of the 2009 ninth IEEE international working conference on source code analysis and manipulation. IEEE Computer Society, Washington, pp 23–32
[20] Weiser M (1981) Program slicing. In: ICSE ’81: Proceedings of the 5th international conference on software engineering. IEEE Press, Piscataway, pp 439–449
[21] Xu B, Qian J, Zhang X, Wu Z, Chen L (2005) A brief survey of program slicing. SIGSOFT Softw. Eng. Notes 30(2): 1–36
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.