Cited in
(only showing first 100 items - show all)- Extending MSVL with semaphore
- Tools and Algorithms for the Construction and Analysis of Systems
- Kernel P systems modelling, testing and verification -- sorting case study
- A complete proof system for propositional projection temporal logic
- Facilitating the design of fault tolerance in transaction level SystemC programs
- MR4UM: a framework for adding fault tolerance to UML state diagrams
- Models and formal verification of multiprocessor system-on-chips
- scientific article; zbMATH DE number 1956587 (Why is no real title available?)
- scientific article; zbMATH DE number 1744960 (Why is no real title available?)
- Computer Aided Verification
- scientific article; zbMATH DE number 1670767 (Why is no real title available?)
- Timed hyperproperties
- Computation tree logic model checking based on multi-valued possibility measures
- An Event-B based approach for cloud composite services verification
- Temporal Logic for Programmable Logic Controllers
- Spiking neural P systems: matrix representation and formal verification
- Search-based testing in membrane computing
- Verify heaps via unified model checking
- Formal verification of safety protocol in train control system
- Formalization and validation of the general inter-ORB protocol (GIOP) using PROMELA and SPIN
- Syntax-directed model checking of sequential programs
- Establishing local temporal heap safety properties with applications to compile-time memory management
- Analyzing a \(\chi\) model of a turntable system using Spin, CADP and Uppaal
- Model Checking Software
- RGITL: a temporal logic framework for compositional reasoning about interleaved programs
- Formal model-driven design of distributed algorithms
- Theoretical Aspects of Computing – ICTAC 2005
- Efficient SAT-based bounded model checking for software verification
- Declarative parameterized verification of distributed protocols via the Cubicle model checker
- Tools and Algorithms for the Construction and Analysis of Systems
- Model checking workflow net based on Petri net
- Proving stabilization of biological systems
- CTL model checking on a shared-memory architecture
- Distributed breadth-first search LTL model checking
- Formal verification of an executable LTL model checker with partial order reduction
- Visibly linear temporal logic
- Cluster-Based LTL Model Checking of Large Systems
- Hybrid Systems: Computation and Control
- \texttt{VeriSIMPL 2}: an open-source software for the verification of max-plus-linear systems
- A geometric view of partial order reduction
- Enabling synchronous and asynchronous communications in CSP for SOC
- scientific article; zbMATH DE number 1953039 (Why is no real title available?)
- scientific article; zbMATH DE number 2087620 (Why is no real title available?)
- Ant colony optimization with partial order reduction for discovering safety property violations in concurrent models
- Pardinus: a temporal relational model finder
- The Edge of Graph Transformation — Graphs for Behavioural Specification
- Unifying Operational Weak Memory Verification: An Axiomatic Approach
- Model-checking structured context-free languages
- Model checking \(\omega \)-regular properties with decoupled search
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
- Best-first heuristic search for multicore machines
- Translating Xd-C programs to MSVL programs
- Star-Topology Decoupling in SPIN
- Automata theory and model checking
- scientific article; zbMATH DE number 2090517 (Why is no real title available?)
- Model checking of pushdown systems for projection temporal logic
- Dynamic structural operational semantics
- Computer Aided Verification
- The computational complexity of scenario-based agent verification and design
- Efficient on-the-fly model-checking for regular alternation-free -calculus
- Tools and Algorithms for the Construction and Analysis of Systems
- Büchi automata optimisations formalised in Isabelle/HOL
- Selective Approaches for Solving Weak Games
- Compositional analysis of C/C++ programs with veriSoft
- scientific article; zbMATH DE number 1946767 (Why is no real title available?)
- Comparison of algorithms for checking emptiness on Büchi automata
- Two-stage agent program verification
- Family-based SPL model checking using parity games with variability
- ConSpec - A formal language for policy specification
- LTL to self-loop alternating automata with generic acceptance and back
- Model checking of linear-time properties in multi-valued systems
- Model Checking Software
- Compositional verification of a communication protocol for a remotely operated aircraft
- UNITY and Büchi automata
- Fundamental Approaches to Software Engineering
- Constraint LTL satisfiability checking without automata
- Linear Encodings of Bounded LTL Model Checking
- A formal model for service-oriented interactions
- scientific article; zbMATH DE number 1304378 (Why is no real title available?)
- Semantics and pragmatics of real-time maude
- scientific article; zbMATH DE number 1744963 (Why is no real title available?)
- scientific article; zbMATH DE number 1755146 (Why is no real title available?)
- scientific article; zbMATH DE number 1796121 (Why is no real title available?)
- A data-flow approach to test multi-agent ASMs
- Z2SAL: a translation-based model checker for Z
- Model checking with bounded context switching
- Designing the automatic transformation of visual languages
- Towards light-weight probabilistic model checking
- Extending symmetry reduction techniques to a realistic model of computation
- The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
- Inferring Synchronization under Limited Observability
- Model checking dynamic memory allocation in operating systems
- Formal analysis of oscillatory behaviors in biological regulatory networks: an alternative approach
- Formal Modeling and Analysis of Timed Systems
- Reasoning about Conditions and Exceptions to Laws in Regulatory Conformance Checking
- Verifying a signature architecture: a comparative case study
- CTRL: extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks
- Unfoldings: A partial-order approach to model checking.
- Finite and infinite implementation of transition systems
- Unconditional secure communication: a Russian cards protocol
This page was built for software: SPIN
