Computer aided verification

More about the book

The book features a collection of invited talks and sessions covering a range of topics in formal specifications, verification, and model checking. It begins with discussions on the realities of formal specifications in industrial code and the implications of e-voting on democracy. Subsequent sessions delve into automata theory, presenting algorithms for checking universality and minimizing generalized Büchi automata. Tools for interface compatibility and composition are introduced alongside advancements in arithmetic, including applications for real addition. The sessions also explore bounded model checking and abstraction/refinement techniques, highlighting lazy abstraction with interpolants and the use of statically computed invariants. Various tools for verification, such as C assertion checkers and software model checkers, are presented. Symbolic trajectory evaluation is another focus, emphasizing automatic refinement and vacuity detection. Further discussions cover property specification, time complexity in model checking, and the challenges of verifying communicating timed automata. Concurrency is addressed through symbolic model checking of concurrent programs, while tree languages and pushdown systems are examined for model checking improvements. Termination analysis and tools for concolic unit testing are also included, alongside techniques for memory consistency verification and shape analysis, showcasing advancem