Thumbnail
Access Restriction
Open

Author Yakhnis, Vladimir ♦ Winter, Victor
Source CiteSeerX
Content type Text
File Format PDF
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Partial Function ♦ Nonstrict Explicit Domain ♦ Automating Correctness Proof ♦ High Consequence System ♦ Formal Reasoning ♦ Software Development ♦ Strong Impact ♦ Formal Method ♦ Reasoning Framework ♦ Machine Control ♦ Powerful Technique ♦ Additional Dimension
Abstract As our society becomes technologically more complex, computers are being used in greater and greater numbers of high consequence systems. Giving a machine control over the lives of humans can be disturbing, especially if the software that is run on such a machine has bugs. Formal reasoning is one of the most powerful techniques available to demonstrate the correctness of a piece of software. When reasoning about software and its development, one frequently encounters expressions that contain partial functions. As might be expected, the presence of partial functions introduces an additional dimension of difficulty to the reasoning framework. This difficulty produces an especially strong impact in the case of high consequence systems. An ability to use formal methods for constructing software is essential if we want to obtain greater confidence in such systems through formal reasoning. This is only reasonable under automation of software development and verification. However, the ubiquit...
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study