Verification, Model Checking, and Abstract Interpretation

DOI10.1007/11609773zbMath1176.68126OpenAlexW2496613029MaRDI QIDQ5898629

Yaniv Sa'ar, Nir Piterman, Amir Pnueli

Publication date: 12 February 2007

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/11609773

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Effective Synthesis of Asynchronous Systems from GR(1) Specifications, LTL receding horizon control for finite deterministic systems, Graph Games and Reactive Synthesis, Verifying specifications in the language L against temporal properties nonexpressible in this language, Incorporating monitors in reactive synthesis without paying the price, Efficient and Dynamic Algorithms for Alternating Büchi Games and Maximal End-Component Decomposition, Maintenance goals of agents in a dynamic environment: formulation and policy construction, CGMurphi: automatic synthesis of numerical controllers for nonlinear hybrid systems, Index appearance record with preorders, Fairness, assumptions, and guarantees for extended bounded response \textsf{LTL+P} synthesis, Supervisory control and reactive synthesis: a comparative introduction, Augmented finite transition systems as abstractions for control synthesis, Agent planning programs, Tableaux for realizability of safety specifications, Reactive synthesis for relay-explorer consensus with intermittent communication, Realizability problem for constraint LTL, Harmonization of interacting automata, Towards a notion of unsatisfiable and unrealizable cores for LTL, Synthesis of Reactive(1) designs, Synthesis from scenario-based specifications, Antichains and compositional algorithms for LTL synthesis, Symbolic bounded synthesis, Robust control for signal temporal logic specifications using discrete average space robustness, Index Appearance Record for Transforming Rabin Automata into Parity Automata, Optimal Translation of LTL to Limit Deterministic Automata, GR(1)*: GR(1) specifications extended with existential guarantees, Problems of synthesis of \(\Sigma\)-automata specified in languages LP and LF of first order logic, Efficient controller synthesis for a fragment of \(\mathrm{MTL}_{0,\infty}\), Synthesizing robust systems, Functional Encryption for Inner Product with Full Function Privacy, Diagnostic Information for Realizability, A weakness measure for GR(1) formulae, Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games, Performance heuristics for GR(1) synthesis and related algorithms, Safety synthesis for incrementally stable switched systems using discretization-free multi-resolution abstractions, Funnel control for fully actuated systems under a fragment of signal temporal logic specifications, An automata-theoretic approach to model-checking systems and specifications over infinite data domains, Synthesis of succinct systems