Laboratory of Intelligent Software
Software Engineering and Artificial Intelligence
[Making correct software]
Software is pervasive throughout society, including life-critical and asset-management applications. In such areas, it is extremely important to verify that the software behaves as desired, together with its safety and correctness. Unfortunately, this is extremely difficult to do.
We can analyze a sequence of computer instructions (a program) in order to see what will occur, given particular inputs and circumstances. This allows us to check if the software has desired properties; for example, “If the brake pedal is pressed, the speed will certainly decrease without failure” or “Given any input, there will be a response produced”. (Maybe you have an irritating experience that even if you have given data to the computer and clicked the OK button, you cannot get a response from it!)
The difficulty is that in order to determine “Given any circumstances, the software will perform correctly”, there are a huge number of imaginable inputs and circumstances and it is difficult to check them all. Intelligent software is necessary to resolve this problem, and artificial intelligence (AI) is the key technique.
[Software development using artificial intelligence]
The most powerful technique is to write a formal, mathematical proof that the software has the properties desired. We use AI to automatically create such proofs.
Mathematical induction is a particularly important technique for certain proofs, and often proceeds as follows:
(1) The statement is true for value 0.
(2) If the statement is true for value n, then it is true for value n+1.
Proving these two cases suffices to prove the theorem for all natural numbers, while avoiding the need to explicitly consider all cases one by one.
Similar reasoning can be used in software, where the data in question is not constrained to a single natural number. By extending this to (one-dimensional) strings, (two-dimensional) images or (more complicated) data such as the web, we can efficiently examine various inputs and circumstances such as “arbitrary input data” or “at an arbitrary time”.