Handbook of Model Checking

DOI10.1007/978-3-319-10575-8zbMath1390.68001OpenAlexW2912640545MaRDI QIDQ4572078

No author found.

Publication date: 4 July 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8

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)

Related Items

A divide \& conquer approach to conditional stable model checking, Strategy Complexity of Point Payoff, Mean Payoff and Total Payoff Objectives in Countable MDPs, Learning infinite-word automata with loop-index queries, Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers, Automated Verification of Parallel Nested DFS, Partial Order Reduction for Deep Bug Finding in Synchronous Hardware, Model-checking structured context-free languages, N-PAT: A Nested Model-Checker, Combining Model Checking and Deduction, Event-driven temporal logic pattern for control software requirements specification, Why there is no general solution to the problem of software verification, Fast three-valued abstract bit-vector arithmetic, Using approximation for the verification of token-scaling models, Unnamed Item, Abstraction-based control synthesis using partial information, On the power of finite ambiguity in Büchi complementation, Refutation-aware Gentzen-style calculi for propositional until-free linear-time temporal logic, Unnamed Item, Assumption-based runtime verification, Model checking meets auto-tuning of high-performance programs, LTL-specification for development and verification of control programs, Session-based concurrency in Maude: executable semantics and type checking, Mirrors and memory in quantum automata, Synthesis of parametric hybrid automata from time series, Decidability of liveness for concurrent objects on the TSO memory model, Unnamed Item, \textsf{symQV}: automated symbolic verification of quantum programs, Simulation by Rounds of Letter-to-Letter Transducers, Synthesizing Computable Functions from Rational Specifications Over Infinite Words, Verifiably safe exploration for end-to-end reinforcement learning, Digital Bifurcation Analysis of Internet Congestion Control Protocols, Generative program analysis and beyond: the power of domain-specific languages (invited paper), Calculational design of a regular model checker by abstract interpretation, Strategies, model checking and branching-time properties in Maude, Non-deterministic Weighted Automata on Random Words, Unnamed Item, Unnamed Item, Unnamed Item, Book review of: J. F. Groote and M. R. Mousavi, Modeling and analysis of communicating systems, Unnamed Item, Fifty years of Hoare's logic, 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, Unnamed Item, Unnamed Item, Abstraction for non-ground answer set programs, On the Complexity of Value Iteration, Unnamed Item, Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers, Diagnosability verification using LTL model checking, Task-Aware Verifiable RNN-Based Policies for Partially Observable Markov Decision Processes, Back to the future: a fresh look at linear temporal logic