Publication:5227061

Daniel Kroening, Doron A. Peled, Orna Grumberg, Helmut Veith, Edmund M. Clarke

Publication date: 5 August 2019

68-01: Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science

68Q60: Specification and verification (program logics, model checking, etc.)

68-02: Research exposition (monographs, survey articles) pertaining to computer science

Related Items

Unnamed Item, Unnamed Item, A Theory of Distributed Markov Chains, Stubborn Sets, Frozen Actions, and Fair Testing, Unnamed Item, Compositional Specification in Rewriting Logic, A Parametrized Analysis of Algorithms on Hierarchical Graphs, Parameter Synthesis Through Temporal Logic Specifications, Deadlock checking by a behavioral effect system for lock handling, The mechanical generation of fault trees for reactive systems via retrenchment. II. Clocked and feedback circuits, Finding minimum and maximum termination time of timed automata models with cyclic behaviour, Diagnosability analysis of patterns on bounded labeled prioritized Petri nets, A symbolic shortest path algorithm for computing subgame-perfect Nash equilibria, Accelerating worst case execution time analysis of timed automata models with cyclic behaviour, Verification of distributed systems with the axiomatic system of MSVL, A quantitative study of pure parallel processes, An automatic abstraction technique for verifying featured, parameterised systems, Differential dynamic logic for hybrid systems, Supervisory control and reactive synthesis: a comparative introduction, A system for deduction-based formal verification of workflow-oriented software models, A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability, Improving parity games in practice, Quasi-optimal partial order reduction, Formal verification of robotic cell injection systems up to 4-DOF using \textsf{HOL Light}, Estimation of the complexity of the potential transformation algorithm for solving cyclic games on graphs, Deciding probabilistic bisimilarity distance one for probabilistic automata, Book review of: E. M. Clarke (ed.) et al., Handbook of model checking, SAT-based explicit LTL reasoning and its application to satisfiability checking, The complexity of model checking multi-stack systems, An application of temporal projection to interleaving concurrency, Petri nets with name creation for transient secure association, Verification and Control of Probabilistic Rectangular Hybrid Automata, Introduction to Model Checking, BDD-Based Symbolic Model Checking, SAT-Based Model Checking, Combining Model Checking and Deduction, Symbolic Trajectory Evaluation