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)
- 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
- HRELTL: a temporal logic for hybrid systems
- Agent planning programs
- An executable specification of a formal argumentation protocol
- Formal verification technique for grid service chain model and its application
- A rigorous methodology for specification and verification of business processes
- Time-budgeting: a component based development methodology for real-time embedded systems
- Bisimulation conversion and verification procedure for goal-based control systems
- Fair multi-party contract signing using private contract signatures
- Verification of Boolean programs with unbounded thread creation
- Modeling and analysis of gene regulatory networks
- Using formal verification to evaluate the execution time of Spark applications
- Compressing BMC encodings with QBF
- Complexity of fixed-size bit-vector logics
- Dynamical modeling and analysis of large cellular regulatory networks
- Verification of consensus algorithms using satisfiability solving
- Component-wise incremental LTL model checking
- NuSMV: A new symbolic model checker
- A compiler for MSVL and its applications
- Translating Java for multiple model checkers: The Bandera back-end
- SAT-based explicit LTL reasoning and its application to satisfiability checking
- Unbeast: Symbolic Bounded Synthesis
- 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
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)
