Compositional reasoning

DOI10.1007/978-3-319-10575-8_12MaRDI QIDQ3176370zbMATH OpenOpenAlexFDO

Authors Dimitra Giannakopoulou, Kedar S. Namjoshi, Corina S. Păsăreanu

Publication date 20 July 2018

Published in Handbook of Model Checking (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-10575-8_12

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Abstract patterns of compositional reasoning.
• scientific article; zbMATH DE number 4180789
• Automatic Synthesis of Assumptions for Compositional Model Checking
• On the completeness of compositional reasoning methods
• Compositionality in state space verification methods

Cites work

• scientific article; zbMATH DE number 1701752 (Why is no real title available?)
• scientific article; zbMATH DE number 3926220 (Why is no real title available?)
• scientific article; zbMATH DE number 4050939 (Why is no real title available?)
• scientific article; zbMATH DE number 177514 (Why is no real title available?)
• scientific article; zbMATH DE number 1283472 (Why is no real title available?)
• scientific article; zbMATH DE number 610968 (Why is no real title available?)
• scientific article; zbMATH DE number 1956523 (Why is no real title available?)
• scientific article; zbMATH DE number 1956591 (Why is no real title available?)
• scientific article; zbMATH DE number 1982207 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• scientific article; zbMATH DE number 3423547 (Why is no real title available?)
• A semantics for concurrent separation logic
• Abstract patterns of compositional reasoning.
• Abstraction and abstraction refinement
• All for the price of few (parameterized verification through view abstraction)
• Alternating-time temporal logic
• An abstract account of composition
• An axiomatic basis for computer programming
• Automated Assume-Guarantee Reasoning by Abstraction Refinement
• Automated assumption generation for compositional verification
• Automatic symbolic compositional verification by learning assumptions
• Compositionality Entails Sequentializability
• Computer aided verification. 19th international conference, CAV 2007, Berlin, Germany, July 3--7, 2007. Proceedings.
• Concurrency verification. Introduction to compositional and noncompositional methods
• Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages
• Guarded commands, nondeterminacy and formal derivation of programs
• Inductive data flow graphs
• Inference of finite automata using homing sequences
• Learning Minimal Separating DFA’s for Compositional Verification
• Learning probabilistic systems from tree samples
• Learning regular sets from queries and counterexamples
• Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning
• Learning-based compositional verification for synchronous probabilistic systems
• Local Proofs for Linear-Time Properties of Concurrent Programs
• Local proofs for global safety properties
• Local symmetry and compositional verification
• Modular verification of multithreaded programs
• Nonlinear dynamics of networks: the groupoid formalism
• On the Construction of Submodule Specifications and Communication Protocols
• On the completeness of compositional reasoning methods
• Parallelizing a symbolic compositional model-checking algorithm
• Predicate abstraction and refinement for verifying multi-threaded programs
• Process algebra and model checking
• Proofs of Networks of Processes
• Proving the Correctness of Multiprocess Programs
• Symmetry and Completeness in the Analysis of Parameterized Systems
• Synthesis of interface specifications for Java classes
• Temporal logic and fair discrete systems
• Tentative steps toward a development method for interfering programs
• Three optimizations for assume-guarantee reasoning with \(L^{*}\)
• Uncovering symmetries in irregular process networks
• Verification of parameterized concurrent programs by modular reasoning about data and control
• Verifying properties of parallel programs

Cited in

(10)

• Aspects of compositionality
• Compositional verification of railway interlocking systems
• Formal features of compositionality
• Compositional Reasoning about Shared Futures
• Compositional reasoning using intervals and time reversal
• scientific article; zbMATH DE number 1759496 (Why is no real title available?)
• \textsc{LTL} falsification in infinite-state systems
• The comprehension construction
• Compositional CompCert
• Proving the existence of fair paths in infinite-state systems

Describes a project that uses

Uses Software

• MOCHA

This page was built for publication: Compositional reasoning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3176370)