Computer Aided Verification

Table of Contents

1. Altmetric Badge
   Book Overview
2. Altmetric Badge
   Chapter 1 Automatically Proving Program Termination
3. Altmetric Badge
   Chapter 2 A Mathematical Approach to RTL Verification
4. Altmetric Badge
   Chapter 3 Software Bugs Seen from an Industrial Perspective or Can Formal Methods Help on Automotive Software Development?
5. Altmetric Badge
   Chapter 4 Algorithms for Interface Synthesis
6. Altmetric Badge
   Chapter 5 A Tutorial on Satisfiability Modulo Theories
7. Altmetric Badge
   Chapter 6 A JML Tutorial: Modular Specification and Verification of Functional Behavior for Java
8. Altmetric Badge
   Chapter 7 Verification of Hybrid Systems
9. Altmetric Badge
   Chapter 8 SAT-Based Compositional Verification Using Lazy Learning
10. Altmetric Badge
    Chapter 9 Local Proofs for Global Safety Properties
11. Altmetric Badge
    Chapter 10 Low-Level Library Analysis and Summarization
12. Altmetric Badge
    Chapter 11 Verification Across Intellectual Property Boundaries
13. Altmetric Badge
    Chapter 12 On Synthesizing Controllers from Bounded-Response Properties
14. Altmetric Badge
    Chapter 13 An Accelerated Algorithm for 3-Color Parity Games with an Application to Timed Games
15. Altmetric Badge
    Chapter 14 UPPAAL-Tiga: Time for Playing Games!
16. Altmetric Badge
    Chapter 15 The TASM Toolset: Specification, Simulation, and Formal Verification of Real-Time Systems
17. Altmetric Badge
    Chapter 16 Systematic Acceleration in Regular Model Checking
18. Altmetric Badge
    Chapter 17 Parameterized Verification of Infinite-State Processes with Global Conditions
19. Altmetric Badge
    Chapter 18 CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes
20. Altmetric Badge
    Chapter 19 jMoped: A Test Environment for Java Programs
21. Altmetric Badge
    Chapter 20 Hector : Software Model Checking with Cooperating Analysis Plugins
22. Altmetric Badge
    Chapter 21 The Why/Krakatoa/Caduceus Platform for Deductive Program Verification
23. Altmetric Badge
    Chapter 22 Shape Analysis for Composite Data Structures
24. Altmetric Badge
    Chapter 23 Array Abstractions from Proofs
25. Altmetric Badge
    Chapter 24 Context-Bounded Analysis of Multithreaded Programs with Dynamic Linked Structures
26. Altmetric Badge
    Chapter 25 Revamping TVLA: Making Parametric Shape Analysis Competitive
27. Altmetric Badge
    Chapter 26 Fast and Accurate Static Data-Race Detection for Concurrent Programs
28. Altmetric Badge
    Chapter 27 Parametric and Sliced Causality
29. Altmetric Badge
    Chapter 28 Spade : Verification of Multithreaded Dynamic and Recursive Programs
30. Altmetric Badge
    Chapter 29 Anzu: A Tool for Property Synthesis
31. Altmetric Badge
    Chapter 30 RAT: A Tool for the Formal Analysis of Requirements
32. Altmetric Badge
    Chapter 31 Parallelising Symbolic State-Space Generators
33. Altmetric Badge
    Chapter 32 I/O Efficient Accepting Cycle Detection
34. Altmetric Badge
    Chapter 33 C32SAT: Checking C Expressions
35. Altmetric Badge
    Chapter 34 CVC3
36. Altmetric Badge
    Chapter 35 BAT: The Bit-Level Analysis Tool
37. Altmetric Badge
    Chapter 36 LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals
38. Altmetric Badge
    Chapter 37 Three-Valued Abstraction for Continuous-Time Markov Chains
39. Altmetric Badge
    Chapter 38 Magnifying-Lens Abstraction for Markov Decision Processes
40. Altmetric Badge
    Chapter 39 Underapproximation for Model-Checking Based on Random Cryptographic Constructions
41. Altmetric Badge
    Chapter 40 Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra
42. Altmetric Badge
    Chapter 41 Structural Abstraction of Software Verification Conditions
43. Altmetric Badge
    Chapter 42 An Abstract Domain for Analyzing Heap-Manipulating Low-Level Software
44. Altmetric Badge
    Chapter 43 Adaptive Symmetry Reduction
45. Altmetric Badge
    Chapter 44 From Liveness to Promptness
46. Altmetric Badge
    Chapter 45 Automated Assumption Generation for Compositional Verification
47. Altmetric Badge
    Chapter 46 Abstraction and Counterexample-Guided Construction of ω -Automata for Model Checking of Step-Discrete Linear Hybrid Models
48. Altmetric Badge
    Chapter 47 Test Coverage for Continuous and Hybrid Systems
49. Altmetric Badge
    Chapter 48 Hybrid Systems: From Verification to Falsification
50. Altmetric Badge
    Chapter 49 Comparison Under Abstraction for Verifying Linearizability
51. Altmetric Badge
    Chapter 50 Leaping Loops in the Presence of Abstraction
52. Altmetric Badge
    Chapter 51 Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
53. Altmetric Badge
    Chapter 52 A Decision Procedure for Bit-Vectors and Arrays
54. Altmetric Badge
    Chapter 53 Boolean Abstraction for Temporal Logic Satisfiability
55. Altmetric Badge
    Chapter 54 A Lazy and Layered SMT( $\mathcal{BV}$ ) Solver for Hard Industrial Verification Problems