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 13:03] vkuncak |
sav08:verification_as_science [2010/02/22 13:13] vkuncak |
||
|---|---|---|---|
| Line 14: | Line 14: | ||
| In synthesis: Given a specification, find a program that satisfies this specification. | 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 38: | 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 and it is easier evaluate these techniques on 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: | ||