Static analysis - Revision history

David Monniaux: /* How it works in a nutshell */

2012-10-25T20:43:07Z

How it works in a nutshell

David Monniaux: /* How it works in a nutshell */

2012-10-25T20:40:43Z

How it works in a nutshell

David Monniaux: /* How it works in a nutshell */

2012-10-25T20:35:13Z

How it works in a nutshell

David Monniaux at 20:34, 25 October 2012

2012-10-25T20:34:28Z

David Monniaux at 20:27, 25 October 2012

2012-10-25T20:27:18Z

David Monniaux at 20:15, 25 October 2012

2012-10-25T20:15:40Z

David Monniaux at 20:10, 25 October 2012

2012-10-25T20:10:35Z

David Monniaux: Created page with "'''Static analysis''' is the act of deriving information about computer software (or, more generally, hardware or protocols) without actually running it, as opposed to '''dyna..."

2012-10-25T20:01:24Z

Created page with "'''Static analysis''' is the act of deriving information about computer software (or, more generally, hardware or protocols) without actually running it, as opposed to '''dyna..."

New page

'''Static analysis''' is the act of deriving information about computer software (or, more generally, hardware or protocols) without actually running it, as opposed to '''dynamic analysis''', which basically means testing the software by running it on sample cases in the hope of exercising a bug.

@@ Line 51: / Line 51: @@
 The comments marked as [[wikipedia:loop invariant|''invariants'']] are properties that are true throughout the execution (thus “invariants”). Technically, they are ''inductive invariants'' because they are shown to be true throughout a program execution by [[wikipedia:mathematical induction|mathematical induction]].
-The way our static analysis tool work is by deriving such properties
+The way our static analysis tool work is by deriving such properties, then showing that they entail user-specified assertions or other properties of interest. The user may also specify some assumptions about the environment of the program (library functions whose source code is not provided, external inputs...).
 ==Caveats==

@@ Line 2: / Line 2: @@
 ==How it works in a nutshell==
-Let us try [[Pagai]], one of our tools, on this C program:
+Let us try [[Pagai]], one of our tools, on this C program (an admittedly artificial example):
 <pre>int f() {
 	int i = 0;
@@ Line 17: / Line 17: @@
 	return i+j;
 }</pre>
 ==Caveats==

@@ Line 3: / Line 3: @@
 ==How it works in a nutshell==
 Let us try [[Pagai]], one of our tools, on this C program:
-<code>
+<pre>int f() {
 	int i = 0;
 	int j = 0;
@@ Line 17: / Line 16: @@
+	}
 	return i+j;
+}</pre>
 ==Caveats==

← Older revision		Revision as of 20:34, 25 October 2012
Line 1:		Line 1:
	'''Static analysis''' is the act of deriving information about computer software (or, more generally, hardware or protocols) without actually running it, as opposed to '''dynamic analysis''', which basically means testing the software by running it on sample cases in the hope of exercising a bug.		'''Static analysis''' is the act of deriving information about computer software (or, more generally, hardware or protocols) without actually running it, as opposed to '''dynamic analysis''', which basically means testing the software by running it on sample cases in the hope of exercising a bug.
		+
		+	==How it works in a nutshell==
		+	Let us try [[Pagai]], one of our tools, on this C program:
		+	<code>
		+	int f() {
		+	int i = 0;
		+	int j = 0;
		+
		+	while (i < 50) {
		+	j = 0;
		+	while (j < 50) {
		+	i++;
		+	j++;
		+	}
		+	i = i-j+1;
		+	}
		+	return i+j;
		+	}
		+	</code>

	==Caveats==		==Caveats==

@@ Line 1: / Line 1: @@
 '''Static analysis''' is the act of deriving information about computer software (or, more generally, hardware or protocols) without actually running it, as opposed to '''dynamic analysis''', which basically means testing the software by running it on sample cases in the hope of exercising a bug.
 Certain commercial providers call “static analysis” any check based on the source code of the program, including stylistic checks (e.g. presence of comments at any function entry, statistics on loop nests, and so on). In contrast, the analysis that we do inside the STATOR project is sound and based on the semantics of the program — meaning that if the analysis tool concludes, for instance, that some type conversion cannot overflow because the range of the value does not exceed that of the target type, this this is true for all execution of the program.  “Sound” means that our analysis will never ignore some cases that are actually possible in the program, so if it says that some problem does not occur, then it ''cannot'' occur (in some sense, it has proved that it cannot occur). Many commercial tools will instead provide ''false negatives'' — failing to point some issue that the tool is claimed to detect.
-This sounds too good to be true, and you may think there should be a catch. There are actually several. The main one is that a tool cannot be both sound and ''complete'' — here, completeness means that the tool is capable of proving any true property of the program. This means that a sound tool will fail to prove some properties, thus issuing warnings about problems that do not exist in the real system — ''false positives'' or ''false alarms''. This is unavoidable, as it is a consequence of mathematical properties of [[wikipedia:computable function|computable functions]] (the mathematical constructs underlying computer programs), more precisely of [[wikipedia:Rice's theorem|Rice's theorem]].
+This sounds too good to be true, and you may think there should be a catch. There are actually several.

← Older revision		Revision as of 20:15, 25 October 2012
Line 1:		Line 1:
	'''Static analysis''' is the act of deriving information about computer software (or, more generally, hardware or protocols) without actually running it, as opposed to '''dynamic analysis''', which basically means testing the software by running it on sample cases in the hope of exercising a bug.		'''Static analysis''' is the act of deriving information about computer software (or, more generally, hardware or protocols) without actually running it, as opposed to '''dynamic analysis''', which basically means testing the software by running it on sample cases in the hope of exercising a bug.

−	Certain commercial providers call “static analysis” any check based on the source code of the program, including stylistic checks (e.g. presence of comments at any function entry, statistics on loop nests, and so on). In contrast, the analysis that we do inside the STATOR project is sound and based on the semantics of the program — meaning that if the analysis tool concludes, for instance, that some type conversion cannot overflow because the range of the value does not exceed that of the target type, this this is true for all execution of the program. “Sound” means that our analysis will never ignore some cases that are actually possible in the program.	+	Certain commercial providers call “static analysis” any check based on the source code of the program, including stylistic checks (e.g. presence of comments at any function entry, statistics on loop nests, and so on). In contrast, the analysis that we do inside the STATOR project is sound and based on the semantics of the program — meaning that if the analysis tool concludes, for instance, that some type conversion cannot overflow because the range of the value does not exceed that of the target type, this this is true for all execution of the program. “Sound” means that our analysis will never ignore some cases that are actually possible in the program, so if it says that some problem does not occur, then it ''cannot'' occur (in some sense, it has proved that it cannot occur). Many commercial tools will instead provide ''false negatives'' — failing to point some issue that the tool is claimed to detect.
		+
		+	This sounds too good to be true, and you may think there should be a catch. There are actually several. The main one is that a tool cannot be both sound and ''complete'' — here, completeness means that the tool is capable of proving any true property of the program. This means that a sound tool will fail to prove some properties, thus issuing warnings about problems that do not exist in the real system — ''false positives'' or ''false alarms''. This is unavoidable, as it is a consequence of mathematical properties of [[wikipedia:computable function\|computable functions]] (the mathematical constructs underlying computer programs), more precisely of [[wikipedia:Rice's theorem\|Rice's theorem]].

← Older revision		Revision as of 20:10, 25 October 2012
Line 1:		Line 1:
	'''Static analysis''' is the act of deriving information about computer software (or, more generally, hardware or protocols) without actually running it, as opposed to '''dynamic analysis''', which basically means testing the software by running it on sample cases in the hope of exercising a bug.		'''Static analysis''' is the act of deriving information about computer software (or, more generally, hardware or protocols) without actually running it, as opposed to '''dynamic analysis''', which basically means testing the software by running it on sample cases in the hope of exercising a bug.
		+
		+	Certain commercial providers call “static analysis” any check based on the source code of the program, including stylistic checks (e.g. presence of comments at any function entry, statistics on loop nests, and so on). In contrast, the analysis that we do inside the STATOR project is sound and based on the semantics of the program — meaning that if the analysis tool concludes, for instance, that some type conversion cannot overflow because the range of the value does not exceed that of the target type, this this is true for all execution of the program. “Sound” means that our analysis will never ignore some cases that are actually possible in the program.