Handbook of model checking
From MaRDI portal
Publication:4572078
DOI10.1007/978-3-319-10575-8zbMATH Open1390.68001OpenAlexW2912640545MaRDI QIDQ4572078FDOQ4572078
Authors:
Publication date: 4 July 2018
Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8
Recommendations
Proceedings, conferences, collections, etc. pertaining to computer science (68-06) Specification and verification (program logics, model checking, etc.) (68Q60) General reference works (handbooks, dictionaries, bibliographies, etc.) pertaining to computer science (68-00)
Cited In (73)
- Book review of: E. M. Clarke (ed.) et al., Handbook of model checking
- Title not available (Why is that?)
- Title not available (Why is that?)
- Partial order reduction for deep bug finding in synchronous hardware
- Model-checking structured context-free languages
- Title not available (Why is that?)
- Title not available (Why is that?)
- Session-based concurrency in Maude: executable semantics and type checking
- A divide \& conquer approach to conditional stable model checking
- \textsf{symQV}: automated symbolic verification of quantum programs
- Abstraction for non-ground answer set programs
- Title not available (Why is that?)
- Generative program analysis and beyond: the power of domain-specific languages (invited paper)
- Learning infinite-word automata with loop-index queries
- On the Complexity of Value Iteration
- On the power of finite ambiguity in Büchi complementation
- Fifty years of Hoare's logic
- 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
- Automated verification of parallel nested DFS
- Strategy Complexity of Point Payoff, Mean Payoff and Total Payoff Objectives in Countable MDPs
- 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
- Strategies, model checking and branching-time properties in Maude
- Event-driven temporal logic pattern for control software requirements specification
- 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
- Automated and sound synthesis of Lyapunov functions with SMT solvers
- Title not available (Why is that?)
- Using approximation for the verification of token-scaling models
- Flow logic
- Flow logic
- Abstraction-based control synthesis using partial information
- Decidability of liveness for concurrent objects on the TSO memory model
- Title not available (Why is that?)
- Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers
- Introduction to model checking
- Spatio-temporal model-checking of cyber-physical systems using graph queries
- N-PAT: A Nested Model-Checker
- Combining Model Checking and Deduction
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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
- Title not available (Why is that?)
- Diagnosability verification using LTL model checking
- Synthesis of parametric hybrid automata from time series
- Task-aware verifiable RNN-based policies for partially observable Markov decision processes
- Non-deterministic Weighted Automata on Random Words
- LTL-specification for development and verification of control programs
- Knowledge acquisition in multi-agent systems: a formalization of the Eleusis card game
- Mirrors and memory in quantum automata
- A local search approach to protocol verification
- Complexity results for modal logic with recursion via translations and tableaux
- Simulation by Rounds of Letter-to-Letter Transducers
- An Overview of the Maude Strategy Language and its Applications
- Synthesizing Computable Functions from Rational Specifications Over Infinite Words
- A higher-order transformation approach to the formalization and analysis of BPMN using graph transformation systems
- Verifiably safe exploration for end-to-end reinforcement learning
- Invariant neural architecture for learning term synthesis in instantiation proving
- 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
- Deterministic weighted automata under partial observability
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)
