Deprecated: $wgMWOAuthSharedUserIDs=false is deprecated, set $wgMWOAuthSharedUserIDs=true, $wgMWOAuthSharedUserSource='local' instead [Called from MediaWiki\HookContainer\HookContainer::run in /var/www/html/w/includes/HookContainer/HookContainer.php at line 135] in /var/www/html/w/includes/Debug/MWDebug.php on line 372
scientific article; zbMATH DE number 2102731 - MaRDI portal

scientific article; zbMATH DE number 2102731

From MaRDI portal

zbMath1046.68587MaRDI QIDQ4818818

Marco Roveri, Alessandro Cimatti, Edmund M. Clarke, Fausto Giunchiglia

Publication date: 24 September 2004


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



Related Items

Not all bugs are created equal, but robust reachability can tell the difference, Modelling timed reactive systems from natural-language requirements, Verifying data refinements using a model checker, GSTE is partitioned model checking, Exploiting interleaving semantics in symbolic state-space generation, The formal-CAFE methodology and model checking patterns in the specification of e-commerce systems, Data structures for symbolic multi-valued model-checking, Silver: an extensible attribute grammar system, A formalisation of violation, error recovery, and enforcement in the bit transmission problem, MAVEN: Modular aspect verification and interference analysis, From NuSMV to SPIN: Experiences with model checking flight guidance systems, An action-based approach to the formal specification and automatic analysis of business processes under authorization constraints, Using Patterns and Composite Propositions to Automate the Generation of LTL Specifications, Collaborative models for autonomous systems controller synthesis, A work-efficient distributed algorithm for reachability analysis, From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories, Formal verification based on Boolean expression diagrams, CTL Model-Checking with Graded Quantifiers, Model checking RAISE applicative specifications, CTL update of Kripke models through protections, Linear Temporal Logic Satisfaction in Adversarial Environments Using Secure Control Barrier Certificates, Toward model selection by formal methods, Incremental Learning-Based Testing for Reactive Systems, Applying model-checking to solve queries on semistructured data, Combining fault injection and model checking to verify fault tolerance, recoverability, and diagnosability in multi-agent systems, Verifying a Network Invariant for All Configurations of the Futurebus+ Cache Coherence Protocol, On the order of test goals in specification-based testing, Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints, Diagnostic Information for Realizability, A comparison of tools for teaching formal software verification, Complementary Criteria for Testing Temporal Logic Properties, Synergistic verification and validation of systems and software engineering models, Towards light-weight probabilistic model checking, Automated planning as an early verification tool for distributed control, Weak, strong, and strong cyclic planning via symbolic model checking, Conformant planning via symbolic model checking and heuristic search, Proof-based verification approaches for dynamic properties: application to the information system domain


Uses Software