[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: [email protected]*Subject*: Re: [NOISE] was Re: java security concerns*From*: [email protected] (Peter Madden) (by way of Duncan Frissell <[email protected]>)*Date*: Wed, 11 Oct 1995 09:35:28 -0400*Sender*: [email protected]

> Did you also send this post to [email protected]? No I didn't -- wasn't sure if that's where F. Stuart's email originated from. Please feel free to circulate to the universe, along with some further clarification below. I hope I wasn't too positive in my support of auto. program verification. There are real problems. However, with the development of the field called formal methods, computation has been directly linked to mathematical logic, which is a much better understood, and well circumscribed, domain than programming languages per se. Applications of formal methods in software engineering depend critically on the use of automated theorem provers to provide improved support for the development of safety critical systems. Potentially catastrophic consequences can derive from the failure of computerized systems upon which human lives rely such as medical diagnostic systems, air traffic control systems and defence systems (the recent failure of the computerized system controlling the London Ambulance Service provides an example of how serious software failure can be). Formal methods are used to provide programs with, or prove that programs have, certain properties: a program may be proved to terminate; two programs may be proved equivalent; an inefficient program may be transformed into an equivalent efficient program; a program may be verified to satisfy some specification (i.e. a program is proved to compute the specified function/relation); and a program may be synthesized that satisfies some specification. Program Verification boils down to proving a mathematical conjecture specifying that a given program will, for all inputs of a certain type, generate outputs of a certain type. This is relatively straightforward -- we already have the program P described in the initial conjecture to be proved. Program synthesis, on the other hand, starts with a similar conjecture *except* that P remains an unidentified variable. The task of synthesis (auto. or otherwise) is to incrementally identify P as the conjecture proof is unraveled. This requires all kinds of "intelligent", and often intuitive, choices during the proof, and is consequently a difficult process to automate. Peter ================================================================= Dr Peter Madden, Email: [email protected] Max-Planck-Institut fuer Informatik, Phone: (49) (681) 302-5434 Im Stadtwald, W-66123 Saarbruecken, Germany. Fax: (49) (681) 302-5401 =================================================================

**Follow-Ups**:**Re: [NOISE] was Re: java security concerns***From:*"Perry E. Metzger" <[email protected]>

- Prev by Date:
**Re: [NOISE] was Re: java security concerns** - Next by Date:
**Public Awarreness of Security** - Prev by thread:
**Re: [NOISE] was Re: java security concerns** - Next by thread:
**Re: [NOISE] was Re: java security concerns** - Index(es):