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>

Example questions in analysis and verification (with sample links):

• Will the program crash?
• Does it compute the correct result?
• Does it leak private information?
• How long does it take to run?
• How much power does it consume?
• Will it turn off automated cruise control? (recall and 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:

1. modelling: establish precise mathematical meaning for software, environment, and questions of interest
   • discrete mathematics, mathematical logic, algebra
2. formalization: formalize this meaning using appropriate representation of programming languages and specification languages
   • program analysis, compilers, theory of formal languages, formal methods
3. designing algorithms: derive algorithms that manipulate such formal objects - key technical step
   • algorithms, dataflow analysis, abstract interpretation, decision procedures, constraint solving (e.g. SAT), theorem proving, AI
4. experimental evaluation: implement these algorithms and apply them to software systems
   • developing and using tools and infrastructures, learning lessons to improve other steps

Like science we are modeling part of reality (software systems and their environment) by introducing some mathematical models. Models are by necessity approximations of reality, because of our partial knowledge about the world and because too detailed models would become intractable.

Specific to SAV is the nature of software as the subject of study, which has several consequences:

• software is engineering artifact: to an extent we can choose our reality through programming language design and software methodology
• software has complex discrete, non-linear structure: millions of lines of code, gigabytes of bits of state, one condition in if statement can radically change future behaviors
• high standards of correctness: interest in details and exceptional behavior (bugs), not just general trends of behavior of software
• high standards along with large size make manual analysis infeasible in most cases and requires automation
• automation requires not just mathematical modeling where we use everyday mathematical techniques, but also formal modeling which requires us to specify the representation of systems and properties, making techniques from mathematical logic and model theory relevant
• 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

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:

• hardware systems are often finite state (but still very large), memory in software is practically unbounded (e.g. linked data structures, arbitrary-precision numbers)
• 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 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