Mickaël Delahaye
Nikolai Kosmatov
ABSTRACT
Various combinations of static and dynamic analysis techniques were recently shown to be beneficial for software verification. A frequent obstacle to combining different tools in a completely automatic way is the lack of a common specification language. Our work proposes to translate a Pre-Post based specification into executable C code. This paper presents e-acsl, subset of the acsl specification language for C programs, and its automatic translator into C implemented as a Frama-C plug-in. The resulting C code is executable and can be used by a dynamic analysis tool. We illustrate how the PathCrawler test generation tool automatically treats such pre- and postconditions specified as C functions.
- M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system: An overview. In the Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, International Workshop (CASSIS 2004), volume 3362 of LNCS, pages 49--69. Springer, 2004. Google Scholar
Digital Library
- P. Baudin, J. C. Filliâtre, T. Hubert, C. Marché, B. Monate, Y. Moy, and V. Prevosto. ACSL: ANSI/ISO C Specification Language, v1.6, Sept. 2012. URL: http://frama-c.com/acsl.html.Google Scholar
- P. Baudin, A. Pacalet, J. Raguideau, D. Schoen, and N. Williams. CAVEAT: a tool for software validation. In the 2002 International Conference on Dependable Systems and Networks (DSN 2002), page 537. IEEE Computer Society, 2002. Google ScholarDigital Library
- B. Botella, M. Delahaye, S. Hong-Tuan-Ha, N. Kosmatov, P. Mouy, M. Roger, and N. Williams. Automating structural testing of C programs: Experience with PathCrawler. In the 4th International Workshop on Automation of Software Test (AST 2009), pages 70--78. IEEE Computer Society, 2009.Google ScholarCross Ref
- G. Canet, P. Cuoq, and B. Monate. A value analysis for C programs. In the Ninth IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM 2009), pages 123--124. IEEE Computer Society, 2009. Google ScholarDigital Library
- P. Chalin. Engineering a sound assertion semantics for the verifying compiler. IEEE Transactions on Software Engineering, 36:275--287, 2010. Google ScholarDigital Library
- O. Chebaro, N. Kosmatov, A. Giorgetti, and J. Julliand. Program slicing enhances a verification technique combining static and dynamic analysis. In the ACM Symposium on Applied Computing (SAC 2012), pages 1284--1291. ACM, 2012. Google ScholarDigital Library
- Y. Cheon. A Runtime Assertion Checker for the Java Modeling Language. Iowa State Univ., 2003. URL: http://cs.iastate.edu/~leavens/JML/Relatedpapers/index.html.Google ScholarCross Ref
- C. Comar, J. Kanig, and Y. Moy. Integrating formal program verification with testing. In the Embedded Real-Time Software and Systems Congress (ERTS 2012), 2012.Google Scholar
- L. Correnson and J. Signoles. Combining Analyses for C Program Verification. In the 17th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2012), volume 7437 of LNCS, pages 108--130. Springer, 2012.Google Scholar
- C. Csallner and Y. Smaragdakis. Check'n'crash: combining static checking and testing. In the 27th International Conference on Software Engineering (ICSE 2005), pages 422--431. ACM, 2005. Google ScholarDigital Library
- P. Cuoq, F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski. Frama-C, a program analysis perspective. In the 10th International Conference on Software Engineering and Formal Methods (SEFM 2012), volume 7504 of LNCS, pages 233--247. Springer, 2012. Google ScholarDigital Library
- M. D. Ernst, J. H. Perkins, P. J. Guo, S. McCamant, C. Pacheco, M. S. Tschantz, and C. Xiao. The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program., 69(1--3):35--45, 2007. Google ScholarDigital Library
- M. Fähndrich, M. Barnett, and F. Logozzo. Embedded contract languages. In the 2010 ACM Symposium on Applied Computing (SAC 2010), pages 2103--2110. ACM, 2010. Google ScholarDigital Library
- J.-C. Filliâtre and C. Marché. The Why/Krakatoa/Caduceus platform for deductive program verification. In the 19th International Conference on Computer Aided Verification (CAV 2007), volume 4590 of LNCS, pages 173--177. Springer, 2007. Google ScholarDigital Library
- B. S. Gulavani, T. A. Henzinger, Y. Kannan, A. V. Nori, and S. K. Rajamani. SYNERGY: a new algorithm for property checking. In the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2006), pages 117--127. ACM, 2006. Google ScholarDigital Library
- B. Hackett, M. Das, D. Wang, and Z. Yang. Modular checking for buffer overflows in the large. In 28th International Conference on Software Engineering (ICSE 2006), pages 232--241. ACM, 2006. Google ScholarDigital Library
- B. Konikowska, A. Tarlecki, and A. Blikle. A three-valued logic for software specification and validation. Fundam. Inform., pages 411--453, 1991.Google Scholar
- B. Meyer. Object-Oriented Software Construction. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1988. Google ScholarDigital Library
- G. C. Necula, S. McPeak, and W. Weimer. CCured: type-safe retrofitting of legacy code. In 29th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages (POPL 2002), pages 128--139. ACM, 2002. Google ScholarDigital Library
- J. Signoles. E-ACSL: Executable ANSI/ISO C Specification Language, Jan. 2012. URL: http://frama-c.com/download/e-acsl/e-acsl.pdf.Google Scholar
- J. Signoles. E-ACSL Version 1.5-4. Implementation in Frama-C Plug-in E-ACSL version 0.1, Jan. 2012. URL: http://frama-c.com/download/e-acsl/e-acsl-implementation.pdf.Google Scholar
- Y. Smaragdakis and C. Csallner. Combining static and dynamic reasoning for bug detection. In the First International Conference on Tests and Proofs (TAP 2007), volume 4454 of LNCS, pages 1--16. Springer, 2007. Google ScholarDigital Library
- Common specification language for static and dynamic analysis of C programs
Recommendations
An Abstract Specification Language for Static Program Analysis
Static program analysers typically come with a set of hard-coded checks, leaving little room for the user to add additional properties. In this work, we present a uniform approach to enable the specification of new static analysis checks in a concise ...
Operational ontological approach to formal programming language specification
Development of formal programming language specifications is an important problem of theoretical and practical programming. The paper presents operational ontological approach to formal specification of programming languages. It defines formalism for ...
Comments