LARA Projects in SAV 2009 In the order of final project presentation: Analysis of Assembly Execution Time Constraint Solving Modulo Theories Generation and Analysis of Transition Systems Combining Systematic Exploration and Symbolic Execution Computing Reachability Predicates Inferring return values and path conditions for library functions Program Synthesis Type System for External Uniqueness Unofficial Class Projects WS2S Decision Procedure in Software Verification SMT Solvers in Symbolic Execution