Automated technology for verification and analysis

En savoir plus sur le livre

The content includes invited talks and regular papers covering various topics in code auditing, model checking, and verification techniques. Key discussions focus on policies and proofs, industry trends, and property-driven abstraction for heap-manipulating programs. Notable papers explore abstraction refinement through topology invariants, complete SAT-based model checking for context-free processes, and bounded model checking for analog circuits. The efficient computation of minimal coverability sets for Petri nets and verification using models from simulation traces are also highlighted. Further contributions include automatic merge-point detection for sequential equivalence checking, proving termination of tree-manipulating programs, and symbolic fault tree analysis for reactive systems. The collection addresses game values in crash games, timed control strategies, and simulations on probabilistic automata. Mechanization of powerset construction for restricted classes of automata and verification of heap-manipulating programs in an SMT framework are discussed as well. Additional topics include distributed synthesis for alternating-time logics, finite state modeling of real-time systems, and approximate verification of Promela models. The content also covers formal methodologies for testing complex systems, bounded model checking for branching time logics, and compositional semantics for dynamic fault trees. Short paper