Temporal Verification of Reactive Systems: Response

DOI10.1007/978-3-642-13754-9_13zbMath1288.68169OpenAlexW1606403830MaRDI QIDQ3587259

Publication date: 7 September 2010

Published in: Time for Verification (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-13754-9_13

Mathematics Subject Classification ID

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

Related Items (47)

Mechanizing a process algebra for network protocols ⋮ A temporal logic for asynchronous hyperproperties ⋮ Synthesizing efficient systems in probabilistic environments ⋮ Verifying a simplification of mutual exclusion by Lycklama-Hadzilacos ⋮ Graph Games and Reactive Synthesis ⋮ Automation of Quantitative Information-Flow Analysis ⋮ Synthesis of large dynamic concurrent programs from dynamic specifications ⋮ Finite-trace linear temporal logic: coinductive completeness ⋮ Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems ⋮ Leveraging Horn clause solving for compositional verification of PLC software ⋮ Horn Clause Solvers for Program Verification ⋮ Sound concurrent traces for online monitoring ⋮ Nontransitive temporal multiagent logic, information and knowledge, deciding algorithms ⋮ Theoretical and practical approaches to the denotational semantics for MDESL based on UTP ⋮ Generating invariants for non-linear loops by linear algebraic methods ⋮ Runtime verification of real-time event streams using the tool HStriver ⋮ Formal verification and quantitative metrics of MPSoC data dynamics ⋮ Formal communication elimination and sequentialization equivalence proofs for distributed system models ⋮ Temporal normal form for Linear Temporal Logic formulae1 ⋮ Safety assurance via on-line monitoring ⋮ Generalizing the Template Polyhedral Domain ⋮ Deductive verification of alternating systems ⋮ Parametrized invariance for infinite state processes ⋮ Rewriting-Based Runtime Verification for Alternation-Free HyperLTL ⋮ Inference Rules in Multi-agents’ Temporal Logics ⋮ RGITL: a temporal logic framework for compositional reasoning about interleaved programs ⋮ Functional Analysis of Large-Scale DNA Strand Displacement Circuits ⋮ Adaptation of Open Component-Based Systems ⋮ Game Quantification Patterns ⋮ On the Key Dependent Message Security of the Fujisaki-Okamoto Constructions ⋮ Liveness by Invisible Invariants ⋮ Verifying Reference Counting Implementations ⋮ SAT-Based Model Checking without Unrolling ⋮ Distributed and Predictable Software Model Checking ⋮ A temporal negative normal form which preserves implicants and implicates ⋮ Linear Temporal Logic with Non-transitive Time, Algorithms for Decidability and Verification of Admissibility ⋮ Towards a Thread-Local Proof Technique for Starvation Freedom ⋮ Realizability of Real-Time Logics ⋮ A practical integration of first-order reasoning and decision procedures ⋮ A proof theory for model checking ⋮ Unification and Inference Rules in the Multi-modal Logic of Knowledge and Linear Time LTK ⋮ Directed graph encoding in quantum computing supporting edge-failures ⋮ On automation in the verification of software barriers: experience report ⋮ Specification and verification of concurrent programs through refinements ⋮ Collecting statistics over runtime executions ⋮ Proof-based verification approaches for dynamic properties: application to the information system domain ⋮ Back to the future: a fresh look at linear temporal logic

This page was built for publication: Temporal Verification of Reactive Systems: Response