Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:verification_as_science [2010/02/22 10:42] vkuncak |
sav08:verification_as_science [2010/02/22 13:13] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Verification as Science - A View of Automated Software Analysis and Verification (SAV) ====== | + | ====== 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. | ||
| + | |||
| + | <draw name=sav08_synth_picture> | ||
| Key steps in building such tools: | Key steps in building such tools: | ||
| Line 36: | Line 40: | ||
| * automation means implementing **algorithms** for processing representation of software (e.g. source code) and representation of properties (e.g. formulas expressing desired properties), the study of these algorithms leads to questions of **decidability**, **computational complexity**, and **heuristics** that work on software systems of interest | * automation means implementing **algorithms** for processing representation of software (e.g. source code) and representation of properties (e.g. formulas expressing desired properties), the study of these algorithms leads to questions of **decidability**, **computational complexity**, and **heuristics** that work on software systems of interest | ||
| - | ===== Why Focus on Software ===== | ||
| - | We focus on software because our examples come from software | + | ===== Why Focus on SAV for Software ===== |
| + | |||
| + | We focus on software because software systems are the most complex human-made artifacts. | ||
| + | * and we can also write them ourselves and provide examples | ||
| Techniques we describe also apply to hardware and other systems: | Techniques we describe also apply to hardware and other systems: | ||
| - | * hardware systems can be simulated in software | + | * hardware systems are often finite state (but still very large), memory in software is practically unbounded (e.g. linked data structures, arbitrary-precision numbers) |
| - | * hardware systems are often finite state (but still very large), memory in software is practically unbounded (e.g. linked data structures) | + | * often we can write (concurrent) software whose behavior mimics hardware; if we can analyze this software, we can also analyze the corresponding hardware |
| - | * automated hardware verification is more successful than SAV, so there is a lot of space for future research | + | * automated hardware verification is more developed than automated software verification - a lot of space for future research in software |
| * in embedded systems we need to analyze software, hardware, and the environment (physics, biology); many of our techniques are still useful (even if not sufficient) for such systems | * in embedded systems we need to analyze software, hardware, and the environment (physics, biology); many of our techniques are still useful (even if not sufficient) for such systems | ||