Handbook of model checking
From MaRDI portal
Recommendations
Cited in
(99)- Non-deterministic Weighted Automata on Random Words
- Modeling of parallel program synchronization primitives
- Book review of: E. M. Clarke (ed.) et al., Handbook of model checking
- scientific article; zbMATH DE number 7561612 (Why is no real title available?)
- Model-checking structured context-free languages
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- Partial order reduction for deep bug finding in synchronous hardware
- Separability and non-determinizability of WSTS
- LTL-specification for development and verification of control programs
- scientific article; zbMATH DE number 7589539 (Why is no real title available?)
- scientific article; zbMATH DE number 7577573 (Why is no real title available?)
- An exact schedulability test for real-time systems with abstract scheduler on multiprocessor platforms
- Pattern-based approach to automation of deductive verification of process-oriented programs: patterns, lemmas and algorithms
- A divide \& conquer approach to conditional stable model checking
- Session-based concurrency in Maude: executable semantics and type checking
- \textsf{symQV}: automated symbolic verification of quantum programs
- Learning infinite-word automata with loop-index queries
- Abstraction for non-ground answer set programs
- Generative program analysis and beyond: the power of domain-specific languages (invited paper)
- Knowledge acquisition in multi-agent systems: a formalization of the Eleusis card game
- scientific article; zbMATH DE number 7559473 (Why is no real title available?)
- Mirrors and memory in quantum automata
- On the Complexity of Value Iteration
- Fifty years of Hoare's logic
- A local search approach to protocol verification
- On the power of finite ambiguity in Büchi complementation
- On the termination problem for probabilistic higher-order recursive programs
- Assumption-based runtime verification
- Back to the future: a fresh look at linear temporal logic
- Software testing in computable analysis
- Complexity results for modal logic with recursion via translations and tableaux
- Automated verification of parallel nested DFS
- Strategy Complexity of Point Payoff, Mean Payoff and Total Payoff Objectives in Countable MDPs
- Symbolic realisation of epistemic processes
- Efficient simulation for hardware model checking
- Book review of: J. F. Groote and M. R. Mousavi, Modeling and analysis of communicating systems
- Constrained existence problem for weak subgame perfect equilibria with \(\omega \)-regular Boolean objectives
- One-pass and tree-shaped tableau systems for TPTL and \(\mathrm{TPTL_b+Past}\)
- Building strategies into QBF proofs
- ASQ-IT: interactive explanations for reinforcement-learning agents
- Strategies, model checking and branching-time properties in Maude
- Simulation by Rounds of Letter-to-Letter Transducers
- Certifying phase abstraction
- Event-driven temporal logic pattern for control software requirements specification
- An Overview of the Maude Strategy Language and its Applications
- A program instrumentation framework for automatic verification
- Why there is no general solution to the problem of software verification
- Fast three-valued abstract bit-vector arithmetic
- From verification to causality-based explications (invited talk)
- Automated and sound synthesis of Lyapunov functions with SMT solvers
- Optimal transformations of games and automata using Muller conditions
- Faster algorithms for bounded liveness in graphs and game graphs
- Calculational design of a regular model checker by abstract interpretation
- How to play in infinite MDPs (invited talk)
- Using approximation for the verification of token-scaling models
- scientific article; zbMATH DE number 1487860 (Why is no real title available?)
- Synthesizing Computable Functions from Rational Specifications Over Infinite Words
- Flow logic
- Flow logic
- Remarks on Parikh-recognizable omega-languages
- A higher-order transformation approach to the formalization and analysis of BPMN using graph transformation systems
- Abstraction-based control synthesis using partial information
- Verifiably safe exploration for end-to-end reinforcement learning
- LTL reactive synthesis with a few hints
- Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers
- Decidability of liveness for concurrent objects on the TSO memory model
- Finite-memory strategies for almost-sure energy-meanpayoff objectives in MDPs
- scientific article; zbMATH DE number 1701755 (Why is no real title available?)
- Introduction to model checking
- Invariant neural architecture for learning term synthesis in instantiation proving
- N-PAT: A Nested Model-Checker
- Spatio-temporal model-checking of cyber-physical systems using graph queries
- Combining Model Checking and Deduction
- Propositional dynamic logic formula synthesis and some applications
- When is the normalized edit distance over non-uniform weights a metric?
- scientific article; zbMATH DE number 7649960 (Why is no real title available?)
- Black-box rare-event simulation for safety testing of AI agents: an overview
- scientific article; zbMATH DE number 7559495 (Why is no real title available?)
- Digital bifurcation analysis of Internet congestion control protocols
- Model checking meets auto-tuning of high-performance programs
- Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic
- scientific article; zbMATH DE number 7559300 (Why is no real title available?)
- Automatic assume-guarantee reasoning for safety and liveness using passive learning
- Automatic WSTS-based repair and deadlock detection of parameterized systems
- Diagnosability verification using LTL model checking
- Timed automata verification and synthesis via finite automata learning
- Synthesis of parametric hybrid automata from time series
- Local search for solving satisfiability of polynomial formulas
- Learning model checking and the kernel trick for signal temporal logic on stochastic processes
- Automatic program instrumentation for automatic verification
- Transition power abstractions for deep counterexample detection
- On strings in software model checking
- Automata with timers
- Timed automata verification and synthesis via finite automata learning
- Strategy complexity of limsup and liminf threshold objectives in countable MDPs, with applications to optimal expected payoffs
- The reachable simulation problem
- Deterministic weighted automata under partial observability
- Task-aware verifiable RNN-based policies for partially observable Markov decision processes
- \textsc{Cgaal}: distributed on-the-fly ATL model checker with heuristics
This page was built for publication: Handbook of model checking
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4572078)
