scientific article; zbMATH DE number 910719

From MaRDI portal

zbMath0847.68063MaRDI QIDQ4885877

No author found.

Publication date: 28 July 1996


Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.



Related Items

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