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 (74)

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

This page was built for publication: