scientific article; zbMATH DE number 1903365

zbMATH Open1010.68766MaRDI QIDQ4804909FDOQ4804909

Armando Tacchella, Edmund Clarke, Marco Roveri, Marco Pistore, Alessandro Cimatti, Enrico Giunchiglia, Fausto Giunchiglia, Roberto Sebastiani

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?)

Mathematics Subject Classification ID

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
• Model Checking of Biological Systems
• An action-based approach to the formal specification and automatic analysis of business processes under authorization constraints
• 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
• Modeling and Analysis of Gene Regulatory Networks
• 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
• Formal Dependability Modeling and Analysis: A Survey
• Symbolic bounded synthesis
• Early verification and validation of mission critical systems
• Theorem proving for pointwise metric temporal logic over the naturals via translations
• 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
• Testing Distributed Systems Through Symbolic Model Checking
• From Monadic Logic to PSL
• Automata-Theoretic Model Checking Revisited
• Linear temporal logic symbolic model checking
• HRELTL: a temporal logic for hybrid systems
• Agent planning programs
• Analysis of UML Activities Using Dynamic Meta Modeling
• BDD-Based Symbolic Model Checking
• 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
• 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
• Verification of SpecC using predicate abstraction
• 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
• Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation
• Unbeast: Symbolic Bounded Synthesis
• Title not available (Why is that?)
• Spiking neural P systems: matrix representation and formal verification
• Search-based testing in membrane computing
• Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings
• A Logical Approach to Data-Aware Automated Sequence Generation
• 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
• Kernel P Systems Modelling, Testing and Verification - Sorting Case Study
• Integrating Topological Proofs with Model Checking to Instrument Iterative Design
• Synthesis of succinct systems
• Proving Stabilization of Biological 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
• 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
• Model Revision from Temporal Logic Properties in Computational Systems Biology
• Formal verification of timed synchronous dataflow graphs using lustre
• A model learning based testing approach for kernel P systems
• Tighter construction of tight Büchi automata
• A New Approach for the Construction of Multiway Decision Graphs
• From Philosophical to Industrial Logics

Uses Software

• NuSMV
• Chaff

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)