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, Unnamed Item, Unnamed Item, A Theory of Distributed Markov Chains, Stubborn Sets, Frozen Actions, and Fair Testing, Unnamed Item, On the Model Checking Problem for Some Extension of CTL*, Multi-Valued Reasoning about Reactive Systems, Compositional Specification in Rewriting Logic, A Parametrized Analysis of Algorithms on Hierarchical Graphs, Parameter Synthesis Through Temporal Logic Specifications, Predicate Abstraction in Program Verification: Survey and Current Trends, LTL-Specification of Bounded Counter Machines, Unnamed Item, Unnamed Item, From linear temporal logics to Büchi automata: the early and simple principle, On monitoring linear temporal properties, Verification Modulo theories, Analysis and Transformation of Constrained Horn Clauses for Program Verification, Active learning for deterministic bottom-up nominal tree automata, An efficient customized clock allocation algorithm for a class of timed automata, On the complexity of rational verification, Certified reinforcement learning with logic guidance, Enhancing active model learning with equivalence checking using simulation relations, Session-based concurrency in Maude: executable semantics and type checking, Why3-do: the way of harmonious distributed system proofs, Probabilistic total store ordering, 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, Equilibria for games with combined qualitative and quantitative objectives, Measuring the constrained reachability in quantum Markov chains, Closing the gap between discrete abstractions and continuous control: completeness via robustness and controllability, 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, Efficient data validation for geographical interlocking systems, Computation tree logic model checking over possibilistic decision processes under finite-memory scheduler, Parameter synthesis of polynomial dynamical systems, Zone-based verification of timed automata: extrapolations, simulations and what next?, Small-gain theorem for safety verification of interconnected systems, On the combination of polyhedral abstraction and SMT-based model checking for Petri nets, On the hierarchical community structure of practical Boolean formulas, Thread-modular analysis of release-acquire concurrency, MC/DC test cases generation based on BDDs, Formal model of the interplay between TGF-\(\beta 1\) and MMP-9 and their dynamics in hepatocellular carcinoma, Untangling the graphs of timed automata to decrease the number of clocks, Formal verification of robotic cell injection systems up to 4-DOF using \textsf{HOL Light}, Syntax-guided synthesis for lemma generation in hardware model checking, A design of GPU-based quantitative model checking, 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, Formal analysis of composable DeFi protocols, 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