Handbook of model checking

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

• Introduction to model checking
• Model checking
• scientific article; zbMATH DE number 1633145
• scientific article; zbMATH DE number 1487860
• scientific article; zbMATH DE number 5585443

Mathematics Subject Classification ID

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 (72)

• 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?)
• Title not available (Why is that?)
• Model-checking structured context-free languages
• Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Assumption-based runtime verification
• Back to the future: a fresh look at linear temporal logic
• Strategy Complexity of Point Payoff, Mean Payoff and Total Payoff Objectives in Countable MDPs
• Digital Bifurcation Analysis of Internet Congestion Control Protocols
• 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
• Task-Aware Verifiable RNN-Based Policies for Partially Observable Markov Decision Processes
• Title not available (Why is that?)
• Spatio-Temporal Model-Checking of Cyber-Physical Systems Using Graph Queries
• Using approximation for the verification of token-scaling models
• Abstraction-based control synthesis using partial information
• Decidability of liveness for concurrent objects on the TSO memory model
• Partial Order Reduction for Deep Bug Finding in Synchronous Hardware
• 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
• N-PAT: A Nested Model-Checker
• Combining Model Checking and Deduction
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Automated Verification of Parallel Nested DFS
• 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)