Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav08:verification_as_science [2010/02/22 10:56] vkuncak |
sav08:verification_as_science [2010/02/22 13:03] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Verification as Science ====== | + | ====== A Methodological View ====== |
- | In this course we study how to build software analysis and verification tools, which automatically answer certain classes of questions about software systems of interest: | + | In this course we study how to build software analysis, verification, and synthesis tools, which automatically answer certain classes of questions about software systems of interest: |
<draw name=sav08_big_picture> | <draw name=sav08_big_picture> | ||
- | Example questions (with sample links): | + | Example questions in analysis and verification (with sample links): |
* [[http://www.praxis-his.com/sparkada/publications_journals.asp|Will the program crash?]] | * [[http://www.praxis-his.com/sparkada/publications_journals.asp|Will the program crash?]] | ||
* [[http://www.key-project.org/|Does it compute the correct result?]] | * [[http://www.key-project.org/|Does it compute the correct result?]] | ||
Line 12: | Line 12: | ||
* [[http://portal.acm.org/citation.cfm?id=963948.963960|How much power does it consume?]] | * [[http://portal.acm.org/citation.cfm?id=963948.963960|How much power does it consume?]] | ||
* [[http://dx.doi.org/10.1016/j.conengprac.2004.04.002|Will it turn off automated cruise control?]] ([[http://abcnews.go.com/Blotter/toyota-recalls-prius-lexus-437000-vehicles/story?id=9784512|recall]] and [[http://abcnews.go.com/Blotter/RunawayToyotas|other runaway Toyota stories]]) | * [[http://dx.doi.org/10.1016/j.conengprac.2004.04.002|Will it turn off automated cruise control?]] ([[http://abcnews.go.com/Blotter/toyota-recalls-prius-lexus-437000-vehicles/story?id=9784512|recall]] and [[http://abcnews.go.com/Blotter/RunawayToyotas|other runaway Toyota stories]]) | ||
+ | |||
+ | In synthesis: Given a specification, find a program that satisfies this specification. | ||
Key steps in building such tools: | Key steps in building such tools: |