Nir Piterman Libri

Focusing on automata theoretic techniques, the book explores their application in model checking and satisfiability for advanced extensions of LTL, particularly in hardware design specifications. It highlights Intel's development of ForSpec, a specification language that expands LTL, and discusses the integration of automata in its backend translation tool. The study emphasizes the renewed interest in automata connectives and the effective use of alternating automata in this context, providing insights into their role in enhancing hardware model checking.

This book constitutes the refereed proceedings of the 11th International Haifa Verification Conference, HVC 2015, held in Haifa, Israel, in November 2015. The 17 revised full papers and 4 invited talks presented were carefully reviewed and selected from numerous submissions. The papers are organized in topical sections on hybrid systems; tools; verification of robotics; symbolic execution; model checking; timed systems; SAT solving; multi domain verification; and synthesis.

This book constitutes the proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2013, held in Rome, Italy, in March 2013. The 42 papers presented in this volume were carefully reviewed and selected from 172 submissions. They are organized in topical sections named: Markov chains; termination; SAT/SMT; games and synthesis; process algebra; pushdown; runtime verification and model checking; concurrency; learning and abduction; timed automata; security and access control; frontiers (graphics and quantum); functional programs and types; tool demonstrations; explicit-state model checking; Büchi automata; and competition on software verification.