Automatic Synthesis of Assumptions for Compositional Model Checking

DOI10.1007/11888116_12MaRDI QIDQ3613064zbMATH OpenOpenAlexFDO

Authors Bernd Finkbeiner, Sven Schewe, Matthias Brill

Publication date 11 March 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11888116_12

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)

Recommendations

• Automated Assumption Generation for Compositional Verification
• Automated assumption generation for compositional verification
• Automatic symbolic compositional verification by learning assumptions
• scientific article; zbMATH DE number 4180789
• Parameterized compositional model checking
• Computer Aided Verification
• scientific article; zbMATH DE number 1670785
• Compositional and quantitative model checking (extended abstract)
• scientific article; zbMATH DE number 1903350

Cites work

• Compositional minimisation of finite state systems using interface specifications
• Computer Aided Verification
• scientific article; zbMATH DE number 1670774 (Why is no real title available?)
• scientific article; zbMATH DE number 1693039 (Why is no real title available?)
• scientific article; zbMATH DE number 4180789 (Why is no real title available?)
• scientific article; zbMATH DE number 1956591 (Why is no real title available?)
• scientific article; zbMATH DE number 1798181 (Why is no real title available?)
• scientific article; zbMATH DE number 1863177 (Why is no real title available?)
• Synthesis of interface specifications for Java classes
• The Rely-Guarantee method for verifying shared variable concurrent programs

Cited in

(8)

• Assumption-commitment support for CSP model checking
• An explanatory presentation of composition rules for assumption- commitment specifications
• Compositional reasoning
• On the dynamics of a pendulum mounted on a movable platform
• A study of permanent rotations of a heavy dynamically symmetric rigid body with a vibrating suspension point
• Automated Technology for Verification and Analysis
• Information Flow Guided Synthesis
• Automated assumption generation for compositional verification

Describes a project that uses

Uses Software

• SPIN

This page was built for publication: Automatic Synthesis of Assumptions for Compositional Model Checking

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