ECLAIR: Difference between revisions
Reference to publication about ECLAIR added. |
No edit summary |
||
| Line 17: | Line 17: | ||
== Capabilities == |
== Capabilities == |
||
ECLAIR uses [[formal methods]]-based static code analysis techniques such as [[abstract interpretation]] and [[model checking]] combined with [[constraint satisfaction]] techniques to detect or prove the absence of certain run |
ECLAIR uses [[formal methods]]-based static code analysis techniques such as [[abstract interpretation]] and [[model checking]] combined with [[constraint satisfaction]] techniques to detect or prove the absence of certain [[run time (program lifecycle phase)|run time errors]] in [[source code]]. It is a complete re-engineering of a series of prototypes<ref>{{cite arXiv |author=R. Bagnara, P. M. Hill, E. Zaffanella |eprint=0711.0345 |title=A Prolog-based Environment for Reasoning about Programming Languages |year=2007 }}</ref> developed at the Applied Formal Methods Laboratory of the [[University of Parma]]. |
||
ECLAIR supports the automatic checking of conformance with respect to several coding standards, among which [[MISRA C]], MISRA C++, CERT C Secure Coding Standard, CERT C++ Secure Coding Standard, High-Integrity C++, [[NASA]]/[[JPL]] C, [[ESA]]/BSSC C/C++, [[Joint Strike Fighter program|JSF]] C++, EC--<ref>{{cite doi|10.1016/j.infsof.2004.08.001}}</ref>, Netrino Embedded C<ref>{{cite isbn|1442164824}}</ref>, The Power of Ten (C)<ref>{{cite doi|10.1109/MC.2006.212}}</ref>, Industrial Strength C++<ref>{{cite isbn|0131209655}}</ref>. |
ECLAIR supports the automatic checking of conformance with respect to several coding standards, among which [[MISRA C]], MISRA C++, CERT C Secure Coding Standard, CERT C++ Secure Coding Standard, High-Integrity C++, [[NASA]]/[[JPL]] C, [[ESA]]/BSSC C/C++, [[Joint Strike Fighter program|JSF]] C++, EC--<ref>{{cite doi|10.1016/j.infsof.2004.08.001}}</ref>, Netrino Embedded C<ref>{{cite isbn|1442164824}}</ref>, The Power of Ten (C)<ref>{{cite doi|10.1109/MC.2006.212}}</ref>, Industrial Strength C++<ref>{{cite isbn|0131209655}}</ref>. |
||
Revision as of 14:15, 26 November 2012
 | This article, ECLAIR, has recently been created via the Articles for creation process. Please check to see if the reviewer has accidentally left this template after accepting the draft and take appropriate action as necessary.
Reviewer tools: Inform author |
| Developer(s) | BUGSENG |
|---|---|
| Stable release | 1.2
/ November 12, 2012 |
| Operating system | Cross-platform |
| Type | static code analysis |
| License | Proprietary |
| Website | ECLAIR |
ECLAIR is a static code analysis tool for the automatic analysis, verification, testing and transformation of C and C++ programs.
Capabilities
ECLAIR uses formal methods-based static code analysis techniques such as abstract interpretation and model checking combined with constraint satisfaction techniques to detect or prove the absence of certain run time errors in source code. It is a complete re-engineering of a series of prototypes[1] developed at the Applied Formal Methods Laboratory of the University of Parma.
ECLAIR supports the automatic checking of conformance with respect to several coding standards, among which MISRA C, MISRA C++, CERT C Secure Coding Standard, CERT C++ Secure Coding Standard, High-Integrity C++, NASA/JPL C, ESA/BSSC C/C++, JSF C++, EC--[2], Netrino Embedded C[3], The Power of Ten (C)[4], Industrial Strength C++[5].
ECLAIR can automatically synthesize sets of unit test inputs that reach a specified coverage criterion (or prove that, due to infeasible conditions in the program, such coverage cannot be attained).
ECLAIR can also be used to perform complex program transformations: program regions in the source identified by syntactic and semantics-based criteria can be automatically found and optionally replaced with a parametrized substitution.
See also
References
- ^ R. Bagnara, P. M. Hill, E. Zaffanella (2007). "A Prolog-based Environment for Reasoning about Programming Languages". arXiv:0711.0345.
{{cite arXiv}}: CS1 maint: multiple names: authors list (link) - ^ Attention: This template ({{cite doi}}) is deprecated. To cite the publication identified by doi:10.1016/j.infsof.2004.08.001, please use {{cite journal}} (if it was published in a bona fide academic journal, otherwise {{cite report}} with
|doi=10.1016/j.infsof.2004.08.001instead. - ^ Template:Cite isbn
- ^ Attention: This template ({{cite doi}}) is deprecated. To cite the publication identified by doi:10.1109/MC.2006.212, please use {{cite journal}} (if it was published in a bona fide academic journal, otherwise {{cite report}} with
|doi=10.1109/MC.2006.212instead. - ^ Template:Cite isbn
External links
- Official website
- Partial list of CERT C rules supported by ECLAIR
- Partial list of CERT C++ rules supported by ECLAIR
Category:Static program analysis tools Category:Software testing tools Category:Software verification tools