Synthesis of large dynamic concurrent programs from dynamic specifications
From MaRDI portal
Publication:346790
DOI10.1007/s10703-016-0252-9zbMath1392.68143arXiv0801.1687OpenAlexW1677924248MaRDI QIDQ346790
Publication date: 30 November 2016
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/0801.1687
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Modular Verification of Interactive Systems with an Application to Biology, Finite-state concurrent programs can be expressed in pairwise normal form
Uses Software
Cites Work
- Reasoning about networks with many identical finite state processes
- Using branching time temporal logic to synthesize synchronization skeletons
- Characterizing finite Kripke structures in propositional temporal logic
- Eventually-serializable data services
- Enhancing model checking in verification by AI techniques
- Modalities for model checking: Branching time logic strikes back
- Symbolic synthesis of masking fault-tolerant distributed programs
- A framework for automated distributed implementation of component-based models
- Dynamic input/output automata: a formal and compositional model for dynamic systems
- Synthesis of fault-tolerant concurrent programs
- Synthesis of concurrent systems for an atomic read/atomic write model of computation
- Synthesis from Component Libraries with Costs
- Abstract Model Repair
- Bounded Synthesis
- Temporal Verification of Reactive Systems: Response
- Synthesis from Component Libraries
- Synthesis of Communicating Processes from Temporal Logic Specifications
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Self-stabilizing systems in spite of distributed control
- Reasoning about systems with many processes
- Decidability of Parameterized Verification
- Computer Aided Verification
- Latticed-LTL Synthesis in the Presence of Noisy Inputs
- An axiomatic basis for computer programming
- Depth-First Search and Linear Graph Algorithms
- Verification, Model Checking, and Abstract Interpretation
- Finite-state concurrent programs can be expressed in pairwise normal form
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
