CESAR

swMATH8510MaRDI QIDQ20519

No author found.

Related Items (only showing first 100 items - show all)

Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Automatic verification of finite-state concurrent systems using temporal logic specifications ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Counting CTL ⋮ Logical Analysis of Hybrid Systems ⋮ Unnamed Item ⋮ An automata-theoretic approach to branching-time model checking ⋮ Real-Time Systems ⋮ Unnamed Item ⋮ Calculational design of a regular model checker by abstract interpretation ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Verifying a Network Invariant for All Configurations of the Futurebus+ Cache Coherence Protocol ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Knowledge Based Scheduling of Distributed Systems ⋮ An Automata-Theoretic Approach to Infinite-State Systems ⋮ Correct Hardware Design and Verification Methods ⋮ Methods for Knowledge Based Controlling of Distributed Systems ⋮ Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra ⋮ Symbolic model checking with rich assertional languages ⋮ Automatic verification of parameterized networks of processes ⋮ Unnamed Item ⋮ Bounded model checking using satisfiability solving ⋮ Meanings of Model Checking ⋮ Smaller Abstractions for ∀CTL* without Next ⋮ Formal language properties of hybrid systems with strong resets ⋮ From Philosophical to Industrial Logics ⋮ ATL with Strategy Contexts and Bounded Memory ⋮ Unnamed Item ⋮ Automatically verifying temporal properties of pointer programs with cyclic proof ⋮ Computer Aided Verification ⋮ Unnamed Item ⋮ Branching-Time Temporal Logics with Minimal Model Quantifiers ⋮ Automatic verification of timed concurrent constraint programs ⋮ Alternating automata: Unifying truth and validity checking for temporal logics ⋮ Measuring and Synthesizing Systems in Probabilistic Environments ⋮ Unnamed Item ⋮ Unnamed Item ⋮ \(\mathsf{QCTL}\) model-checking with \(\mathsf{QBF}\) solvers ⋮ From pre-historic to post-modern symbolic model checking ⋮ Compositional analysis for verification of parameterized systems ⋮ Bounded model checking of infinite state systems ⋮ Sémantique asynchrone et comportements infinis en CPS ⋮ Two normal form theorems for CSP programs ⋮ Introduction to Model Checking ⋮ Temporal Logic and Fair Discrete Systems ⋮ Combining Model Checking and Testing ⋮ Combining Model Checking and Deduction ⋮ Transfer of Model Checking to Industrial Practice ⋮ Algebraic simulations ⋮ Structure-based deadlock checking of asynchronous circuits ⋮ Coverage metrics for temporal logic model checking ⋮ A mechanism of function calls in MSVL ⋮ Question-guided stubborn set methods for state properties ⋮ Formal modeling and verification for MVB ⋮ Unnamed Item ⋮ Polynomial interrupt timed automata: verification and expressiveness ⋮ Characterizing finite Kripke structures in propositional temporal logic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A theory of formal synthesis via inductive learning ⋮ Dependences in Strategy Logic ⋮ Unnamed Item ⋮ A complete proof system for propositional projection temporal logic ⋮ Unnamed Item ⋮ rCOS: Defining Meanings of Component-Based Software Architectures ⋮ Formal Modelling, Analysis and Verification of Hybrid Systems ⋮ Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving ⋮ Unnamed Item ⋮ On the semantics of strategy logic ⋮ 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 ⋮ Model checking and synthesis for branching multi-weighted logics ⋮ Augmenting ATL with strategy contexts ⋮ Model checking of pushdown systems for projection temporal logic ⋮ Supervisory control and reactive synthesis: a comparative introduction ⋮ A proof system for unified temporal logic ⋮ A sound and complete proof system for a unified temporal logic ⋮ Complete Abstractions and Subclassical Modal Logics ⋮ \textsc{NeVer}: a tool for artificial neural networks verification ⋮ SPECIFICATION AND VERIFICATION OF CONURRENT SYSTEMS IN CESAR ⋮ Towards a notion of unsatisfiable and unrealizable cores for LTL ⋮ Automated analysis of mutual exclusion algorithms using CCS ⋮ Ranked Predicate Abstraction for Branching Time: Complete, Incremental, and Precise ⋮ Integrating predicate transition nets with first order temporal logic in the specification and verification of concurrent systems ⋮ Priority scheduling of distributed systems based on model checking ⋮ Interrupt timed automata: verification and expressiveness

This page was built for software: CESAR