Handbook of model checking
From MaRDI portal
Publication:4572078
Recommendations
Cited in
(73)- A local search approach to protocol verification
- Deterministic weighted automata under partial observability
- Knowledge acquisition in multi-agent systems: a formalization of the Eleusis card game
- Verifiably safe exploration for end-to-end reinforcement learning
- LTL-specification for development and verification of control programs
- Invariant neural architecture for learning term synthesis in instantiation proving
- Mirrors and memory in quantum automata
- Simulation by Rounds of Letter-to-Letter Transducers
- 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
- Synthesizing Computable Functions from Rational Specifications Over Infinite Words
- Complexity results for modal logic with recursion via translations and tableaux
- An Overview of the Maude Strategy Language and its Applications
- A higher-order transformation approach to the formalization and analysis of BPMN using graph transformation systems
- Abstraction-based control synthesis using partial information
- Generative program analysis and beyond: the power of domain-specific languages (invited paper)
- Learning infinite-word automata with loop-index queries
- Partial order reduction for deep bug finding in synchronous hardware
- Strategy Complexity of Point Payoff, Mean Payoff and Total Payoff Objectives in Countable MDPs
- Digital bifurcation analysis of Internet congestion control protocols
- Non-deterministic Weighted Automata on Random Words
- Using approximation for the verification of token-scaling models
- scientific article; zbMATH DE number 1701755 (Why is no real title available?)
- On the power of finite ambiguity in Büchi complementation
- N-PAT: A Nested Model-Checker
- Model-checking structured context-free languages
- Decidability of liveness for concurrent objects on the TSO memory model
- A divide \& conquer approach to conditional stable model checking
- Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers
- Book review of: J. F. Groote and M. R. Mousavi, Modeling and analysis of communicating systems
- Synthesis of parametric hybrid automata from time series
- Book review of: E. M. Clarke (ed.) et al., Handbook of model checking
- 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
- Abstraction for non-ground answer set programs
- scientific article; zbMATH DE number 7559300 (Why is no real title available?)
- Diagnosability verification using LTL model checking
- Calculational design of a regular model checker by abstract interpretation
- Why there is no general solution to the problem of software verification
- Fast three-valued abstract bit-vector arithmetic
- Fifty years of Hoare's logic
- Model checking meets auto-tuning of high-performance programs
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- Automated and sound synthesis of Lyapunov functions with SMT solvers
- scientific article; zbMATH DE number 7559495 (Why is no real title available?)
- Combining Model Checking and Deduction
- Task-aware verifiable RNN-based policies for partially observable Markov decision processes
- Session-based concurrency in Maude: executable semantics and type checking
- scientific article; zbMATH DE number 7559473 (Why is no real title available?)
- Back to the future: a fresh look at linear temporal logic
- On the termination problem for probabilistic higher-order recursive programs
- \textsf{symQV}: automated symbolic verification of quantum programs
- scientific article; zbMATH DE number 7561612 (Why is no real title available?)
- scientific article; zbMATH DE number 7589539 (Why is no real title available?)
- On the Complexity of Value Iteration
- scientific article; zbMATH DE number 7649960 (Why is no real title available?)
- Introduction to model checking
- scientific article; zbMATH DE number 1487860 (Why is no real title available?)
- Flow logic
- Flow logic
- Event-driven temporal logic pattern for control software requirements specification
- Assumption-based runtime verification
- scientific article; zbMATH DE number 7577573 (Why is no real title available?)
- Strategies, model checking and branching-time properties in Maude
- Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic
- Automated verification of parallel nested DFS
- Spatio-temporal model-checking of cyber-physical systems using graph queries
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)
