CESAR

swMATH8510MaRDI QIDQ20519FDOQ20519

Author name not available (Why is that?)

Official website: http://link.springer.com/chapter/10.1007%2F3-540-11494-7_22

Cited In (only showing first 100 items - show all)

• Dependences in strategy logic
• \(\mathsf{QCTL}\) model-checking with \(\mathsf{QBF}\) solvers
• Automated analysis of mutual exclusion algorithms using CCS
• Title not available (Why is that?)
• Automatic verification of timed concurrent constraint programs
• An efficient approach for abstraction-refinement in model checking
• Augmenting ATL with strategy contexts
• Two normal form theorems for CSP programs
• Sémantique asynchrone et comportements infinis en CPS
• Title not available (Why is that?)
• Correct Hardware Design and Verification Methods
• Formal modelling, analysis and verification of hybrid systems
• Supervisory control and reactive synthesis: a comparative introduction
• A theory of formal synthesis via inductive learning
• Title not available (Why is that?)
• Using partial orders for the efficient verification of deadlock freedom and safety properties
• Title not available (Why is that?)
• Vacuity in practice: temporal antecedent failure
• Is your model checker on time? On the complexity of model checking for timed modal logics
• Temporal logic and fair discrete systems
• Combining symmetry reduction and under-approximation for symbolic model checking
• Complete abstractions and subclassical modal logics
• On the unusual effectiveness of logic in computer science
• Title not available (Why is that?)
• Title not available (Why is that?)
• Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving
• Program repair without regret
• Partitioned PLTL model-checking for refined transition systems
• An axiomatic semantics for \(\mathsf{ioco} \underline{\mathsf{s}}\) conformance relation
• Title not available (Why is that?)
• Linear temporal logic symbolic model checking
• A canonical form based decision procedure and model checking approach for propositional projection temporal logic
• A complete axiom system for propositional projection temporal logic with cylinder computation model
• Knowledge based scheduling of distributed systems
• Ranked Predicate Abstraction for Branching Time: Complete, Incremental, and Precise
• Title not available (Why is that?)
• Control machines: A new model of parallelism for compositional specifications and their effective compilation
• Model checking with strong fairness
• Local proofs for global safety properties
• Title not available (Why is that?)
• A proof system for unified temporal logic
• Introduction to model checking
• Model checking for hybrid logic
• Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems
• Synchrobench
• Model checking of systems with many identical timed processes
• On the semantics of strategy logic
• Title not available (Why is that?)
• Generating counterexamples for quantitative safety specifications in probabilistic B
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automatic verification of parameterized networks of processes
• Logical analysis of hybrid systems. Proving theorems for complex dynamics.
• Properties of a predicate transformer of the VRS system
• ATL with Strategy Contexts and Bounded Memory
• CTL Model-Checking with Graded Quantifiers
• Title not available (Why is that?)
• Title not available (Why is that?)
• Runtime verification of component-based systems
• Title not available (Why is that?)
• The modeling library of eavesdropping methods in quantum cryptography protocols by model checking
• Distributed symbolic model checking for \(\mu\)-calculus
• Verifying time partitioning in the DEOS scheduling kernel
• Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra
• Title not available (Why is that?)
• Structure-based deadlock checking of asynchronous circuits
• Dependences in strategy logic
• Syntax-directed model checking of sequential programs
• Meanings of model checking
• Model checking of pushdown systems for projection temporal logic
• rCOS: defining meanings of component-based software architectures
• Verifying a network invariant for all configurations of the Futurebus+ cache coherence protocol
• Title not available (Why is that?)
• Fifty years of Hoare's logic
• Title not available (Why is that?)
• Automated formal analysis and verification: an overview
• Title not available (Why is that?)
• Temporal normal form for linear temporal logic formulae
• Measuring and synthesizing systems in probabilistic environments
• Combining model checking and testing
• Transfer of model checking to industrial practice
• Probabilistic temporal logics via the modal mu-calculus
• Calculational design of a regular model checker by abstract interpretation
• Counting CTL
• On the order of test goals in specification-based testing
• Flow logic
• Flow logic
• Branching-Time Temporal Logics with Minimal Model Quantifiers
• Title not available (Why is that?)
• From Philosophical to Industrial Logics
• Verifying untimed and timed aspects of the experimental batch plant
• Logical vs. behavioural specifications
• Title not available (Why is that?)
• Smaller Abstractions for ∀CTL* without Next
• Combining Model Checking and Deduction
• Genetic Programming and Model Checking: Synthesizing New Mutual Exclusion Algorithms
• A novel approach to verifying context free properties of programs
• Mechanical software verification: high level control aspects from a user's perspective
• Automatically verifying temporal properties of pointer programs with cyclic proof
• Formal language properties of hybrid systems with strong resets

This page was built for software: CESAR