Synthesis of large dynamic concurrent programs from dynamic specifications

DOI10.1007/s10703-016-0252-9zbMath1392.68143arXiv0801.1687OpenAlexW1677924248MaRDI QIDQ346790

Paul C. Attie

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

zbMATH Keywords

synthesisformal specificationmodel checkingtemporal logicconcurrent programdynamic process creation

Mathematics Subject Classification ID

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

• SyncGen

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