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:42] vkuncak |
sav08:verification_as_science [2010/02/22 10:56] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Verification as Science - A View of Automated Software Analysis and Verification (SAV) ====== | + | ====== Verification as Science ====== |
| 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 and verification tools, which automatically answer certain classes of questions about software systems of interest: | ||
| Line 38: | Line 38: | ||
| ===== Why Focus on Software ===== | ===== Why Focus on Software ===== | ||
| - | We focus on software because our examples come from software | + | We focus on software because our examples come from software and it is easier evaluate these techniques on software. |
| 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 | ||