scientific article; zbMATH DE number 1903365
From MaRDI portal
Publication:4804909
zbMATH Open1010.68766MaRDI QIDQ4804909FDOQ4804909
Authors: Alessandro Cimatti, Enrico Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, Armando Tacchella, Edmund Clarke, Fausto Giunchiglia 
Publication date: 1 May 2003
Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2404/24040359.htm
Title of this publication is not available (Why is that?)
Recommendations
Computing methodologies and applications (68U99) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (only showing first 100 items - show all)
- Spiking neural P systems: matrix representation and formal verification
- Search-based testing in membrane computing
- Proving stabilization of biological systems
- Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings
- Model checking merged program traces
- Performance heuristics for GR(1) synthesis and related algorithms
- Kernel P systems: from modelling to verification and testing
- Automatic synthesis of transiently correct network updates via Petri games
- The ASMETA approach to safety assurance of software systems
- An explicit transition system construction approach to LTL satisfiability checking
- Toward model selection by formal methods
- ZDD-based algorithmic framework for solving shortest reconfiguration problems
- An automatic method for the dynamic construction of abstractions of states of a formal model
- Synthesis of succinct systems
- Verification and enforcement of access control policies
- Producing explanations for rich logics
- Formal verification of temporal properties for reduced overhead in grid scientific workflows
- Linear-Time Model Checking: Automata Theory in Practice
- A new rule for LTL tableaux
- A backward-traversal-based approach for symbolic model checking of uniform strategies for constrained reachability
- Aeon 2021: bifurcation decision trees in Boolean networks
- Greening R. Thomas' framework with environment variables: a divide and conquer approach
- Strategies, model checking and branching-time properties in Maude
- A Cookbook for Temporal Conceptual Data Modelling with Description Logics
- Social bot detection as a temporal logic model checking problem
- AutoHyper: explicit-state model checking for HyperLTL
- Verification Modulo theories
- Formal verification of timed synchronous dataflow graphs using Lustre
- Symbolic model checking the knowledge in Herbivore protocol
- Model Revision from Temporal Logic Properties in Computational Systems Biology
- A model learning based testing approach for kernel P systems
- Tighter construction of tight Büchi automata
- Analysis of UML Activities Using Dynamic Meta Modeling
- A New Approach for the Construction of Multiway Decision Graphs
- From Philosophical to Industrial Logics
- Integrating topological proofs with model checking to instrument iterative design
- N-PAT: A Nested Model-Checker
- Towards better heuristics for solving bounded model checking problems
- Benchmarking Model- and Satisfiability-Checking on Bi-infinite Time
- A verification-driven framework for iterative design of controllers
- A logical approach to data-aware automated sequence generation
- Falsification of combined invariance and reachability specifications in hybrid control systems
- Parameterized synthesis of self-stabilizing protocols in symmetric networks
- Diagnosability verification using LTL model checking
- A resolution calculus for the branching-time temporal logic CTL
- \textsc{CoqCryptoLine}: a verified model checker with certified results
- A truly symbolic linear-time algorithm for SCC decomposition
- Verification of SpecC using predicate abstraction
- TOrPEDO : witnessing model correctness with topological proofs
- A first-order coalition logic for BDI-agents
- Cyclic-routing of unmanned aerial vehicles
- Kernel P systems modelling, testing and verification -- sorting case study
- Constrained Kripke structure for identifying parameters of biological models
- Title not available (Why is that?)
- Timed hyperproperties
- Model Checking Contracts – A Case Study
- \texttt{VeriSIMPL 2}: an open-source software for the verification of max-plus-linear systems
- Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system
- Extracting unsatisfiable cores for LTL via temporal resolution
- SMT-based scenario verification for hybrid systems
- Translating Xd-C programs to MSVL programs
- Model checking \(\omega \)-regular properties with decoupled search
- NuMDG: a new tool for multiway decision graphs construction
- Taming the complexity of biochemical models through bisimulation and collapsing: theory and practice
- Interrupt timed automata: verification and expressiveness
- On regular temporal logics with past
- Enhancing unsatisfiable cores for LTL with information on temporal relevance
- Computer Aided Verification
- An action-based approach to the formal specification and automatic analysis of business processes under authorization constraints
- Formal dependability modeling and analysis: a survey
- A Multi-Core Solver for Parity Games
- Action language verifier: An infinite-state model checker for reactive software specifications
- Learning Meets Verification
- Analysing sanity of requirements for avionics systems
- Verification of \(\mathrm{EB}^3\) specifications using CADP
- Bounded situation calculus action theories
- Automatic symbolic compositional verification by learning assumptions
- Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning
- BDD-based symbolic model checking
- SAT-solving in CSP trace refinement
- A decidability result for the model checking of infinite-state systems
- Recasting Constraint Automata into Büchi Automata
- Temporal property verification as a program analysis task
- On the completeness of bounded model checking for threshold-based distributed algorithms: reachability
- Symbolic bounded synthesis
- Early verification and validation of mission critical systems
- Theorem proving for pointwise metric temporal logic over the naturals via translations
- Model checking of biological systems
- Using Bounded Model Checking to Verify Consensus Algorithms
- Modeling and querying biomolecular interaction networks
- Program repair without regret
- Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams
- Deciding Bit-Vector Formulas with mcSAT
- Synthesis of obfuscation policies to ensure privacy and utility
- Title not available (Why is that?)
- Testing Distributed Systems Through Symbolic Model Checking
- From Monadic Logic to PSL
- Automata-Theoretic Model Checking Revisited
- Linear temporal logic symbolic model checking
- Symbolic CTL model checking of asynchronous systems using constrained saturation
Uses Software
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4804909)
