Model checking
From MaRDI portal
Recommendations
Cited in
(only showing first 100 items - show all)- Model checking action system refinements
- Differential dynamic logic for hybrid systems
- Model checking using net unfoldings
- Supervisory control and reactive synthesis: a comparative introduction
- Model checking at IBM
- 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
- Model checking.
- Software model checking
- Verification and control of probabilistic rectangular hybrid automata
- scientific article; zbMATH DE number 6720711 (Why is no real title available?)
- Introduction to model checking
- Modeling for Verification
- BDD-based symbolic model checking
- SAT-Based Model Checking
- Combining Model Checking and Deduction
- Symbolic trajectory evaluation
- scientific article; zbMATH DE number 4178463 (Why is no real title available?)
- Model Checking Value-Passing Modal Specifications
- Discriminative Model Checking
- CTL Model Checking for Boolean Program
- scientific article; zbMATH DE number 2020179 (Why is no real title available?)
- scientific article; zbMATH DE number 2021573 (Why is no real title available?)
- Deadlock checking by a behavioral effect system for lock handling
- scientific article; zbMATH DE number 2038698 (Why is no real title available?)
- scientific article; zbMATH DE number 2080188 (Why is no real title available?)
- scientific article; zbMATH DE number 1487867 (Why is no real title available?)
- scientific article; zbMATH DE number 1798181 (Why is no real title available?)
- Handbook of model checking
- The mechanical generation of fault trees for reactive systems via retrenchment. II. Clocked and feedback circuits
- scientific article; zbMATH DE number 2090135 (Why is no real title available?)
- scientific article; zbMATH DE number 910719 (Why is no real title available?)
- Model Checking Using Generalized Testing Automata
- A theory of distributed Markov chains
- Stubborn Sets, Frozen Actions, and Fair Testing
- Deciding probabilistic bisimilarity distance one for probabilistic automata
- Probabilistic timed automata with one clock and initialised clock-dependent probabilities
- On the Model Checking Problem for Some Extension of CTL*
- Multi-Valued Reasoning about Reactive Systems
- Finding minimum and maximum termination time of timed automata models with cyclic behaviour
- scientific article; zbMATH DE number 7559459 (Why is no real title available?)
- Compositional specification in rewriting logic
- Flow logic
- Diagnosability analysis of patterns on bounded labeled prioritized Petri nets
- New proposals to improve a MAC layer protocol in wireless sensor networks
- Meanings of model checking
- A Parametrized Analysis of Algorithms on Hierarchical Graphs
- Parameter synthesis through temporal logic specifications
- Predicate Abstraction in Program Verification: Survey and Current Trends
- Verification: Theory and Practice
- LTL-specification of bounded counter machines
- 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
- CRNs exposed: a method for the systematic exploration of chemical reaction networks
- 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
- Realizable and context-free hyperlanguages
- Reverse Engineering Through Automata Learning
- Symbolic analysis and parameter synthesis for time Petri nets using Maude and SMT solving
- MAG\(\pi\): types for failure-prone communication
- A matrix-based approach to parity games
- Model checking race-freedom when ``sequential consistency for data-race-free programs is guaranteed
- Searching for ribbon-shaped paths in fair transition systems
- Learning assumptions for compositional verification of timed automata
- Quantitative reachability Stackelberg-Pareto synthesis is \textsf{NEXPTIME}-complete
- Systems of fixpoint equations: abstraction, games, up-to techniques and local algorithms
- Temporal team semantics revisited
- Coalgebraic CTL: fixpoint characterization and polynomial-time model checking
This page was built for publication: Model checking
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5227061)
