scientific article; zbMATH DE number 7088727

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

Publication date: 5 August 2019

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Specification and verification (program logics, model checking, etc.) (68Q60) Research exposition (monographs, survey articles) pertaining to computer science (68-02)

Related Items

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, Introduction to Model Checking, BDD-Based Symbolic Model Checking, SAT-Based Model Checking, Combining Model Checking and Deduction, Symbolic Trajectory Evaluation, Thread-modular analysis of release-acquire concurrency, On the Model Checking Problem for Some Extension of CTL*, Multi-Valued Reasoning about Reactive Systems, 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, The complexity of model checking multi-stack systems, Untangling the graphs of timed automata to decrease the number of clocks, An application of temporal projection to interleaving concurrency, Verification and Control of Probabilistic Rectangular Hybrid Automata, Formal analysis of composable DeFi protocols, 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, Compositional Specification in Rewriting Logic, Supervisory control and reactive synthesis: a comparative introduction, 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, Formal verification of robotic cell injection systems up to 4-DOF using \textsf{HOL Light}, 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, Unnamed Item, Deadlock checking by a behavioral effect system for lock handling, Unnamed Item, Predicate Abstraction in Program Verification: Survey and Current Trends, Unnamed Item, Unnamed Item, The mechanical generation of fault trees for reactive systems via retrenchment. II. Clocked and feedback circuits, Syntax-guided synthesis for lemma generation in hardware model checking, A design of GPU-based quantitative model checking, An automatic abstraction technique for verifying featured, parameterised systems, Finding minimum and maximum termination time of timed automata models with cyclic behaviour, Diagnosability analysis of patterns on bounded labeled prioritized Petri nets, A system for deduction-based formal verification of workflow-oriented software models, Unnamed Item, A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability, Petri nets with name creation for transient secure association, A Parametrized Analysis of Algorithms on Hierarchical Graphs, Parameter Synthesis Through Temporal Logic Specifications, Estimation of the complexity of the potential transformation algorithm for solving cyclic games on graphs, Improving parity games in practice, Unnamed Item, Quasi-optimal partial order reduction, A symbolic shortest path algorithm for computing subgame-perfect Nash equilibria, Deciding probabilistic bisimilarity distance one for probabilistic automata, Efficient data validation for geographical interlocking systems, A Theory of Distributed Markov Chains, Stubborn Sets, Frozen Actions, and Fair Testing, Book review of: E. M. Clarke (ed.) et al., Handbook of model checking, Differential dynamic logic for hybrid systems, Computation tree logic model checking over possibilistic decision processes under finite-memory scheduler, Unnamed Item, SAT-based explicit LTL reasoning and its application to satisfiability checking, Parameter synthesis of polynomial dynamical systems, LTL-Specification of Bounded Counter Machines, 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