scientific article; zbMATH DE number 1903365

zbMath1010.68766MaRDI QIDQ4804909

Armando Tacchella, Marco Roveri, Marco Pistore, Alessandro Cimatti, Enrico Giunchiglia, Roberto Sebastiani, Edmund M. 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: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Computing methodologies and applications (68U99) Specification and verification (program logics, model checking, etc.) (68Q60)

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

Verification Modulo theories ⋮ ZDD-based algorithmic framework for solving shortest reconfiguration problems ⋮ Towards better heuristics for solving bounded model checking problems ⋮ Constrained Kripke structure for identifying parameters of biological models ⋮ A model learning based testing approach for kernel P systems ⋮ A Multi-Core Solver for Parity Games ⋮ Analysis of UML Activities Using Dynamic Meta Modeling ⋮ Model Revision from Temporal Logic Properties in Computational Systems Biology ⋮ From Monadic Logic to PSL ⋮ Automata-Theoretic Model Checking Revisited ⋮ Recasting Constraint Automata into Büchi Automata ⋮ A New Approach for the Construction of Multiway Decision Graphs ⋮ Benchmarking Model- and Satisfiability-Checking on Bi-infinite Time ⋮ Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system ⋮ Extracting unsatisfiable cores for LTL via temporal resolution ⋮ Timed hyperproperties ⋮ Integrating Topological Proofs with Model Checking to Instrument Iterative Design ⋮ A Logical Approach to Data-Aware Automated Sequence Generation ⋮ Analysing sanity of requirements for avionics systems ⋮ Verification of \(\mathrm{EB}^3\) specifications using CADP ⋮ Bounded situation calculus action theories ⋮ Model checking \(\omega \)-regular properties with decoupled search ⋮ Modeling and querying biomolecular interaction networks ⋮ Taming the complexity of biochemical models through bisimulation and collapsing: theory and practice ⋮ Verification of SpecC using predicate abstraction ⋮ Automatic verification of multi-agent systems by model checking via ordered binary decision diagrams ⋮ A compiler for MSVL and its applications ⋮ BDD-Based Symbolic Model Checking ⋮ Greening R. Thomas' framework with environment variables: a divide and conquer approach ⋮ Aeon 2021: bifurcation decision trees in Boolean networks ⋮ Action language verifier: An infinite-state model checker for reactive software specifications ⋮ Model Checking of Biological Systems ⋮ Formal verification of temporal properties for reduced overhead in grid scientific workflows ⋮ Social bot detection as a temporal logic model checking problem ⋮ Modeling and Analysis of Gene Regulatory Networks ⋮ Formal verification technique for grid service chain model and its application ⋮ Early verification and validation of mission critical systems ⋮ Kernel P systems: from modelling to verification and testing ⋮ A Cookbook for Temporal Conceptual Data Modelling with Description Logics ⋮ Linear-Time Model Checking: Automata Theory in Practice ⋮ HRELTL: a temporal logic for hybrid systems ⋮ Cyclic-routing of unmanned aerial vehicles ⋮ Falsification of combined invariance and reachability specifications in hybrid control systems ⋮ An action-based approach to the formal specification and automatic analysis of business processes under authorization constraints ⋮ Agent planning programs ⋮ Model Checking Contracts – A Case Study ⋮ Bisimulation conversion and verification procedure for goal-based control systems ⋮ NuMDG: a new tool for multiway decision graphs construction ⋮ SAT-solving in CSP trace refinement ⋮ A decidability result for the model checking of infinite-state systems ⋮ An explicit transition system construction approach to LTL satisfiability checking ⋮ Unnamed Item ⋮ Learning Meets Verification ⋮ Kernel P Systems Modelling, Testing and Verification - Sorting Case Study ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A first-order coalition logic for BDI-agents ⋮ Temporal property verification as a program analysis task ⋮ SMT-based scenario verification for hybrid systems ⋮ Interrupt timed automata: verification and expressiveness ⋮ Symbolic bounded synthesis ⋮ Linear temporal logic symbolic model checking ⋮ Using Bounded Model Checking to Verify Consensus Algorithms ⋮ Verification of consensus algorithms using satisfiability solving ⋮ An automatic method for the dynamic construction of abstractions of states of a formal model ⋮ Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning ⋮ Automatic symbolic compositional verification by learning assumptions ⋮ Theorem proving for pointwise metric temporal logic over the naturals via translations ⋮ Toward model selection by formal methods ⋮ Unbeast: Symbolic Bounded Synthesis ⋮ Symbolic Model Checking the Knowledge in Herbivore Protocol ⋮ Verification of Boolean programs with unbounded thread creation ⋮ Spiking neural P systems: matrix representation and formal verification ⋮ Search-based testing in membrane computing ⋮ Strategies, model checking and branching-time properties in Maude ⋮ Complexity of fixed-size bit-vector logics ⋮ Enhancing unsatisfiable cores for LTL with information on temporal relevance ⋮ Component-wise incremental LTL model checking ⋮ Synthesis of obfuscation policies to ensure privacy and utility ⋮ A resolution calculus for the branching-time temporal logic CTL ⋮ Verification and enforcement of access control policies ⋮ Fair multi-party contract signing using private contract signatures ⋮ Model Checking Merged Program Traces ⋮ On regular temporal logics with past ⋮ Producing explanations for rich logics ⋮ Dynamical modeling and analysis of large cellular regulatory networks ⋮ From Philosophical to Industrial Logics ⋮ On the completeness of bounded model checking for threshold-based distributed algorithms: reachability ⋮ Testing Distributed Systems Through Symbolic Model Checking ⋮ Translating Xd-C programs to MSVL programs ⋮ Time-budgeting: a component based development methodology for real-time embedded systems ⋮ Proving Stabilization of Biological Systems ⋮ Formal verification of timed synchronous dataflow graphs using lustre ⋮ Program repair without regret ⋮ Formal Dependability Modeling and Analysis: A Survey ⋮ Performance heuristics for GR(1) synthesis and related algorithms ⋮ Parameterized synthesis of self-stabilizing protocols in symmetric networks ⋮ Deciding Bit-Vector Formulas with mcSAT ⋮ Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings ⋮ TOrPEDO : witnessing model correctness with topological proofs

Uses Software

This page was built for publication: