scientific article; zbMATH DE number 910719
From MaRDI portal
Publication:4885877
zbMath0847.68063MaRDI QIDQ4885877
No author found.
Publication date: 28 July 1996
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (40)
Extracting unsatisfiable cores for LTL via temporal resolution ⋮ Formal verification of mobile robot protocols ⋮ An abstraction-refinement methodology for reasoning about network games ⋮ Invariant-driven specifications in Maude ⋮ Modeling for Verification ⋮ Symbolic model checking for channel-based component connectors ⋮ Wu's characteristic set method for SystemVerilog assertions verification ⋮ On equilibria in quantitative games with reachability/safety objectives ⋮ Synthesising correct concurrent runtime monitors ⋮ Application of static analyses for state-space reduction to the microcontroller binary code ⋮ A state/event-based model-checking approach for the analysis of abstract system properties ⋮ Flash memory efficient LTL model checking ⋮ Symbolic execution of Reo circuits using constraint automata ⋮ Towards a notion of unsatisfiable and unrealizable cores for LTL ⋮ A computer scientist looks at game theory. ⋮ On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties ⋮ Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning ⋮ Automatic verification of reduction techniques in higher order logic ⋮ Model checking RAISE applicative specifications ⋮ SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata ⋮ Quantifier elimination by dependency sequents ⋮ Minimal refinements of specifications in modal and temporal logics ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Modeling Concurrent systems specified in a Temporal Concurrent Constraint language-I ⋮ Minimal refinements of specifications in modal and temporal logics ⋮ Partial order reduction for state/event LTL with application to component-interaction automata ⋮ On ACTL formulas having linear counterexamples ⋮ Verification by augmented abstraction: The automata-theoretic view ⋮ Actor-based slicing techniques for efficient reduction of Rebeca models ⋮ A novel analysis space for pointer analysis and its application for bug finding ⋮ Pentagons: a weakly relational abstract domain for the efficient validation of array accesses ⋮ An axiomatic semantics for \(\mathsf{ioco} \underline{\mathsf{s}}\) conformance relation ⋮ Active learning for extended finite state machines ⋮ CEGAR for compositional analysis of qualitative properties in Markov decision processes ⋮ Variable and clause elimination for LTL satisfiability checking ⋮ Evaluation of cyber security and modelling of risk propagation with Petri nets ⋮ Verification by augmented finitary abstraction ⋮ Compositional verification of asynchronous concurrent systems using CADP
Uses Software
This page was built for publication:
